{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Enriched where

import Data.Kind (Constraint, Type)
import Prelude (($))

import Proarrow.Core (Promonad(..), CategoryOf(..), CAT, UN, Is, Kind)
import Proarrow.Category.Bicategory (Bicategory(O, I), Monad(..))
import Proarrow.Category.Bicategory.MonoidalAsBi (Mon2(..), MonK(..))
import Proarrow.Object.BinaryProduct ()


type family V (vk :: k -> Type) :: CAT k
type family Arr (v :: CAT k) (a :: vk exta) (b :: vk extb) :: v exta extb
type (a :: vk exta) %~> (b :: vk extb) = Arr (V vk) a b

class (Bicategory (V vk)) => ECategory (vk :: k -> Type) where
  type EOb (a :: vk exta) :: Constraint
  eid :: EOb (a :: vk exta) => I ~> a %~> a
  ecomp :: (EOb (a :: vk exta), EOb (b :: vk extb), EOb (c :: vk extc))
        => ((a :: vk exta) %~> b) `O` (b %~> c) ~> a %~> c


type CATK :: Kind -> () -> Kind
data CATK k ext where
  CK :: k -> CATK k i
type instance UN CK (CK a) = a

type instance V (CATK k) = MonK Type
type instance Arr (MonK Type) (CK a) (CK b) = MK (a ~> b)

-- | A regular category as a Type-enriched category
instance CategoryOf k => ECategory (CATK k) where
  type EOb (a :: CATK k exta) = (Is CK a, Ob (UN CK a))
  eid :: forall (exta :: ()) (a :: CATK k exta). EOb a => I ~> (a %~> a)
eid = (() ~> (UN 'CK a ~> UN 'CK a))
-> Mon2 ('MK ()) ('MK (UN 'CK a ~> UN 'CK a))
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 ((() ~> (UN 'CK a ~> UN 'CK a))
 -> Mon2 ('MK ()) ('MK (UN 'CK a ~> UN 'CK a)))
-> (() ~> (UN 'CK a ~> UN 'CK a))
-> Mon2 ('MK ()) ('MK (UN 'CK a ~> UN 'CK a))
forall a b. (a -> b) -> a -> b
$ \() -> UN 'CK a ~> UN 'CK a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  ecomp :: forall (exta :: ()) (a :: CATK k exta) (extb :: ())
       (b :: CATK k extb) (extc :: ()) (c :: CATK k extc).
(EOb a, EOb b, EOb c) =>
O (a %~> b) (b %~> c) ~> (a %~> c)
ecomp = ((UN 'CK b ~> UN 'CK c, UN 'CK a ~> UN 'CK b)
 ~> (UN 'CK a ~> UN 'CK c))
-> Mon2
     ('MK (UN 'CK b ~> UN 'CK c, UN 'CK a ~> UN 'CK b))
     ('MK (UN 'CK a ~> UN 'CK c))
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 (((UN 'CK b ~> UN 'CK c, UN 'CK a ~> UN 'CK b)
  ~> (UN 'CK a ~> UN 'CK c))
 -> Mon2
      ('MK (UN 'CK b ~> UN 'CK c, UN 'CK a ~> UN 'CK b))
      ('MK (UN 'CK a ~> UN 'CK c)))
-> ((UN 'CK b ~> UN 'CK c, UN 'CK a ~> UN 'CK b)
    ~> (UN 'CK a ~> UN 'CK c))
-> Mon2
     ('MK (UN 'CK b ~> UN 'CK c, UN 'CK a ~> UN 'CK b))
     ('MK (UN 'CK a ~> UN 'CK c))
forall a b. (a -> b) -> a -> b
$ \(UN 'CK b ~> UN 'CK c
f, UN 'CK a ~> UN 'CK b
g) -> UN 'CK b ~> UN 'CK c
f (UN 'CK b ~> UN 'CK c)
-> (UN 'CK a ~> UN 'CK b) -> UN 'CK a ~> UN 'CK c
forall (b :: k) (c :: k) (a :: 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
. UN 'CK a ~> UN 'CK b
g


type MONADK :: forall {k} {kk} {a}. kk (a :: k) a -> k -> Type
data MONADK t ext where
  MDK :: () -> MONADK (t :: kk a a) exta

type instance V (MONADK (t :: kk a a)) = kk
type instance Arr kk (m :: MONADK (t :: kk a a) a) (n :: MONADK t a) = t

-- | A monad in a bicategory as a one object enriched category
instance Monad t => ECategory (MONADK (t :: kk a a)) where
  type EOb (m :: MONADK (t :: kk a a) exta) = (Is MDK m, exta ~ a)
  eid :: forall (exta :: k) (a :: MONADK t exta). EOb a => I ~> (a %~> a)
eid = I ~> t
I ~> Arr (V (MONADK t)) a a
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
I ~> t
eta
  ecomp :: forall (exta :: k) (a :: MONADK t exta) (extb :: k)
       (b :: MONADK t extb) (extc :: k) (c :: MONADK t extc).
(EOb a, EOb b, EOb c) =>
O (a %~> b) (b %~> c) ~> (a %~> c)
ecomp = O t t ~> t
O (Arr (V (MONADK t)) a b) (Arr (V (MONADK t)) b c)
~> Arr (V (MONADK t)) a c
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
O t t ~> t
mu