{-# 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 (RightKanExtension (..), dimapRan)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Monoid (Comonoid (..), Monoid (..))
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) => 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 (i :: j). Ob0 kk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
  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) => Monoidal (ENDO kk k) where
  type Unit = E I
  type E p ** E q = E (p `O` q)
  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

-- | 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