{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Bicategory.Kan where

import Data.Kind (Constraint)

import Proarrow.Category.Bicategory (Bicategory (..), (==), (||), Monad (..), rightUnitorInvWith, Comonad (..), rightUnitorWith)
import Proarrow.Category.Equipment
  ( Equipment (..)
  , HasCompanions (..)
  , flipCompanion
  , flipCompanionInv
  , flipConjoint
  , flipConjointInv
  )
import Proarrow.Core (CAT, CategoryOf (..), Ob, Obj, Profunctor (..), Promonad (..), obj, (\\))

type LeftKanExtension :: forall {k} {kk :: CAT k} {c} {d} {e}. kk c d -> kk c e -> Constraint
class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Lan j f)) => LeftKanExtension (j :: kk c d) (f :: kk c e) where
  type Lan j f :: kk d e
  lan :: f ~> Lan j f `O` j
  lanUniv :: (Ob g) => (f ~> g `O` j) -> Lan j f ~> g

mapLan :: forall j f g. (LeftKanExtension j f, LeftKanExtension j g) => (f ~> g) -> Lan j f ~> Lan j g
mapLan :: forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk c e).
(LeftKanExtension j f, LeftKanExtension j g) =>
(f ~> g) -> Lan j f ~> Lan j g
mapLan f ~> g
fg = forall (j :: kk c d) (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
lanUniv @j (forall (j :: kk c d) (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
lan @j (g ~> O (Lan j g) j) -> (f ~> g) -> f ~> O (Lan j g) j
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. f ~> g
fg)

rebaseLan :: forall f i j. (LeftKanExtension j f, LeftKanExtension i f) => (i ~> j) -> Lan j f ~> Lan i f
rebaseLan :: forall {k} {kk :: CAT k} {c :: k} {e :: k} {d :: k} (f :: kk c e)
       (i :: kk c d) (j :: kk c d).
(LeftKanExtension j f, LeftKanExtension i f) =>
(i ~> j) -> Lan j f ~> Lan i f
rebaseLan i ~> j
ij = forall (j :: kk c d) (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
lanUniv @j ((forall (a :: kk d e). (CategoryOf (kk d e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Lan i f) Obj (Lan i f) -> (i ~> j) -> O (Lan i f) i ~> O (Lan i f) j
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` i ~> j
ij) (O (Lan i f) i ~> O (Lan i f) j)
-> (f ~> O (Lan i f) i) -> f ~> O (Lan i f) j
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk c d) (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
lan @i @f)

dimapLan :: forall i j f g. (LeftKanExtension j f, LeftKanExtension i g) => (i ~> j) -> (f ~> g) -> (Lan j f ~> Lan i g)
dimapLan :: forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (i :: kk c d)
       (j :: kk c d) (f :: kk c e) (g :: kk c e).
(LeftKanExtension j f, LeftKanExtension i g) =>
(i ~> j) -> (f ~> g) -> Lan j f ~> Lan i g
dimapLan i ~> j
ij f ~> g
fg = forall (j :: kk c d) (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
lanUniv @j ((forall (a :: kk d e). (CategoryOf (kk d e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Lan i g) Obj (Lan i g) -> (i ~> j) -> O (Lan i g) i ~> O (Lan i g) j
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` i ~> j
ij) (O (Lan i g) i ~> O (Lan i g) j)
-> (f ~> O (Lan i g) i) -> f ~> O (Lan i g) j
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk c d) (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
lan @i (g ~> O (Lan i g) i) -> (f ~> g) -> f ~> O (Lan i g) i
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. f ~> g
fg) ((Ob i, Ob j) => Lan j f ~> Lan i g)
-> (i ~> j) -> Lan j f ~> Lan i g
forall (a :: kk c d) (b :: kk c d) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ i ~> j
ij

type Density p = Lan p p

lanComonadEpsilon :: forall {kk} {c} {d} (p :: kk c d). (LeftKanExtension p p) => Density p ~> I
lanComonadEpsilon :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} (p :: kk c d).
LeftKanExtension p p =>
Density p ~> I
lanComonadEpsilon = forall (j :: kk c d) (f :: kk c d) (g :: kk d d).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
lanUniv @p @p p ~> O I p
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
leftUnitorInv

lanComonadDelta :: forall {kk} {c} {d} (p :: kk c d). (LeftKanExtension p p) => Density p ~> Density p `O` Density p
lanComonadDelta :: forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (p :: kk c d).
LeftKanExtension p p =>
Density p ~> O (Density p) (Density p)
lanComonadDelta =
  let lpp :: Obj (Lan p p)
lpp = forall (a :: kk d d). (CategoryOf (kk d d), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Lan p p)
  in forall (j :: kk c d) (f :: kk c d) (g :: kk d d).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
lanUniv @p @p (forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @_ @(Lan p p) @(Lan p p) @p (O (Lan p p) (O (Lan p p) p) ~> O (O (Lan p p) (Lan p p)) p)
-> (p ~> O (Lan p p) (O (Lan p p) p))
-> p ~> O (O (Lan p p) (Lan p p)) p
forall (b :: kk c d) (c :: kk c d) (a :: kk c d).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj (Lan p p)
lpp Obj (Lan p p)
-> (p ~> O (Lan p p) p)
-> O (Lan p p) p ~> O (Lan p p) (O (Lan p p) p)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (j :: kk c d) (f :: kk c d).
LeftKanExtension j f =>
f ~> O (Lan j f) j
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
lan @p @p) (O (Lan p p) p ~> O (Lan p p) (O (Lan p p) p))
-> (p ~> O (Lan p p) p) -> p ~> O (Lan p p) (O (Lan p p) p)
forall (b :: kk c d) (c :: kk c d) (a :: kk c d).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk c d) (f :: kk c d).
LeftKanExtension j f =>
f ~> O (Lan j f) j
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
lan @p @p)
      ((Ob (O (Lan p p) (Lan p p)), Ob (O (Lan p p) (Lan p p))) =>
 Lan p p ~> O (Lan p p) (Lan p p))
-> (O (Lan p p) (Lan p p) ~> O (Lan p p) (Lan p p))
-> Lan p p ~> O (Lan p p) (Lan p p)
forall (a :: kk d d) (b :: kk d d) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Obj (Lan p p)
lpp Obj (Lan p p)
-> Obj (Lan p p) -> O (Lan p p) (Lan p p) ~> O (Lan p p) (Lan p p)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj (Lan p p)
lpp)

-- | Density is the "mother of all comonads"
coinj :: forall p. (Comonad p, LeftKanExtension p p) => p ~> Density p
coinj :: forall {k} {kk :: CAT k} {c :: k} (p :: kk c c).
(Comonad p, LeftKanExtension p p) =>
p ~> Density p
coinj = (p ~> I) -> (Lan p p ~> Lan p p) -> O (Lan p p) p ~> Lan p p
forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
       (a :: kk i k) (b :: kk i k).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O a c ~> b
rightUnitorWith (forall (t :: kk c c). Comonad t => t ~> I
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> I
epsilon @p) Lan p p ~> Lan p p
forall (a :: kk c c). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (O (Lan p p) p ~> Lan p p) -> (p ~> O (Lan p p) p) -> p ~> Lan p p
forall (b :: kk c c) (c :: kk c c) (a :: kk c c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk c c) (f :: kk c c).
LeftKanExtension j f =>
f ~> O (Lan j f) j
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
lan @p @p

corun :: forall p. (Comonad p, LeftKanExtension p p) => Density p ~> p
corun :: forall {k} {kk :: CAT k} {c :: k} (p :: kk c c).
(Comonad p, LeftKanExtension p p) =>
Density p ~> p
corun = forall (j :: kk c c) (f :: kk c c) (g :: kk c c).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
lanUniv @p @p p ~> O p p
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> O t t
delta

idLan :: forall f. (LeftKanExtension I f, Ob f) => f ~> Lan I f
idLan :: forall {s} {kk :: CAT s} {c :: s} {e :: s} (f :: kk c e).
(LeftKanExtension I f, Ob f) =>
f ~> Lan I f
idLan = O (Lan I f) I ~> Lan I f
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
rightUnitor (O (Lan I f) I ~> Lan I f) -> (f ~> O (Lan I f) I) -> f ~> Lan I f
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk c c) (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
lan @I @f

lanAlongCompanion
  :: forall {i} {k} hk vk (j :: vk i k) f
   . (LeftKanExtension (Companion hk j) f, Equipment hk vk)
  => Obj j
  -> Lan (Companion hk j) f ~> f `O` Conjoint hk j
lanAlongCompanion :: forall {c} {k :: c} {i :: c} {k :: c} (hk :: CAT c) (vk :: CAT c)
       (j :: vk i k) (f :: hk i k).
(LeftKanExtension (Companion hk j) f, Equipment hk vk) =>
Obj j -> Lan (Companion hk j) f ~> O f (Conjoint hk j)
lanAlongCompanion Obj j
j =
  let f :: Obj f
f = forall (a :: hk i k). (CategoryOf (hk i k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f; conJ :: Conjoint hk j ~> Conjoint hk j
conJ = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
forall (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk Obj j
j
  in forall (j :: hk i k) (f :: hk i k) (g :: hk k k).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> Lan j f ~> g
lanUniv @(Companion hk j) @f
      (f ~> O f I
forall {i :: c} {j :: c} (a :: hk i j).
(Ob0 hk i, Ob0 hk j, Ob a) =>
a ~> O a I
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O a I
rightUnitorInv (f ~> O f I)
-> (O f I ~> O f (O (Conjoint hk j) (Companion hk j)))
-> f ~> O f (O (Conjoint hk j) (Companion hk j))
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== Obj f
f Obj f
-> (I ~> O (Conjoint hk j) (Companion hk j))
-> O f I ~> O f (O (Conjoint hk j) (Companion hk j))
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj j -> I ~> O (Conjoint hk j) (Companion hk j)
forall {j :: c} {k :: c} (f :: vk j k).
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
comConUnit Obj j
j (f ~> O f (O (Conjoint hk j) (Companion hk j)))
-> (O f (O (Conjoint hk j) (Companion hk j))
    ~> O (O f (Conjoint hk j)) (Companion hk j))
-> f ~> O (O f (Conjoint hk j)) (Companion hk j)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
forall (kk :: CAT c) {h :: c} {i :: c} {j :: c} {k :: c}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @_ @f @(Conjoint hk j) @(Companion hk j))
      ((Ob (O f (Conjoint hk j)), Ob (O f (Conjoint hk j))) =>
 Lan (Companion hk j) f ~> O f (Conjoint hk j))
-> (O f (Conjoint hk j) ~> O f (Conjoint hk j))
-> Lan (Companion hk j) f ~> O f (Conjoint hk j)
forall (a :: hk k k) (b :: hk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Obj f
f Obj f
-> (Conjoint hk j ~> Conjoint hk j)
-> O f (Conjoint hk j) ~> O f (Conjoint hk j)
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
       (c :: hk i j) (d :: hk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Conjoint hk j ~> Conjoint hk j
conJ)
      ((Ob (Conjoint hk j), Ob (Conjoint hk j)) =>
 Lan (Companion hk j) f ~> O f (Conjoint hk j))
-> (Conjoint hk j ~> Conjoint hk j)
-> Lan (Companion hk j) f ~> O f (Conjoint hk j)
forall (a :: hk k i) (b :: hk k i) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Conjoint hk j ~> Conjoint hk j
conJ

lanAlongCompanionInv
  :: forall {i} {k} hk vk (j :: vk i k) f
   . (LeftKanExtension (Companion hk j) f, Equipment hk vk)
  => Obj j
  -> f `O` Conjoint hk j ~> Lan (Companion hk j) f
lanAlongCompanionInv :: forall {k} {e :: k} {i :: k} {k :: k} (hk :: CAT k) (vk :: CAT k)
       (j :: vk i k) (f :: hk i e).
(LeftKanExtension (Companion hk j) f, Equipment hk vk) =>
Obj j -> O f (Conjoint hk j) ~> Lan (Companion hk j) f
lanAlongCompanionInv Obj j
j = forall (f :: vk i k) (p :: hk i e) (q :: hk k e).
(Equipment hk vk, Ob q) =>
Obj f -> (p ~> O q (Companion hk f)) -> O p (Conjoint hk f) ~> q
forall {c} {k1 :: c} {j :: c} {k2 :: c} {hk :: CAT c} {vk :: CAT c}
       (f :: vk j k2) (p :: hk j k1) (q :: hk k2 k1).
(Equipment hk vk, Ob q) =>
Obj f -> (p ~> O q (Companion hk f)) -> O p (Conjoint hk f) ~> q
flipConjointInv @j @f @(Lan (Companion hk j) f) Obj j
j (forall (j :: hk i k) (f :: hk i e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
lan @(Companion hk j))

type j |> p = Ran j p
type RightKanExtension :: forall {k} {kk :: CAT k} {c} {d} {e}. kk c d -> kk c e -> Constraint
class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Ran j f)) => RightKanExtension (j :: kk c d) (f :: kk c e) where
  type Ran j f :: kk d e
  ran :: Ran j f `O` j ~> f
  ranUniv :: (Ob g) => (g `O` j ~> f) -> g ~> Ran j f

mapRan :: forall j f g. (RightKanExtension j f, RightKanExtension j g) => (f ~> g) -> Ran j f ~> Ran j g
mapRan :: forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk c e).
(RightKanExtension j f, RightKanExtension j g) =>
(f ~> g) -> Ran j f ~> Ran j g
mapRan f ~> g
fg = forall (j :: kk c d) (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
ranUniv @j (f ~> g
fg (f ~> g) -> (O (Ran j f) j ~> f) -> O (Ran j f) j ~> g
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk c d) (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
ran @j)

rebaseRan :: forall f i j. (RightKanExtension j f, RightKanExtension i f) => (i ~> j) -> Ran j f ~> Ran i f
rebaseRan :: forall {k} {kk :: CAT k} {c :: k} {e :: k} {d :: k} (f :: kk c e)
       (i :: kk c d) (j :: kk c d).
(RightKanExtension j f, RightKanExtension i f) =>
(i ~> j) -> Ran j f ~> Ran i f
rebaseRan i ~> j
ij = forall (j :: kk c d) (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
ranUniv @i @f (forall (j :: kk c d) (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
ran @j (O (Ran j f) j ~> f)
-> (O (Ran j f) i ~> O (Ran j f) j) -> O (Ran j f) i ~> f
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: kk d e). (CategoryOf (kk d e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Ran j f) Obj (Ran j f) -> (i ~> j) -> O (Ran j f) i ~> O (Ran j f) j
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` i ~> j
ij))

dimapRan
  :: forall i j f g. (RightKanExtension j f, RightKanExtension i g) => (i ~> j) -> (f ~> g) -> (Ran j f ~> Ran i g)
dimapRan :: forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (i :: kk c d)
       (j :: kk c d) (f :: kk c e) (g :: kk c e).
(RightKanExtension j f, RightKanExtension i g) =>
(i ~> j) -> (f ~> g) -> Ran j f ~> Ran i g
dimapRan i ~> j
ij f ~> g
fg = forall (j :: kk c d) (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
ranUniv @i (f ~> g
fg (f ~> g) -> (O (Ran j f) i ~> f) -> O (Ran j f) i ~> g
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk c d) (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
ran @j (O (Ran j f) j ~> f)
-> (O (Ran j f) i ~> O (Ran j f) j) -> O (Ran j f) i ~> f
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: kk d e). (CategoryOf (kk d e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Ran j f) Obj (Ran j f) -> (i ~> j) -> O (Ran j f) i ~> O (Ran j f) j
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` i ~> j
ij)) ((Ob i, Ob j) => Ran j f ~> Ran i g)
-> (i ~> j) -> Ran j f ~> Ran i g
forall (a :: kk c d) (b :: kk c d) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ i ~> j
ij

type Codensity p = Ran p p

ranMonadEta :: forall {kk} {c} {d} (p :: kk c d). (RightKanExtension p p) => I ~> Codensity p
ranMonadEta :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} (p :: kk c d).
RightKanExtension p p =>
I ~> Codensity p
ranMonadEta = forall (j :: kk c d) (f :: kk c d) (g :: kk d d).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
ranUniv @p @p O I p ~> p
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
leftUnitor

ranMonadMu :: forall {kk} {c} {d} (p :: kk c d). (RightKanExtension p p) => Codensity p `O` Codensity p ~> Codensity p
ranMonadMu :: forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (p :: kk c d).
RightKanExtension p p =>
O (Codensity p) (Codensity p) ~> Codensity p
ranMonadMu =
  let rpp :: Obj (Ran p p)
rpp = forall (a :: kk d d). (CategoryOf (kk d d), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Ran p p)
  in forall (j :: kk c d) (f :: kk c d) (g :: kk d d).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
ranUniv @p @p (forall (j :: kk c d) (f :: kk c d).
RightKanExtension j f =>
O (Ran j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
ran @p @p (O (Ran p p) p ~> p)
-> (O (O (Ran p p) (Ran p p)) p ~> O (Ran p p) p)
-> O (O (Ran p p) (Ran p p)) p ~> p
forall (b :: kk c d) (c :: kk c d) (a :: kk c d).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj (Ran p p)
rpp Obj (Ran p p)
-> (O (Ran p p) p ~> p)
-> O (Ran p p) (O (Ran p p) p) ~> O (Ran p p) p
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (j :: kk c d) (f :: kk c d).
RightKanExtension j f =>
O (Ran j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
ran @p @p) (O (Ran p p) (O (Ran p p) p) ~> O (Ran p p) p)
-> (O (O (Ran p p) (Ran p p)) p ~> O (Ran p p) (O (Ran p p) p))
-> O (O (Ran p p) (Ran p p)) p ~> O (Ran p p) p
forall (b :: kk c d) (c :: kk c d) (a :: kk c d).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @_ @(Ran p p) @(Ran p p) @p) ((Ob (O (Ran p p) (Ran p p)), Ob (O (Ran p p) (Ran p p))) =>
 O (Ran p p) (Ran p p) ~> Ran p p)
-> (O (Ran p p) (Ran p p) ~> O (Ran p p) (Ran p p))
-> O (Ran p p) (Ran p p) ~> Ran p p
forall (a :: kk d d) (b :: kk d d) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Obj (Ran p p)
rpp Obj (Ran p p)
-> Obj (Ran p p) -> O (Ran p p) (Ran p p) ~> O (Ran p p) (Ran p p)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj (Ran p p)
rpp)

-- | Codensity is the "mother of all monads"
inj :: forall p. (Monad p, RightKanExtension p p) => p ~> Codensity p
inj :: forall {k} {kk :: CAT k} {c :: k} (p :: kk c c).
(Monad p, RightKanExtension p p) =>
p ~> Codensity p
inj = forall (j :: kk c c) (f :: kk c c) (g :: kk c c).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
ranUniv @p @p O p p ~> p
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
O t t ~> t
mu

run :: forall p. (Monad p, RightKanExtension p p) => Codensity p ~> p
run :: forall {k} {kk :: CAT k} {c :: k} (p :: kk c c).
(Monad p, RightKanExtension p p) =>
Codensity p ~> p
run = forall (j :: kk c c) (f :: kk c c).
RightKanExtension j f =>
O (Ran j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
ran @p @p (O (Ran p p) p ~> p) -> (Ran p p ~> O (Ran p p) p) -> Ran p p ~> p
forall (b :: kk c c) (c :: kk c c) (a :: kk c c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (I ~> p) -> (Ran p p ~> Ran p p) -> Ran p p ~> O (Ran p p) p
forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
       (a :: kk i k) (b :: kk i k).
Bicategory kk =>
(I ~> c) -> (a ~> b) -> a ~> O b c
rightUnitorInvWith (forall (t :: kk c c). Monad t => I ~> t
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
I ~> t
eta @p) Ran p p ~> Ran p p
forall (a :: kk c c). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

composeRan
  :: forall i j f
   . (RightKanExtension j f, RightKanExtension i (Ran j f), RightKanExtension (i `O` j) f)
  => Ran i (Ran j f) ~> Ran (i `O` j) f
composeRan :: forall {k} {kk :: CAT k} {j :: k} {d :: k} {c :: k} {e :: k}
       (i :: kk j d) (j :: kk c j) (f :: kk c e).
(RightKanExtension j f, RightKanExtension i (Ran j f),
 RightKanExtension (O i j) f) =>
Ran i (Ran j f) ~> Ran (O i j) f
composeRan =
  forall (j :: kk c d) (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
ranUniv @(i `O` j) @f
    (forall (j :: kk c j) (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
ran @j @f (O (Ran j f) j ~> f)
-> (O (Ran i (Ran j f)) (O i j) ~> O (Ran j f) j)
-> O (Ran i (Ran j f)) (O i j) ~> f
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (j :: kk j d) (f :: kk j e).
RightKanExtension j f =>
O (Ran j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
ran @i @(Ran j f) (O (Ran i (Ran j f)) i ~> Ran j f)
-> (j ~> j) -> O (O (Ran i (Ran j f)) i) j ~> O (Ran j f) j
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk c j). (CategoryOf (kk c j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j) (O (O (Ran i (Ran j f)) i) j ~> O (Ran j f) j)
-> (O (Ran i (Ran j f)) (O i j) ~> O (O (Ran i (Ran j f)) i) j)
-> O (Ran i (Ran j f)) (O i j) ~> O (Ran j f) j
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @_ @(Ran i (Ran j f)) @i @j)

idRan :: forall f. (RightKanExtension I f, Ob f) => f ~> Ran I f
idRan :: forall {s} {kk :: CAT s} {c :: s} {e :: s} (f :: kk c e).
(RightKanExtension I f, Ob f) =>
f ~> Ran I f
idRan = forall (j :: kk c c) (f :: kk c e) (g :: kk c e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
ranUniv @I @f O f I ~> f
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
rightUnitor

ranAlongConjoint
  :: forall {i} {k} hk vk (j :: vk i k) f
   . (RightKanExtension (Conjoint hk j) f, Equipment hk vk)
  => Obj j
  -> Ran (Conjoint hk j) f ~> f `O` Companion hk j
ranAlongConjoint :: forall {c} {k :: c} {i :: c} {k :: c} (hk :: CAT c) (vk :: CAT c)
       (j :: vk i k) (f :: hk k k).
(RightKanExtension (Conjoint hk j) f, Equipment hk vk) =>
Obj j -> Ran (Conjoint hk j) f ~> O f (Companion hk j)
ranAlongConjoint Obj j
j = forall (f :: vk i k) (p :: hk i k) (q :: hk k k).
(Equipment hk vk, Ob p) =>
Obj f -> (O p (Conjoint hk f) ~> q) -> p ~> O q (Companion hk f)
forall {c} {k1 :: c} {j :: c} {k2 :: c} {hk :: CAT c} {vk :: CAT c}
       (f :: vk j k2) (p :: hk j k1) (q :: hk k2 k1).
(Equipment hk vk, Ob p) =>
Obj f -> (O p (Conjoint hk f) ~> q) -> p ~> O q (Companion hk f)
flipConjoint @j @(Ran (Conjoint hk j) f) @f Obj j
j (forall (j :: hk k i) (f :: hk k k).
RightKanExtension j f =>
O (Ran j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
ran @(Conjoint hk j))

ranAlongConjointInv
  :: forall {i} {k} hk vk (j :: vk i k) f
   . (RightKanExtension (Conjoint hk j) f, Equipment hk vk)
  => Obj j
  -> f `O` Companion hk j ~> Ran (Conjoint hk j) f
ranAlongConjointInv :: forall {k} {e :: k} {i :: k} {k :: k} (hk :: CAT k) (vk :: CAT k)
       (j :: vk i k) (f :: hk k e).
(RightKanExtension (Conjoint hk j) f, Equipment hk vk) =>
Obj j -> O f (Companion hk j) ~> Ran (Conjoint hk j) f
ranAlongConjointInv Obj j
j =
  let f :: Obj f
f = forall (a :: hk k e). (CategoryOf (hk k e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f; comJ :: Companion hk j ~> Companion hk j
comJ = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj j
j
  in forall (j :: hk k i) (f :: hk k e) (g :: hk i e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> f) -> g ~> Ran j f
ranUniv @(Conjoint hk j) @f (O f I ~> f
forall {i :: k} {j :: k} (a :: hk i j).
(Ob0 hk i, Ob0 hk j, Ob a) =>
O a I ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
rightUnitor (O f I ~> f)
-> (O (O f (Companion hk j)) (Conjoint hk j) ~> O f I)
-> O (O f (Companion hk j)) (Conjoint hk j) ~> f
forall (b :: hk k e) (c :: hk k e) (a :: hk k e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj f
f Obj f
-> (O (Companion hk j) (Conjoint hk j) ~> I)
-> O f (O (Companion hk j) (Conjoint hk j)) ~> O f I
forall {i :: k} (j :: k) (k :: k) (a :: hk j k) (b :: hk j k)
       (c :: hk i j) (d :: hk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj j -> O (Companion hk j) (Conjoint hk j) ~> I
forall {j :: k} {k :: k} (f :: vk j k).
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
comConCounit Obj j
j) (O f (O (Companion hk j) (Conjoint hk j)) ~> O f I)
-> (O (O f (Companion hk j)) (Conjoint hk j)
    ~> O f (O (Companion hk j) (Conjoint hk j)))
-> O (O f (Companion hk j)) (Conjoint hk j) ~> O f I
forall (b :: hk k e) (c :: hk k e) (a :: hk k e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @_ @f @(Companion hk j) @(Conjoint hk j))
      ((Ob (O f (Companion hk j)), Ob (O f (Companion hk j))) =>
 O f (Companion hk j) ~> Ran (Conjoint hk j) f)
-> (O f (Companion hk j) ~> O f (Companion hk j))
-> O f (Companion hk j) ~> Ran (Conjoint hk j) f
forall (a :: hk i e) (b :: hk i e) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Obj f
f Obj f
-> (Companion hk j ~> Companion hk j)
-> O f (Companion hk j) ~> O f (Companion hk j)
forall {i :: k} (j :: k) (k :: k) (a :: hk j k) (b :: hk j k)
       (c :: hk i j) (d :: hk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Companion hk j ~> Companion hk j
comJ)
      ((Ob (Companion hk j), Ob (Companion hk j)) =>
 O f (Companion hk j) ~> Ran (Conjoint hk j) f)
-> (Companion hk j ~> Companion hk j)
-> O f (Companion hk j) ~> Ran (Conjoint hk j) f
forall (a :: hk i k) (b :: hk i k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Companion hk j ~> Companion hk j
comJ

type LeftKanLift :: forall {k} {kk :: CAT k} {c} {d} {e}. kk d c -> kk e c -> Constraint
class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Lift j f)) => LeftKanLift (j :: kk d c) (f :: kk e c) where
  type Lift j f :: kk e d
  lift :: f ~> j `O` Lift j f
  liftUniv :: (Ob g) => (f ~> j `O` g) -> Lift j f ~> g

mapLift :: forall j f g. (LeftKanLift j f, LeftKanLift j g) => (f ~> g) -> Lift j f ~> Lift j g
mapLift :: forall {k} {kk :: CAT k} {d :: k} {c :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e c).
(LeftKanLift j f, LeftKanLift j g) =>
(f ~> g) -> Lift j f ~> Lift j g
mapLift f ~> g
fg = forall (j :: kk d c) (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> Lift j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> Lift j f ~> g
liftUniv @j (forall (j :: kk d c) (f :: kk e c).
LeftKanLift j f =>
f ~> O j (Lift j f)
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
LeftKanLift j f =>
f ~> O j (Lift j f)
lift @j (g ~> O j (Lift j g)) -> (f ~> g) -> f ~> O j (Lift j g)
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. f ~> g
fg)

rebaseLift :: forall f i j. (LeftKanLift j f, LeftKanLift i f) => (i ~> j) -> Lift j f ~> Lift i f
rebaseLift :: forall {k} {kk :: CAT k} {e :: k} {c :: k} {d :: k} (f :: kk e c)
       (i :: kk d c) (j :: kk d c).
(LeftKanLift j f, LeftKanLift i f) =>
(i ~> j) -> Lift j f ~> Lift i f
rebaseLift i ~> j
ij = forall (j :: kk d c) (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> Lift j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> Lift j f ~> g
liftUniv @j ((i ~> j
ij (i ~> j)
-> (Lift i f ~> Lift i f) -> O i (Lift i f) ~> O j (Lift i f)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk e d). (CategoryOf (kk e d), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Lift i f)) (O i (Lift i f) ~> O j (Lift i f))
-> (f ~> O i (Lift i f)) -> f ~> O j (Lift i f)
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk d c) (f :: kk e c).
LeftKanLift j f =>
f ~> O j (Lift j f)
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
LeftKanLift j f =>
f ~> O j (Lift j f)
lift @i @f)

dimapLift :: forall i j f g. (LeftKanLift j f, LeftKanLift i g) => (i ~> j) -> (f ~> g) -> (Lift j f ~> Lift i g)
dimapLift :: forall {k} {kk :: CAT k} {d :: k} {c :: k} {e :: k} (i :: kk d c)
       (j :: kk d c) (f :: kk e c) (g :: kk e c).
(LeftKanLift j f, LeftKanLift i g) =>
(i ~> j) -> (f ~> g) -> Lift j f ~> Lift i g
dimapLift i ~> j
ij f ~> g
fg = forall (j :: kk d c) (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> Lift j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> Lift j f ~> g
liftUniv @j ((i ~> j
ij (i ~> j)
-> (Lift i g ~> Lift i g) -> O i (Lift i g) ~> O j (Lift i g)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk e d). (CategoryOf (kk e d), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Lift i g)) (O i (Lift i g) ~> O j (Lift i g))
-> (f ~> O i (Lift i g)) -> f ~> O j (Lift i g)
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk d c) (f :: kk e c).
LeftKanLift j f =>
f ~> O j (Lift j f)
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
LeftKanLift j f =>
f ~> O j (Lift j f)
lift @i (g ~> O i (Lift i g)) -> (f ~> g) -> f ~> O i (Lift i g)
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. f ~> g
fg) ((Ob i, Ob j) => Lift j f ~> Lift i g)
-> (i ~> j) -> Lift j f ~> Lift i g
forall (a :: kk d c) (b :: kk d c) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ i ~> j
ij

liftComonadEpsilon :: forall {kk} {c} {d} (p :: kk d c). (LeftKanLift p p) => Lift p p ~> I
liftComonadEpsilon :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} (p :: kk d c).
LeftKanLift p p =>
Lift p p ~> I
liftComonadEpsilon = forall (j :: kk d c) (f :: kk d c) (g :: kk d d).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> Lift j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> Lift j f ~> g
liftUniv @p @p p ~> O p I
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O a I
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O a I
rightUnitorInv

liftComonadDelta :: forall {kk} {c} {d} (p :: kk d c). (LeftKanLift p p) => Lift p p ~> Lift p p `O` Lift p p
liftComonadDelta :: forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (p :: kk d c).
LeftKanLift p p =>
Lift p p ~> O (Lift p p) (Lift p p)
liftComonadDelta =
  let lpp :: Obj (Lift p p)
lpp = forall (a :: kk d d). (CategoryOf (kk d d), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Lift p p)
  in forall (j :: kk d c) (f :: kk d c) (g :: kk d d).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> Lift j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> Lift j f ~> g
liftUniv @p @p (forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @_ @p @(Lift p p) @(Lift p p) (O (O p (Lift p p)) (Lift p p) ~> O p (O (Lift p p) (Lift p p)))
-> (p ~> O (O p (Lift p p)) (Lift p p))
-> p ~> O p (O (Lift p p) (Lift p p))
forall (b :: kk d c) (c :: kk d c) (a :: kk d c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (j :: kk d c) (f :: kk d c).
LeftKanLift j f =>
f ~> O j (Lift j f)
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
LeftKanLift j f =>
f ~> O j (Lift j f)
lift @p @p (p ~> O p (Lift p p))
-> Obj (Lift p p)
-> O p (Lift p p) ~> O (O p (Lift p p)) (Lift p p)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj (Lift p p)
lpp) (O p (Lift p p) ~> O (O p (Lift p p)) (Lift p p))
-> (p ~> O p (Lift p p)) -> p ~> O (O p (Lift p p)) (Lift p p)
forall (b :: kk d c) (c :: kk d c) (a :: kk d c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk d c) (f :: kk d c).
LeftKanLift j f =>
f ~> O j (Lift j f)
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
LeftKanLift j f =>
f ~> O j (Lift j f)
lift @p @p)
      ((Ob (O (Lift p p) (Lift p p)), Ob (O (Lift p p) (Lift p p))) =>
 Lift p p ~> O (Lift p p) (Lift p p))
-> (O (Lift p p) (Lift p p) ~> O (Lift p p) (Lift p p))
-> Lift p p ~> O (Lift p p) (Lift p p)
forall (a :: kk d d) (b :: kk d d) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Obj (Lift p p)
lpp Obj (Lift p p)
-> Obj (Lift p p)
-> O (Lift p p) (Lift p p) ~> O (Lift p p) (Lift p p)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj (Lift p p)
lpp)

idLift :: forall f. (LeftKanLift I f, Ob f) => f ~> Lift I f
idLift :: forall {s} {kk :: CAT s} {e :: s} {d :: s} (f :: kk e d).
(LeftKanLift I f, Ob f) =>
f ~> Lift I f
idLift = O I (Lift I f) ~> Lift I f
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
leftUnitor (O I (Lift I f) ~> Lift I f)
-> (f ~> O I (Lift I f)) -> f ~> Lift I f
forall (b :: kk e d) (c :: kk e d) (a :: kk e d).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk d d) (f :: kk e d).
LeftKanLift j f =>
f ~> O j (Lift j f)
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
LeftKanLift j f =>
f ~> O j (Lift j f)
lift @I @f

liftAlongConjoint
  :: forall {i} {k} hk vk (j :: vk i k) f
   . (LeftKanLift (Conjoint hk j) f, Equipment hk vk)
  => Obj j
  -> Lift (Conjoint hk j) f ~> Companion hk j `O` f
liftAlongConjoint :: forall {s} {i :: s} {i :: s} {k :: s} (hk :: CAT s) (vk :: CAT s)
       (j :: vk i k) (f :: hk i i).
(LeftKanLift (Conjoint hk j) f, Equipment hk vk) =>
Obj j -> Lift (Conjoint hk j) f ~> O (Companion hk j) f
liftAlongConjoint Obj j
j =
  let f :: Obj f
f = forall (a :: hk i i). (CategoryOf (hk i i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f; comJ :: Companion hk j ~> Companion hk j
comJ = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj j
j
  in forall (j :: hk k i) (f :: hk i i) (g :: hk i k).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> Lift j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> Lift j f ~> g
liftUniv @(Conjoint hk j) @f
      (forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @_ @(Conjoint hk j) @(Companion hk j) @f (O (O (Conjoint hk j) (Companion hk j)) f
 ~> O (Conjoint hk j) (O (Companion hk j) f))
-> (f ~> O (O (Conjoint hk j) (Companion hk j)) f)
-> f ~> O (Conjoint hk j) (O (Companion hk j) f)
forall (b :: hk i i) (c :: hk i i) (a :: hk i i).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj j -> I ~> O (Conjoint hk j) (Companion hk j)
forall {j :: s} {k :: s} (f :: vk j k).
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
comConUnit Obj j
j (I ~> O (Conjoint hk j) (Companion hk j))
-> Obj f -> O I f ~> O (O (Conjoint hk j) (Companion hk j)) f
forall {i :: s} (j :: s) (k :: s) (a :: hk j k) (b :: hk j k)
       (c :: hk i j) (d :: hk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj f
f) (O I f ~> O (O (Conjoint hk j) (Companion hk j)) f)
-> (f ~> O I f) -> f ~> O (O (Conjoint hk j) (Companion hk j)) f
forall (b :: hk i i) (c :: hk i i) (a :: hk i i).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. f ~> O I f
forall {i :: s} {j :: s} (a :: hk i j).
(Ob0 hk i, Ob0 hk j, Ob a) =>
a ~> O I a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
leftUnitorInv)
      ((Ob (O (Companion hk j) f), Ob (O (Companion hk j) f)) =>
 Lift (Conjoint hk j) f ~> O (Companion hk j) f)
-> (O (Companion hk j) f ~> O (Companion hk j) f)
-> Lift (Conjoint hk j) f ~> O (Companion hk j) f
forall (a :: hk i k) (b :: hk i k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Companion hk j ~> Companion hk j
comJ (Companion hk j ~> Companion hk j)
-> Obj f -> O (Companion hk j) f ~> O (Companion hk j) f
forall {i :: s} (j :: s) (k :: s) (a :: hk j k) (b :: hk j k)
       (c :: hk i j) (d :: hk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj f
f)
      ((Ob (Companion hk j), Ob (Companion hk j)) =>
 Lift (Conjoint hk j) f ~> O (Companion hk j) f)
-> (Companion hk j ~> Companion hk j)
-> Lift (Conjoint hk j) f ~> O (Companion hk j) f
forall (a :: hk i k) (b :: hk i k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Companion hk j ~> Companion hk j
comJ

liftAlongConjointInv
  :: forall {i} {k} hk vk (j :: vk i k) f
   . (LeftKanLift (Conjoint hk j) f, Equipment hk vk)
  => Obj j
  -> Companion hk j `O` f ~> Lift (Conjoint hk j) f
liftAlongConjointInv :: forall {k} {e :: k} {i :: k} {k :: k} (hk :: CAT k) (vk :: CAT k)
       (j :: vk i k) (f :: hk e i).
(LeftKanLift (Conjoint hk j) f, Equipment hk vk) =>
Obj j -> O (Companion hk j) f ~> Lift (Conjoint hk j) f
liftAlongConjointInv Obj j
j = forall (f :: vk i k) (p :: hk e i) (q :: hk e k).
(Equipment hk vk, Ob q) =>
Obj f -> (p ~> O (Conjoint hk f) q) -> O (Companion hk f) p ~> q
forall {s} {i :: s} {j :: s} {k :: s} {hk :: CAT s} {vk :: CAT s}
       (f :: vk j k) (p :: hk i j) (q :: hk i k).
(Equipment hk vk, Ob q) =>
Obj f -> (p ~> O (Conjoint hk f) q) -> O (Companion hk f) p ~> q
flipCompanionInv @j @f @(Lift (Conjoint hk j) f) Obj j
j (forall (j :: hk k i) (f :: hk e i).
LeftKanLift j f =>
f ~> O j (Lift j f)
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
LeftKanLift j f =>
f ~> O j (Lift j f)
lift @(Conjoint hk j))

type f <| j = Rift j f
type RightKanLift :: forall {k} {kk :: CAT k} {c} {d} {e}. kk d c -> kk e c -> Constraint
class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Rift j f)) => RightKanLift (j :: kk d c) (f :: kk e c) where
  type Rift j f :: kk e d
  rift :: j `O` Rift j f ~> f
  riftUniv :: (Ob g) => (j `O` g ~> f) -> g ~> Rift j f

mapRift :: forall j f g. (RightKanLift j f, RightKanLift j g) => (f ~> g) -> Rift j f ~> Rift j g
mapRift :: forall {k} {kk :: CAT k} {d :: k} {c :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e c).
(RightKanLift j f, RightKanLift j g) =>
(f ~> g) -> Rift j f ~> Rift j g
mapRift f ~> g
fg = forall (j :: kk d c) (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
riftUniv @j (f ~> g
fg (f ~> g) -> (O j (Rift j f) ~> f) -> O j (Rift j f) ~> g
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk d c) (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
rift @j)

rebaseRift :: forall f i j. (RightKanLift j f, RightKanLift i f) => (i ~> j) -> Rift j f ~> Rift i f
rebaseRift :: forall {k} {kk :: CAT k} {e :: k} {c :: k} {d :: k} (f :: kk e c)
       (i :: kk d c) (j :: kk d c).
(RightKanLift j f, RightKanLift i f) =>
(i ~> j) -> Rift j f ~> Rift i f
rebaseRift i ~> j
ij = forall (j :: kk d c) (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
riftUniv @i (forall (j :: kk d c) (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
rift @j @f (O j (Rift j f) ~> f)
-> (O i (Rift j f) ~> O j (Rift j f)) -> O i (Rift j f) ~> f
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (i ~> j
ij (i ~> j)
-> (Rift j f ~> Rift j f) -> O i (Rift j f) ~> O j (Rift j f)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk e d). (CategoryOf (kk e d), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Rift j f)))

dimapRift :: forall i j f g. (RightKanLift j f, RightKanLift i g) => (i ~> j) -> (f ~> g) -> (Rift j f ~> Rift i g)
dimapRift :: forall {k} {kk :: CAT k} {d :: k} {c :: k} {e :: k} (i :: kk d c)
       (j :: kk d c) (f :: kk e c) (g :: kk e c).
(RightKanLift j f, RightKanLift i g) =>
(i ~> j) -> (f ~> g) -> Rift j f ~> Rift i g
dimapRift i ~> j
ij f ~> g
fg = forall (j :: kk d c) (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
riftUniv @i (f ~> g
fg (f ~> g) -> (O i (Rift j f) ~> f) -> O i (Rift j f) ~> g
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk d c) (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
rift @j (O j (Rift j f) ~> f)
-> (O i (Rift j f) ~> O j (Rift j f)) -> O i (Rift j f) ~> f
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (i ~> j
ij (i ~> j)
-> (Rift j f ~> Rift j f) -> O i (Rift j f) ~> O j (Rift j f)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk e d). (CategoryOf (kk e d), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Rift j f))) ((Ob i, Ob j) => Rift j f ~> Rift i g)
-> (i ~> j) -> Rift j f ~> Rift i g
forall (a :: kk d c) (b :: kk d c) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ i ~> j
ij

riftMonadEta :: forall {kk} {c} {d} (p :: kk d c). (RightKanLift p p) => I ~> Rift p p
riftMonadEta :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} (p :: kk d c).
RightKanLift p p =>
I ~> Rift p p
riftMonadEta = forall (j :: kk d c) (f :: kk d c) (g :: kk d d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
riftUniv @p @p O p I ~> p
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
rightUnitor

riftMonadMu :: forall {kk} {c} {d} (p :: kk d c). (RightKanLift p p) => Rift p p `O` Rift p p ~> Rift p p
riftMonadMu :: forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (p :: kk d c).
RightKanLift p p =>
O (Rift p p) (Rift p p) ~> Rift p p
riftMonadMu =
  let rpp :: Obj (Rift p p)
rpp = forall (a :: kk d d). (CategoryOf (kk d d), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Rift p p)
  in forall (j :: kk d c) (f :: kk d c) (g :: kk d d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
riftUniv @p @p (forall (j :: kk d c) (f :: kk d c).
RightKanLift j f =>
O j (Rift j f) ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
rift @p @p (O p (Rift p p) ~> p)
-> (O p (O (Rift p p) (Rift p p)) ~> O p (Rift p p))
-> O p (O (Rift p p) (Rift p p)) ~> p
forall (b :: kk d c) (c :: kk d c) (a :: kk d c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (j :: kk d c) (f :: kk d c).
RightKanLift j f =>
O j (Rift j f) ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
rift @p @p (O p (Rift p p) ~> p)
-> Obj (Rift p p)
-> O (O p (Rift p p)) (Rift p p) ~> O p (Rift p p)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj (Rift p p)
rpp) (O (O p (Rift p p)) (Rift p p) ~> O p (Rift p p))
-> (O p (O (Rift p p) (Rift p p)) ~> O (O p (Rift p p)) (Rift p p))
-> O p (O (Rift p p) (Rift p p)) ~> O p (Rift p p)
forall (b :: kk d c) (c :: kk d c) (a :: kk d c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @_ @p @(Rift p p) @(Rift p p))
      ((Ob (O (Rift p p) (Rift p p)), Ob (O (Rift p p) (Rift p p))) =>
 O (Rift p p) (Rift p p) ~> Rift p p)
-> (O (Rift p p) (Rift p p) ~> O (Rift p p) (Rift p p))
-> O (Rift p p) (Rift p p) ~> Rift p p
forall (a :: kk d d) (b :: kk d d) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Obj (Rift p p)
rpp Obj (Rift p p)
-> Obj (Rift p p)
-> O (Rift p p) (Rift p p) ~> O (Rift p p) (Rift p p)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj (Rift p p)
rpp)

composeRift
  :: forall i j f
   . (RightKanLift j f, RightKanLift i (Rift j f), RightKanLift (j `O` i) f)
  => Rift i (Rift j f) ~> Rift (j `O` i) f
composeRift :: forall {k} {kk :: CAT k} {d :: k} {j :: k} {c :: k} {e :: k}
       (i :: kk d j) (j :: kk j c) (f :: kk e c).
(RightKanLift j f, RightKanLift i (Rift j f),
 RightKanLift (O j i) f) =>
Rift i (Rift j f) ~> Rift (O j i) f
composeRift =
  forall (j :: kk d c) (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
riftUniv @(j `O` i) @f
    (forall (j :: kk j c) (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
rift @j @f (O j (Rift j f) ~> f)
-> (O (O j i) (Rift i (Rift j f)) ~> O j (Rift j f))
-> O (O j i) (Rift i (Rift j f)) ~> f
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: kk j c). (CategoryOf (kk j c), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j Obj j
-> (O i (Rift i (Rift j f)) ~> Rift j f)
-> O j (O i (Rift i (Rift j f))) ~> O j (Rift j f)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (j :: kk d j) (f :: kk e j).
RightKanLift j f =>
O j (Rift j f) ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
rift @i @(Rift j f)) (O j (O i (Rift i (Rift j f))) ~> O j (Rift j f))
-> (O (O j i) (Rift i (Rift j f)) ~> O j (O i (Rift i (Rift j f))))
-> O (O j i) (Rift i (Rift j f)) ~> O j (Rift j f)
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @_ @j @i @(Rift i (Rift j f)))

idRift :: forall f. (RightKanLift I f, Ob f) => f ~> Rift I f
idRift :: forall {s} {kk :: CAT s} {e :: s} {d :: s} (f :: kk e d).
(RightKanLift I f, Ob f) =>
f ~> Rift I f
idRift = forall (j :: kk d d) (f :: kk e d) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
riftUniv @I @f O I f ~> f
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
leftUnitor

riftAlongCompanion
  :: forall {i} {k} hk vk (j :: vk i k) f
   . (RightKanLift (Companion hk j) f, Equipment hk vk)
  => Obj j
  -> Rift (Companion hk j) f ~> Conjoint hk j `O` f
riftAlongCompanion :: forall {s} {i :: s} {i :: s} {k :: s} (hk :: CAT s) (vk :: CAT s)
       (j :: vk i k) (f :: hk i k).
(RightKanLift (Companion hk j) f, Equipment hk vk) =>
Obj j -> Rift (Companion hk j) f ~> O (Conjoint hk j) f
riftAlongCompanion Obj j
j = forall (f :: vk i k) (p :: hk i i) (q :: hk i k).
(Equipment hk vk, Ob p) =>
Obj f -> (O (Companion hk f) p ~> q) -> p ~> O (Conjoint hk f) q
forall {s} {i :: s} {j :: s} {k :: s} {hk :: CAT s} {vk :: CAT s}
       (f :: vk j k) (p :: hk i j) (q :: hk i k).
(Equipment hk vk, Ob p) =>
Obj f -> (O (Companion hk f) p ~> q) -> p ~> O (Conjoint hk f) q
flipCompanion @j @(Rift (Companion hk j) f) @f Obj j
j (forall (j :: hk i k) (f :: hk i k).
RightKanLift j f =>
O j (Rift j f) ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
rift @(Companion hk j))

riftAlongCompanionInv
  :: forall {i} {k} hk vk (j :: vk i k) f
   . (RightKanLift (Companion hk j) f, Equipment hk vk)
  => Obj j
  -> Conjoint hk j `O` f ~> Rift (Companion hk j) f
riftAlongCompanionInv :: forall {k} {e :: k} {i :: k} {k :: k} (hk :: CAT k) (vk :: CAT k)
       (j :: vk i k) (f :: hk e k).
(RightKanLift (Companion hk j) f, Equipment hk vk) =>
Obj j -> O (Conjoint hk j) f ~> Rift (Companion hk j) f
riftAlongCompanionInv Obj j
j =
  let f :: Obj f
f = forall (a :: hk e k). (CategoryOf (hk e k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f; conJ :: Conjoint hk j ~> Conjoint hk j
conJ = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk Obj j
j
  in forall (j :: hk i k) (f :: hk e k) (g :: hk e i).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> f) -> g ~> Rift j f
riftUniv @(Companion hk j) @f
      (O I f ~> f
forall {i :: k} {j :: k} (a :: hk i j).
(Ob0 hk i, Ob0 hk j, Ob a) =>
O I a ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
leftUnitor (O I f ~> f)
-> (O (Companion hk j) (O (Conjoint hk j) f) ~> O I f)
-> O (Companion hk j) (O (Conjoint hk j) f) ~> f
forall (b :: hk e k) (c :: hk e k) (a :: hk e k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj j -> O (Companion hk j) (Conjoint hk j) ~> I
forall {j :: k} {k :: k} (f :: vk j k).
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
comConCounit Obj j
j (O (Companion hk j) (Conjoint hk j) ~> I)
-> Obj f -> O (O (Companion hk j) (Conjoint hk j)) f ~> O I f
forall {i :: k} (j :: k) (k :: k) (a :: hk j k) (b :: hk j k)
       (c :: hk i j) (d :: hk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj f
f) (O (O (Companion hk j) (Conjoint hk j)) f ~> O I f)
-> (O (Companion hk j) (O (Conjoint hk j) f)
    ~> O (O (Companion hk j) (Conjoint hk j)) f)
-> O (Companion hk j) (O (Conjoint hk j) f) ~> O I f
forall (b :: hk e k) (c :: hk e k) (a :: hk e k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @_ @(Companion hk j) @(Conjoint hk j) @f)
      ((Ob (O (Conjoint hk j) f), Ob (O (Conjoint hk j) f)) =>
 O (Conjoint hk j) f ~> Rift (Companion hk j) f)
-> (O (Conjoint hk j) f ~> O (Conjoint hk j) f)
-> O (Conjoint hk j) f ~> Rift (Companion hk j) f
forall (a :: hk e i) (b :: hk e i) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Conjoint hk j ~> Conjoint hk j
conJ (Conjoint hk j ~> Conjoint hk j)
-> Obj f -> O (Conjoint hk j) f ~> O (Conjoint hk j) f
forall {i :: k} (j :: k) (k :: k) (a :: hk j k) (b :: hk j k)
       (c :: hk i j) (d :: hk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj f
f)
      ((Ob (Conjoint hk j), Ob (Conjoint hk j)) =>
 O (Conjoint hk j) f ~> Rift (Companion hk j) f)
-> (Conjoint hk j ~> Conjoint hk j)
-> O (Conjoint hk j) f ~> Rift (Companion hk j) f
forall (a :: hk k i) (b :: hk k i) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Conjoint hk j ~> Conjoint hk j
conJ