{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Bicategory.Kan where

import Data.Kind (Constraint)

import Proarrow.Category.Bicategory
  ( Adjunction (..)
  , Bicategory (..)
  , Comonad (..)
  , Monad (..)
  , rightUnitorInvWith
  , rightUnitorWith
  , (==)
  , (||), flipRightAdjointInv, flipRightAdjoint, flipLeftAdjointInv, flipLeftAdjoint
  )

import Proarrow.Core (CAT, CategoryOf (..), Ob, 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

lanAlongLeftAdjoint
  :: forall {i} {k} kk (j :: kk i k) j' f
   . (LeftKanExtension j f, Adjunction j j', Ob j, Ob j')
  => Lan j f ~> f `O` j'
lanAlongLeftAdjoint :: forall {k} {k :: k} {i :: k} {k :: k} (kk :: k -> k -> Type)
       (j :: kk i k) (j' :: kk k i) (f :: kk i k).
(LeftKanExtension j f, Adjunction j j', Ob j, Ob j') =>
Lan j f ~> O f j'
lanAlongLeftAdjoint =
  forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: CAT k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @kk @f @j'
    (forall (j :: kk i k) (f :: kk i k) (g :: kk 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 @j @f (f ~> O f I
forall {i :: k} {j :: k} (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 (f ~> O f I) -> (O f I ~> O f (O j' j)) -> f ~> O f (O j' j)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (a :: kk i k). (CategoryOf (kk i k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f Obj f -> (I ~> O j' j) -> O f I ~> O f (O j' 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
|| forall (l :: kk i k) (r :: kk k i). Adjunction l r => I ~> O r l
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
I ~> O r l
unit @j @j' (f ~> O f (O j' j))
-> (O f (O j' j) ~> O (O f j') j) -> f ~> O (O f j') 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 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 @_ @f @j' @j))

lanAlongLeftAdjointInv
  :: forall {i} {k} kk (j :: kk i k) j' f
   . (LeftKanExtension j f, Adjunction j j', Ob j, Ob j')
  => f `O` j' ~> Lan j f
lanAlongLeftAdjointInv :: forall {k} {e :: k} {i :: k} {k :: k} (kk :: k -> k -> Type)
       (j :: kk i k) (j' :: kk k i) (f :: kk i e).
(LeftKanExtension j f, Adjunction j j', Ob j, Ob j') =>
O f j' ~> Lan j f
lanAlongLeftAdjointInv = forall (l :: kk i k) (r :: kk k i) (a :: kk i e) (b :: kk k e).
(Adjunction l r, Ob b) =>
(a ~> O b l) -> O a r ~> b
forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk c i) (b :: kk d i).
(Adjunction l r, Ob b) =>
(a ~> O b l) -> O a r ~> b
flipRightAdjointInv @j @j' (forall (j :: kk i k) (f :: kk 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 @j @f)

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

ranAlongRightAdjoint
  :: forall {i} {k} kk (j :: kk i k) j' f
   . (RightKanExtension j' f, Adjunction j j', Ob j, Ob j')
  => Ran j' f ~> f `O` j
ranAlongRightAdjoint :: forall {k} {k :: k} {i :: k} {k :: k} (kk :: k -> k -> Type)
       (j :: kk i k) (j' :: kk k i) (f :: kk k k).
(RightKanExtension j' f, Adjunction j j', Ob j, Ob j') =>
Ran j' f ~> O f j
ranAlongRightAdjoint = forall (l :: kk i k) (r :: kk k i) (a :: kk i k) (b :: kk k k).
(Adjunction l r, Ob a) =>
(O a r ~> b) -> a ~> O b l
forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk c i) (b :: kk d i).
(Adjunction l r, Ob a) =>
(O a r ~> b) -> a ~> O b l
flipRightAdjoint @j @j' (forall (j :: kk k i) (f :: kk 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 @j' @f)

ranAlongRightAdjointInv
  :: forall {i} {k} kk (j :: kk i k) j' f
   . (RightKanExtension j' f, Adjunction j j', Ob j, Ob j')
  => f `O` j ~> Ran j' f
ranAlongRightAdjointInv :: forall {k} {e :: k} {i :: k} {k :: k} (kk :: k -> k -> Type)
       (j :: kk i k) (j' :: kk k i) (f :: kk k e).
(RightKanExtension j' f, Adjunction j j', Ob j, Ob j') =>
O f j ~> Ran j' f
ranAlongRightAdjointInv =
  forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: CAT k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @kk @f @j
    (forall (j :: kk k i) (f :: kk k e) (g :: kk 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 @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 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 @j @j' (O (O f j) j' ~> O f (O j j'))
-> (O f (O j j') ~> O f I) -> O (O f j) j' ~> O f I
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (a :: kk k e). (CategoryOf (kk k e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f Obj f -> (O j j' ~> I) -> O f (O j j') ~> O f I
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
|| forall (l :: kk i k) (r :: kk k i). Adjunction l r => O l r ~> I
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
O l r ~> I
counit @j @j' (O (O f j) j' ~> O f I) -> (O f I ~> f) -> O (O f j) j' ~> f
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== O f I ~> f
forall {i :: k} {j :: k} (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))

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

liftAlongRightAdjoint
  :: forall {i} {k} kk (j :: kk i k) j' f
   . (Ob j, Ob j', LeftKanLift j' f, Adjunction j j')
  => Lift j' f ~> j `O` f
liftAlongRightAdjoint :: forall {s} {i :: s} {i :: s} {k :: s} (kk :: s -> s -> Type)
       (j :: kk i k) (j' :: kk k i) (f :: kk i i).
(Ob j, Ob j', LeftKanLift j' f, Adjunction j j') =>
Lift j' f ~> O j f
liftAlongRightAdjoint =
  forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @kk @j @f
    (forall (j :: kk k i) (f :: kk i i) (g :: kk 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 @j' @f (f ~> O I f
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 (f ~> O I f) -> (O I f ~> O (O j' j) f) -> f ~> O (O j' j) f
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (l :: kk i k) (r :: kk k i). Adjunction l r => I ~> O r l
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
I ~> O r l
unit @j @j' (I ~> O j' j) -> (f ~> f) -> O I f ~> O (O j' j) f
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
|| forall (a :: kk i i). (CategoryOf (kk i i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f (f ~> O (O j' j) f)
-> (O (O j' j) f ~> O j' (O j f)) -> f ~> O j' (O j f)
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 (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 @_ @j' @j @f))

liftAlongRightAdjointInv
  :: forall {i} {k} kk (j :: kk i k) j' f
   . (Ob j, Ob j', LeftKanLift j' f, Adjunction j j')
  => j `O` f ~> Lift j' f
liftAlongRightAdjointInv :: forall {k} {e :: k} {i :: k} {k :: k} (kk :: k -> k -> Type)
       (j :: kk i k) (j' :: kk k i) (f :: kk e i).
(Ob j, Ob j', LeftKanLift j' f, Adjunction j j') =>
O j f ~> Lift j' f
liftAlongRightAdjointInv = forall (l :: kk i k) (r :: kk k i) (a :: kk e i) (b :: kk e k).
(Adjunction l r, Ob b) =>
(a ~> O r b) -> O l a ~> b
forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d).
(Adjunction l r, Ob b) =>
(a ~> O r b) -> O l a ~> b
flipLeftAdjointInv @j @j' (forall (j :: kk k i) (f :: kk 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 @j' @f)

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

riftAlongLeftAdjoint
  :: forall {i} {k} kk (j :: kk i k) j' f
   . (RightKanLift j f, Adjunction j j', Ob j, Ob j')
  => Rift j f ~> j' `O` f
riftAlongLeftAdjoint :: forall {s} {i :: s} {i :: s} {k :: s} (kk :: s -> s -> Type)
       (j :: kk i k) (j' :: kk k i) (f :: kk i k).
(RightKanLift j f, Adjunction j j', Ob j, Ob j') =>
Rift j f ~> O j' f
riftAlongLeftAdjoint = forall (l :: kk i k) (r :: kk k i) (a :: kk i i) (b :: kk i k).
(Adjunction l r, Ob a) =>
(O l a ~> b) -> a ~> O r b
forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d).
(Adjunction l r, Ob a) =>
(O l a ~> b) -> a ~> O r b
flipLeftAdjoint @j @j' (forall (j :: kk i k) (f :: kk 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 @j @f)

riftAlongLeftAdjointInv
  :: forall {i} {k} kk (j :: kk i k) j' f
   . (RightKanLift j f, Adjunction j j', Ob j, Ob j')
  => j' `O` f ~> Rift j f
riftAlongLeftAdjointInv :: forall {k} {e :: k} {i :: k} {k :: k} (kk :: k -> k -> Type)
       (j :: kk i k) (j' :: kk k i) (f :: kk e k).
(RightKanLift j f, Adjunction j j', Ob j, Ob j') =>
O j' f ~> Rift j f
riftAlongLeftAdjointInv =
  forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: CAT k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @kk @j' @f
    (forall (j :: kk i k) (f :: kk e k) (g :: kk 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 @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 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 @_ @j @j' @f (O j (O j' f) ~> O (O j j') f)
-> (O (O j j') f ~> O I f) -> O j (O j' f) ~> O I f
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (l :: kk i k) (r :: kk k i). Adjunction l r => O l r ~> I
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
O l r ~> I
counit @j @j' (O j j' ~> I) -> (f ~> f) -> O (O j j') f ~> O I f
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
|| forall (a :: kk e k). (CategoryOf (kk e k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f (O j (O j' f) ~> O I f) -> (O I f ~> f) -> O j (O j' f) ~> f
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== O I f ~> f
forall {i :: k} {j :: k} (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))