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