{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Bicategory.Terminal where

import Proarrow.Category.Bicategory (Bicategory(..), Monad (..))
import Proarrow.Core (CategoryOf(..), Profunctor(..), CAT, Promonad (..), dimapDefault)
import Data.Type.Equality (type (~~))

data TK = T0
type TERMK :: CAT TK
data TERMK j k where
  T1 :: TERMK T0 T0

type Terminal :: CAT (TERMK j k)
data Terminal a b where
  Terminal :: Terminal T1 T1

instance Profunctor (Terminal :: CAT (TERMK T0 T0)) where
  dimap :: forall (c :: TERMK 'T0 'T0) (a :: TERMK 'T0 'T0)
       (b :: TERMK 'T0 'T0) (d :: TERMK 'T0 'T0).
(c ~> a) -> (b ~> d) -> Terminal a b -> Terminal c d
dimap = (c ~> a) -> (b ~> d) -> Terminal a b -> Terminal c d
Terminal c a -> Terminal b d -> Terminal a b -> Terminal 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 :: TERMK 'T0 'T0) (b :: TERMK 'T0 'T0) r.
((Ob a, Ob b) => r) -> Terminal a b -> r
\\ Terminal a b
Terminal = r
(Ob a, Ob b) => r
r
instance Promonad (Terminal :: CAT (TERMK T0 T0)) where
  id :: forall (a :: TERMK 'T0 'T0). Ob a => Terminal a a
id = Terminal a a
Terminal 'T1 'T1
Terminal
  Terminal b c
Terminal . :: forall (b :: TERMK 'T0 'T0) (c :: TERMK 'T0 'T0)
       (a :: TERMK 'T0 'T0).
Terminal b c -> Terminal a b -> Terminal a c
. Terminal a b
Terminal = Terminal a c
Terminal 'T1 'T1
Terminal
instance (j ~ T0, k ~ T0) => CategoryOf (TERMK j k) where
  type (~>) = Terminal
  type Ob @(TERMK j k) p = (p ~~ T1)

instance Bicategory TERMK where
  type Ob0 TERMK k = (k ~ T0)
  type I = T1
  type O a b = T1
  (Ob0 TERMK i, Ob0 TERMK j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: TK) (j :: TK) (ps :: TERMK i j) (qs :: TERMK i j) r.
((Ob0 TERMK i, Ob0 TERMK j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ ps ~> qs
Terminal ps qs
Terminal = r
(Ob0 TERMK i, Ob0 TERMK j, Ob ps, Ob qs) => r
r
  a ~> b
Terminal a b
Terminal o :: forall {k1 :: TK} (i :: TK) (j :: TK) (a :: TERMK i j)
       (b :: TERMK i j) (c :: TERMK j k1) (d :: TERMK j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` c ~> d
Terminal c d
Terminal = O a c ~> O b d
Terminal 'T1 'T1
Terminal
  leftUnitor :: forall (i :: TK) (j :: TK) (a :: TERMK i j). Obj a -> O I a ~> a
leftUnitor Obj a
Terminal a a
Terminal = O I a ~> a
Terminal 'T1 'T1
Terminal
  leftUnitorInv :: forall (i :: TK) (j :: TK) (a :: TERMK i j). Obj a -> a ~> O I a
leftUnitorInv Obj a
Terminal a a
Terminal = a ~> O I a
Terminal 'T1 'T1
Terminal
  rightUnitor :: forall (i :: TK) (j :: TK) (a :: TERMK i j). Obj a -> O a I ~> a
rightUnitor Obj a
Terminal a a
Terminal = O a I ~> a
Terminal 'T1 'T1
Terminal
  rightUnitorInv :: forall (i :: TK) (j :: TK) (a :: TERMK i j). Obj a -> a ~> O a I
rightUnitorInv Obj a
Terminal a a
Terminal = a ~> O a I
Terminal 'T1 'T1
Terminal
  associator :: forall {j1 :: TK} {k1 :: TK} (i :: TK) (j2 :: TK) (a :: TERMK i j2)
       (b :: TERMK j2 j1) (c :: TERMK j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator Obj a
Terminal a a
Terminal Obj b
Terminal b b
Terminal Obj c
Terminal c c
Terminal = O (O a b) c ~> O a (O b c)
Terminal 'T1 'T1
Terminal
  associatorInv :: forall {j1 :: TK} {k1 :: TK} (i :: TK) (j2 :: TK) (a :: TERMK i j2)
       (b :: TERMK j2 j1) (c :: TERMK j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv Obj a
Terminal a a
Terminal Obj b
Terminal b b
Terminal Obj c
Terminal c c
Terminal = O a (O b c) ~> O (O a b) c
Terminal 'T1 'T1
Terminal

instance Monad T1 where
  eta :: I ~> 'T1
eta = I ~> 'T1
Terminal 'T1 'T1
Terminal
  mu :: O 'T1 'T1 ~> 'T1
mu = O 'T1 'T1 ~> 'T1
Terminal 'T1 'T1
Terminal