{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Bicategory.Terminal where

import Data.Type.Equality (type (~), type (~~))

import Proarrow.Category.Bicategory (Bicategory (..), Monad (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault)

type Terminal :: CAT (Unit j k)
data Terminal a b where
  Terminal :: Terminal 'Unit 'Unit

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

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

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