Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory.Terminal

Documentation

data TK Source Comments #

Constructors

T0

Instances

Instances details

Bicategory TERMK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

Associated Types

type Ob0 TERMK (k :: TK)
Instance details Defined in Proarrow.Category.Bicategory.Terminal type Ob0 TERMK (k :: TK) = k ~ 'T0
type I
Instance details Defined in Proarrow.Category.Bicategory.Terminal type I = 'T1
type O (a :: TERMK 'T0 j) (b :: TERMK j 'T0)
Instance details Defined in Proarrow.Category.Bicategory.Terminal type O (a :: TERMK 'T0 j) (b :: TERMK j 'T0) = 'T1

Methods

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 Source Comments #

(\\\) :: 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 Source Comments #

leftUnitor :: forall (i :: TK) (j :: TK) (a :: TERMK i j). Obj a -> O (I :: TERMK i i) a ~> a Source Comments #

leftUnitorInv :: forall (i :: TK) (j :: TK) (a :: TERMK i j). Obj a -> a ~> O (I :: TERMK i i) a Source Comments #

rightUnitor :: forall (i :: TK) (j :: TK) (a :: TERMK i j). Obj a -> O a (I :: TERMK j j) ~> a Source Comments #

rightUnitorInv :: forall (i :: TK) (j :: TK) (a :: TERMK i j). Obj a -> a ~> O a (I :: TERMK j j) Source Comments #

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) Source Comments #

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 Source Comments #

Monad 'T1 Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

Methods

eta :: (I :: TERMK 'T0 'T0) ~> 'T1 Source Comments #

mu :: O 'T1 'T1 ~> 'T1 Source Comments #

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

type I = 'T1

type Ob0 TERMK (k :: TK) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

type Ob0 TERMK (k :: TK) = k ~ 'T0

type O (a :: TERMK 'T0 j) (b :: TERMK j 'T0) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

type O (a :: TERMK 'T0 j) (b :: TERMK j 'T0) = 'T1

data TERMK (j :: TK) (k :: TK) where Source Comments #

Constructors

T1 :: TERMK 'T0 'T0

Instances

Instances details

Bicategory TERMK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

Associated Types

type Ob0 TERMK (k :: TK)
Instance details Defined in Proarrow.Category.Bicategory.Terminal type Ob0 TERMK (k :: TK) = k ~ 'T0
type I
Instance details Defined in Proarrow.Category.Bicategory.Terminal type I = 'T1
type O (a :: TERMK 'T0 j) (b :: TERMK j 'T0)
Instance details Defined in Proarrow.Category.Bicategory.Terminal type O (a :: TERMK 'T0 j) (b :: TERMK j 'T0) = 'T1

Methods

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 Source Comments #

(\\\) :: 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 Source Comments #

leftUnitor :: forall (i :: TK) (j :: TK) (a :: TERMK i j). Obj a -> O (I :: TERMK i i) a ~> a Source Comments #

leftUnitorInv :: forall (i :: TK) (j :: TK) (a :: TERMK i j). Obj a -> a ~> O (I :: TERMK i i) a Source Comments #

rightUnitor :: forall (i :: TK) (j :: TK) (a :: TERMK i j). Obj a -> O a (I :: TERMK j j) ~> a Source Comments #

rightUnitorInv :: forall (i :: TK) (j :: TK) (a :: TERMK i j). Obj a -> a ~> O a (I :: TERMK j j) Source Comments #

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) Source Comments #

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 Source Comments #

Monad 'T1 Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

Methods

eta :: (I :: TERMK 'T0 'T0) ~> 'T1 Source Comments #

mu :: O 'T1 'T1 ~> 'T1 Source Comments #

(j ~ 'T0, k ~ 'T0) => CategoryOf (TERMK j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Bicategory.Terminal type (~>) = Terminal :: TERMK j k -> TERMK j k -> Type

Promonad (Terminal :: TERMK 'T0 'T0 -> TERMK 'T0 'T0 -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

Methods

id :: forall (a :: TERMK 'T0 'T0). Ob a => Terminal a a Source Comments #

(.) :: forall (b :: TERMK 'T0 'T0) (c :: TERMK 'T0 'T0) (a :: TERMK 'T0 'T0). Terminal b c -> Terminal a b -> Terminal a c Source Comments #

Profunctor (Terminal :: TERMK 'T0 'T0 -> TERMK 'T0 'T0 -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

Methods

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 Source Comments #

(\\) :: forall (a :: TERMK 'T0 'T0) (b :: TERMK 'T0 'T0) r. ((Ob a, Ob b) => r) -> Terminal a b -> r Source Comments #

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

type I = 'T1

type Ob0 TERMK (k :: TK) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

type Ob0 TERMK (k :: TK) = k ~ 'T0

type O (a :: TERMK 'T0 j) (b :: TERMK j 'T0) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

type O (a :: TERMK 'T0 j) (b :: TERMK j 'T0) = 'T1

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

type (~>) = Terminal :: TERMK j k -> TERMK j k -> Type

type Ob (p :: TERMK j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

type Ob (p :: TERMK j k) = p ~~ 'T1

data Terminal (a :: TERMK j k) (b :: TERMK j k) where Source Comments #

Constructors

Terminal :: Terminal 'T1 'T1

Instances

Instances details

Promonad (Terminal :: TERMK 'T0 'T0 -> TERMK 'T0 'T0 -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Terminal Methods id :: forall (a :: TERMK 'T0 'T0). Ob a => Terminal a a Source Comments # (.) :: forall (b :: TERMK 'T0 'T0) (c :: TERMK 'T0 'T0) (a :: TERMK 'T0 'T0). Terminal b c -> Terminal a b -> Terminal a c Source Comments #
Profunctor (Terminal :: TERMK 'T0 'T0 -> TERMK 'T0 'T0 -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Terminal Methods 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 Source Comments # (\\) :: forall (a :: TERMK 'T0 'T0) (b :: TERMK 'T0 'T0) r. ((Ob a, Ob b) => r) -> Terminal a b -> r Source Comments #