{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Endo where

import Proarrow.Category.Bicategory (Bicategory (..), Comonad (..), Monad (..))
import Proarrow.Category.Bicategory qualified as B
import Proarrow.Category.Bicategory.Kan (LeftKanExtension (..), RightKanExtension (..), dimapRan)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, obj)
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Object.Coexponential (Coclosed (..))
import Proarrow.Object.Exponential (Closed (..))

type data ENDO (kk :: CAT j) (k :: j) = E (kk k k)
type instance UN E (E p) = p

type Endo :: forall {kk} {k}. CAT (ENDO kk k)
data Endo p q where
  Endo :: p ~> q -> Endo (E p) (E q)

mkEndo :: (CategoryOf (kk k k)) => (p :: kk k k) ~> q -> Endo (E p) (E q)
mkEndo :: forall {j} (kk :: j -> j -> Type) (k :: j) (p :: kk k k)
       (q :: kk k k).
CategoryOf (kk k k) =>
(p ~> q) -> Endo (E p) (E q)
mkEndo p ~> q
pq = (p ~> q) -> Endo (E p) (E q)
forall {j} {kk :: CAT j} {k :: j} (p :: kk k k) (q :: kk k k).
(p ~> q) -> Endo (E p) (E q)
Endo p ~> q
pq ((Ob p, Ob q) => Endo (E p) (E q)) -> (p ~> q) -> Endo (E p) (E q)
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
pq

instance (Bicategory kk, Ob0 kk k) => Profunctor (Endo :: CAT (ENDO kk k)) where
  dimap :: forall (c :: ENDO kk k) (a :: ENDO kk k) (b :: ENDO kk k)
       (d :: ENDO kk k).
(c ~> a) -> (b ~> d) -> Endo a b -> Endo c d
dimap = (c ~> a) -> (b ~> d) -> Endo a b -> Endo c d
Endo c a -> Endo b d -> Endo a b -> Endo c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: ENDO kk k) (b :: ENDO kk k) r.
((Ob a, Ob b) => r) -> Endo a b -> r
\\ Endo p ~> q
f = r
(Ob p, Ob q) => r
(Ob a, Ob b) => r
r ((Ob p, Ob q) => r) -> (p ~> q) -> r
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
f
instance (Bicategory kk, Ob0 kk k) => Promonad (Endo :: CAT (ENDO kk k)) where
  id :: forall (a :: ENDO kk k). Ob a => Endo a a
id = (UN E a ~> UN E a) -> Endo (E (UN E a)) (E (UN E a))
forall {j} {kk :: CAT j} {k :: j} (p :: kk k k) (q :: kk k k).
(p ~> q) -> Endo (E p) (E q)
Endo UN E a ~> UN E a
forall (a :: kk k k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Endo p ~> q
m . :: forall (b :: ENDO kk k) (c :: ENDO kk k) (a :: ENDO kk k).
Endo b c -> Endo a b -> Endo a c
. Endo p ~> q
n = (p ~> q) -> Endo (E p) (E q)
forall {j} {kk :: CAT j} {k :: j} (p :: kk k k) (q :: kk k k).
(p ~> q) -> Endo (E p) (E q)
Endo (p ~> q
m (p ~> q) -> (p ~> p) -> p ~> q
forall (b :: kk k k) (c :: kk k k) (a :: kk k k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p ~> p
p ~> q
n)
instance (Bicategory kk, Ob0 kk k) => CategoryOf (ENDO kk k) where
  type (~>) = Endo
  type Ob p = (Is E p, Ob (UN E p))

instance (Bicategory kk, Ob0 kk k, (Ob (I :: kk k k))) => MonoidalProfunctor (Endo :: CAT (ENDO kk k)) where
  par0 :: Endo Unit Unit
par0 = (I ~> I) -> Endo (E I) (E I)
forall {j} {kk :: CAT j} {k :: j} (p :: kk k k) (q :: kk k k).
(p ~> q) -> Endo (E p) (E q)
Endo I ~> I
forall (a :: kk k k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Endo p ~> q
f par :: forall (x1 :: ENDO kk k) (x2 :: ENDO kk k) (y1 :: ENDO kk k)
       (y2 :: ENDO kk k).
Endo x1 x2 -> Endo y1 y2 -> Endo (x1 ** y1) (x2 ** y2)
`par` Endo p ~> q
g = (O p p ~> O q q) -> Endo (E (O p p)) (E (O q q))
forall {j} (kk :: j -> j -> Type) (k :: j) (p :: kk k k)
       (q :: kk k k).
CategoryOf (kk k k) =>
(p ~> q) -> Endo (E p) (E q)
mkEndo (p ~> q
f (p ~> q) -> (p ~> q) -> O p p ~> O q q
forall {i :: j} (j :: j) (k :: j) (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` p ~> q
g)

-- | The monoidal subcategory of a bicategory for a single object.
instance (Bicategory kk, Ob0 kk k, (Ob (I :: kk k k))) => Monoidal (ENDO kk k) where
  type Unit = E I
  type E p ** E q = E (p `O` q)
  withOb2 :: forall (a :: ENDO kk k) (b :: ENDO kk k) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(E a) @(E b) Ob (a ** b) => r
r = r
Ob (a ** b) => r
(Ob0 kk k, Ob0 kk k, Ob (O (UN E a) (UN E b)),
 Ob (O (UN E a) (UN E b))) =>
r
r ((Ob0 kk k, Ob0 kk k, Ob (O (UN E a) (UN E b)),
  Ob (O (UN E a) (UN E b))) =>
 r)
-> (O (UN E a) (UN E b) ~> O (UN E a) (UN E b)) -> r
forall (i :: j) (j :: j) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ (forall (a :: kk k k). (CategoryOf (kk k k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj (UN E a)
-> (UN E b ~> UN E b) -> O (UN E a) (UN E b) ~> O (UN E a) (UN E b)
forall {i :: j} (j :: j) (k :: j) (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 k k). (CategoryOf (kk k k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)
  leftUnitor :: forall (a :: ENDO kk k). Ob a => (Unit ** a) ~> a
leftUnitor = (O I (UN E a) ~> UN E a) -> Endo (E (O I (UN E a))) (E (UN E a))
forall {j} (kk :: j -> j -> Type) (k :: j) (p :: kk k k)
       (q :: kk k k).
CategoryOf (kk k k) =>
(p ~> q) -> Endo (E p) (E q)
mkEndo O I (UN E a) ~> UN E a
forall {i :: j} {j :: j} (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
B.leftUnitor
  leftUnitorInv :: forall (a :: ENDO kk k). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN E a ~> O I (UN E a)) -> Endo (E (UN E a)) (E (O I (UN E a)))
forall {j} (kk :: j -> j -> Type) (k :: j) (p :: kk k k)
       (q :: kk k k).
CategoryOf (kk k k) =>
(p ~> q) -> Endo (E p) (E q)
mkEndo UN E a ~> O I (UN E a)
forall {i :: j} {j :: j} (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
B.leftUnitorInv
  rightUnitor :: forall (a :: ENDO kk k). Ob a => (a ** Unit) ~> a
rightUnitor = (O (UN E a) I ~> UN E a) -> Endo (E (O (UN E a) I)) (E (UN E a))
forall {j} (kk :: j -> j -> Type) (k :: j) (p :: kk k k)
       (q :: kk k k).
CategoryOf (kk k k) =>
(p ~> q) -> Endo (E p) (E q)
mkEndo O (UN E a) I ~> UN E a
forall {i :: j} {j :: j} (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
B.rightUnitor
  rightUnitorInv :: forall (a :: ENDO kk k). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN E a ~> O (UN E a) I) -> Endo (E (UN E a)) (E (O (UN E a) I))
forall {j} (kk :: j -> j -> Type) (k :: j) (p :: kk k k)
       (q :: kk k k).
CategoryOf (kk k k) =>
(p ~> q) -> Endo (E p) (E q)
mkEndo UN E a ~> O (UN E a) I
forall {i :: j} {j :: j} (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
B.rightUnitorInv
  associator :: forall (a :: ENDO kk k) (b :: ENDO kk k) (c :: ENDO kk k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(E p) @(E q) @(E r) = (O (O (UN E a) (UN E b)) (UN E c)
 ~> O (UN E a) (O (UN E b) (UN E c)))
-> Endo
     (E (O (O (UN E a) (UN E b)) (UN E c)))
     (E (O (UN E a) (O (UN E b) (UN E c))))
forall {j} (kk :: j -> j -> Type) (k :: j) (p :: kk k k)
       (q :: kk k k).
CategoryOf (kk k k) =>
(p ~> q) -> Endo (E p) (E q)
mkEndo (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 j) {h :: j} {i :: j} {j :: j} {k :: j}
       (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)
B.associator @kk @p @q @r)
  associatorInv :: forall (a :: ENDO kk k) (b :: ENDO kk k) (c :: ENDO kk k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(E p) @(E q) @(E r) = (O (UN E a) (O (UN E b) (UN E c))
 ~> O (O (UN E a) (UN E b)) (UN E c))
-> Endo
     (E (O (UN E a) (O (UN E b) (UN E c))))
     (E (O (O (UN E a) (UN E b)) (UN E c)))
forall {j} (kk :: j -> j -> Type) (k :: j) (p :: kk k k)
       (q :: kk k k).
CategoryOf (kk k k) =>
(p ~> q) -> Endo (E p) (E q)
mkEndo (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 j) {h :: j} {i :: j} {j :: j} {k :: j}
       (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
B.associatorInv @kk @p @q @r)

instance
  (Bicategory kk, Ob0 kk k, Ob (I :: kk k k), forall (f :: kk k k) (g :: kk k k). (Ob f, Ob g) => RightKanExtension f g)
  => Closed (ENDO kk k)
  where
  type E f ~~> E g = E (Ran f g)
  curry' :: forall (a :: ENDO kk k) (b :: ENDO kk k) (c :: ENDO kk k).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' (Endo @g p ~> q
g) (Endo @j p ~> q
j) (Endo p ~> q
h) = (q ~> Ran q q) -> Endo (E q) (E (Ran q q))
forall {j} {kk :: CAT j} {k :: j} (p :: kk k k) (q :: kk k k).
(p ~> q) -> Endo (E p) (E q)
Endo (forall (j :: kk k k) (f :: kk k k) (g :: kk k k).
(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 @_ @g p ~> q
O p p ~> q
h) ((Ob q, Ob q) => Endo (E q) (E (Ran q q)))
-> (q ~> q) -> Endo (E q) (E (Ran q q))
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
q ~> q
g ((Ob q, Ob q) => Endo (E q) (E (Ran q q)))
-> (q ~> q) -> Endo (E q) (E (Ran q q))
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
q ~> q
j ((Ob p, Ob q) => Endo (E q) (E (Ran q q)))
-> (p ~> q) -> Endo (E q) (E (Ran q q))
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
h
  uncurry' :: forall (b :: ENDO kk k) (c :: ENDO kk k) (a :: ENDO kk k).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' (Endo @j p ~> q
j) (Endo @f p ~> q
f) (Endo p ~> q
h) = (O p q ~> q) -> Endo (E (O p q)) (E q)
forall {j} {kk :: CAT j} {k :: j} (p :: kk k k) (q :: kk k k).
(p ~> q) -> Endo (E p) (E q)
Endo (forall (j :: kk k k) (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 (O q q ~> q) -> (O p q ~> O q q) -> O p q ~> q
forall (b :: kk k k) (c :: kk k k) (a :: kk k k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (p ~> q
h (p ~> q) -> (q ~> q) -> O p q ~> O q q
forall {i :: j} (j :: j) (k :: j) (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` p ~> q
q ~> q
j)) ((Ob q, Ob q) => Endo (E (O p q)) (E q))
-> (q ~> q) -> Endo (E (O p q)) (E q)
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
q ~> q
j ((Ob q, Ob q) => Endo (E (O p q)) (E q))
-> (q ~> q) -> Endo (E (O p q)) (E q)
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
q ~> q
f
  ^^^ :: forall (b :: ENDO kk k) (y :: ENDO kk k) (x :: ENDO kk k)
       (a :: ENDO kk k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(^^^) (Endo p ~> q
f) (Endo p ~> q
g) = (Ran q p ~> Ran p q) -> Endo (E (Ran q p)) (E (Ran p q))
forall {j} {kk :: CAT j} {k :: j} (p :: kk k k) (q :: kk k k).
(p ~> q) -> Endo (E p) (E q)
Endo ((p ~> q) -> (p ~> q) -> Ran q p ~> Ran p q
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 p ~> q
g p ~> q
f) ((Ob p, Ob q) => Endo (E (Ran q p)) (E (Ran p q)))
-> (p ~> q) -> Endo (E (Ran q p)) (E (Ran p q))
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
f ((Ob p, Ob q) => Endo (E (Ran q p)) (E (Ran p q)))
-> (p ~> q) -> Endo (E (Ran q p)) (E (Ran p q))
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
g

instance
  (Bicategory kk, Ob0 kk k, Ob (I :: kk k k), forall (f :: kk k k) (g :: kk k k). (Ob f, Ob g) => LeftKanExtension f g)
  => Coclosed (ENDO kk k)
  where
  type E f <~~ E g = E (Lan g f)
  coeval' :: forall (a :: ENDO kk k) (b :: ENDO kk k).
Obj a -> Obj b -> a ~> ((a <~~ b) ** b)
coeval' (Endo @g p ~> q
g) (Endo @j p ~> q
j) = (q ~> O (Lan q q) q) -> Endo (E q) (E (O (Lan q q) q))
forall {j} {kk :: CAT j} {k :: j} (p :: kk k k) (q :: kk k k).
(p ~> q) -> Endo (E p) (E q)
Endo (forall (j :: kk k k) (f :: kk k k).
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) ((Ob q, Ob q) => Endo (E q) (E (O (Lan q q) q)))
-> (q ~> q) -> Endo (E q) (E (O (Lan q q) q))
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
q ~> q
g ((Ob q, Ob q) => Endo (E q) (E (O (Lan q q) q)))
-> (q ~> q) -> Endo (E q) (E (O (Lan q q) q))
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
q ~> q
j
  coevalUniv' :: forall (b :: ENDO kk k) (c :: ENDO kk k) (a :: ENDO kk k).
Obj b -> Obj c -> (a ~> (c ** b)) -> (a <~~ b) ~> c
coevalUniv' (Endo @j p ~> q
j) (Endo @f p ~> q
f) (Endo p ~> q
h) = (Lan q p ~> q) -> Endo (E (Lan q p)) (E q)
forall {j} {kk :: CAT j} {k :: j} (p :: kk k k) (q :: kk k k).
(p ~> q) -> Endo (E p) (E q)
Endo (forall (j :: kk k k) (f :: kk k 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 p ~> q
p ~> O p p
h) ((Ob q, Ob q) => Endo (E (Lan q p)) (E q))
-> (q ~> q) -> Endo (E (Lan q p)) (E q)
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
q ~> q
j ((Ob q, Ob q) => Endo (E (Lan q p)) (E q))
-> (q ~> q) -> Endo (E (Lan q p)) (E q)
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
q ~> q
f ((Ob p, Ob q) => Endo (E (Lan q p)) (E q))
-> (p ~> q) -> Endo (E (Lan q p)) (E q)
forall (a :: kk k k) (b :: kk k k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> q
h

-- | Monads are monoids in the category of endo-1-cells.
instance (Bicategory kk, Ob (I :: kk a a), Monad m, Ob m) => Monoid (E m :: ENDO kk a) where
  mempty :: Unit ~> E m
mempty = (I ~> m) -> Endo (E I) (E m)
forall {j} (kk :: j -> j -> Type) (k :: j) (p :: kk k k)
       (q :: kk k k).
CategoryOf (kk k k) =>
(p ~> q) -> Endo (E p) (E q)
mkEndo I ~> m
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
I ~> t
eta
  mappend :: (E m ** E m) ~> E m
mappend = (O m m ~> m) -> Endo (E (O m m)) (E m)
forall {j} (kk :: j -> j -> Type) (k :: j) (p :: kk k k)
       (q :: kk k k).
CategoryOf (kk k k) =>
(p ~> q) -> Endo (E p) (E q)
mkEndo O m m ~> m
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
O t t ~> t
mu

-- | Comonads are comonoids in the category of endo-1-cells.
instance (Bicategory kk, Ob (I :: kk a a), Comonad c, Ob c) => Comonoid (E c :: ENDO kk a) where
  counit :: E c ~> Unit
counit = (c ~> I) -> Endo (E c) (E I)
forall {j} (kk :: j -> j -> Type) (k :: j) (p :: kk k k)
       (q :: kk k k).
CategoryOf (kk k k) =>
(p ~> q) -> Endo (E p) (E q)
mkEndo c ~> I
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> I
epsilon
  comult :: E c ~> (E c ** E c)
comult = (c ~> O c c) -> Endo (E c) (E (O c c))
forall {j} (kk :: j -> j -> Type) (k :: j) (p :: kk k k)
       (q :: kk k k).
CategoryOf (kk k k) =>
(p ~> q) -> Endo (E p) (E q)
mkEndo c ~> O c c
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> O t t
delta