module Proarrow.Category.Instance.Unit where

import Proarrow.Core (CAT, CategoryOf(..), Profunctor(..), Promonad(..), dimapDefault)
import Proarrow.Object.Initial (HasInitialObject(..))
import Proarrow.Object.Terminal (HasTerminalObject(..))


type data UNIT = U

type Unit :: CAT UNIT
data Unit a b where
  Unit :: Unit U U


-- | The category with one object, the terminal category.
instance CategoryOf UNIT where
  type (~>) = Unit
  type Ob a = a ~ U

instance Promonad Unit where
  id :: forall (a :: UNIT). Ob a => Unit a a
id = Unit a a
Unit U U
Unit
  Unit b c
Unit . :: forall (b :: UNIT) (c :: UNIT) (a :: UNIT).
Unit b c -> Unit a b -> Unit a c
. Unit a b
Unit = Unit a c
Unit U U
Unit

instance Profunctor Unit where
  dimap :: forall (c :: UNIT) (a :: UNIT) (b :: UNIT) (d :: UNIT).
(c ~> a) -> (b ~> d) -> Unit a b -> Unit c d
dimap = (c ~> a) -> (b ~> d) -> Unit a b -> Unit c d
Unit c a -> Unit b d -> Unit a b -> Unit 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) -> Unit a b -> r
\\ Unit a b
Unit = r
(Ob a, Ob b) => r
r

instance HasTerminalObject UNIT where
  type TerminalObject = U
  terminate' :: forall (a :: UNIT). Obj a -> a ~> TerminalObject
terminate' Obj a
Unit a a
Unit = a ~> TerminalObject
Unit U U
Unit

instance HasInitialObject UNIT where
  type InitialObject = U
  initiate' :: forall (a :: UNIT). Obj a -> InitialObject ~> a
initiate' Obj a
Unit a a
Unit = InitialObject ~> a
Unit U U
Unit