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