{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Monoidal.Endo where


import Proarrow.Core (Promonad(..), CategoryOf(..), Profunctor(..), UN, Is, CAT, dimapDefault)
import Proarrow.Category.Bicategory (Bicategory(..), Monad(..), Comonad(..))
import Proarrow.Category.Bicategory qualified as B
import Proarrow.Category.Monoidal (Monoidal(..))
import Proarrow.Monoid (Monoid(..), Comonoid(..))


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

-- | 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)
  Endo p ~> q
f par :: forall (a :: ENDO kk k) (b :: ENDO kk k) (c :: ENDO kk k)
       (d :: ENDO kk k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`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 {k1 :: j} (i :: j) (j :: j) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` p ~> q
g)
  leftUnitor :: forall (a :: ENDO kk k). Obj a -> (Unit ** a) ~> a
leftUnitor (Endo p ~> q
p) = (O I q ~> q) -> Endo (E (O I q)) (E 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 (Obj q -> O I q ~> q
forall (i :: j) (j :: j) (a :: kk i j). Obj a -> O I a ~> a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> O I a ~> a
B.leftUnitor p ~> q
Obj q
p)
  leftUnitorInv :: forall (a :: ENDO kk k). Obj a -> a ~> (Unit ** a)
leftUnitorInv (Endo p ~> q
p) = (q ~> O I q) -> Endo (E q) (E (O I 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 (Obj q -> q ~> O I q
forall (i :: j) (j :: j) (a :: kk i j). Obj a -> a ~> O I a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> a ~> O I a
B.leftUnitorInv p ~> q
Obj q
p)
  rightUnitor :: forall (a :: ENDO kk k). Obj a -> (a ** Unit) ~> a
rightUnitor (Endo p ~> q
p) = (O q I ~> q) -> Endo (E (O q I)) (E 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 (Obj q -> O q I ~> q
forall (i :: j) (j :: j) (a :: kk i j). Obj a -> O a I ~> a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> O a I ~> a
B.rightUnitor p ~> q
Obj q
p)
  rightUnitorInv :: forall (a :: ENDO kk k). Obj a -> a ~> (a ** Unit)
rightUnitorInv (Endo p ~> q
p) = (q ~> O q I) -> Endo (E q) (E (O q 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 (Obj q -> q ~> O q I
forall (i :: j) (j :: j) (a :: kk i j). Obj a -> a ~> O a I
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> a ~> O a I
B.rightUnitorInv p ~> q
Obj q
p)
  associator :: forall (a :: ENDO kk k) (b :: ENDO kk k) (c :: ENDO kk k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator (Endo p ~> q
p) (Endo p ~> q
q) (Endo p ~> q
r) = (O (O q q) q ~> O q (O q q))
-> Endo (E (O (O q q) q)) (E (O q (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 (Obj q -> Obj q -> Obj q -> O (O q q) q ~> O q (O q q)
forall {j1 :: j} {k1 :: j} (i :: j) (j2 :: j) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
B.associator p ~> q
Obj q
p p ~> q
Obj q
q p ~> q
Obj q
r)
  associatorInv :: forall (a :: ENDO kk k) (b :: ENDO kk k) (c :: ENDO kk k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv (Endo p ~> q
p) (Endo p ~> q
q) (Endo p ~> q
r) = (O q (O q q) ~> O (O q q) q)
-> Endo (E (O q (O q q))) (E (O (O q 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 (Obj q -> Obj q -> Obj q -> O q (O q q) ~> O (O q q) q
forall {j1 :: j} {k1 :: j} (i :: j) (j2 :: j) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
B.associatorInv p ~> q
Obj q
p p ~> q
Obj q
q p ~> q
Obj q
r)

-- | Monads are monoids in the category of endo-1-cells.
instance (Bicategory kk, Monad 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, Comonad 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