proarrow-0: Category theory with a central role for profunctors
Safe HaskellNone
LanguageHaskell2010

Proarrow.Category.Enriched

Documentation

type family V (vk :: k -> Type) :: CAT k Source Comments #

Instances

Instances details
type V (CATK k :: () -> Kind) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched

type V (CATK k :: () -> Kind) = MonK Type
type V (BIPARAK k :: () -> Kind) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched.Bipara

type V (BIPARAK k :: () -> Kind) = MonK (PRO k k)
type V (MONADK t :: k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched

type V (MONADK t :: k -> Type) = kk

type family Arr (v :: CAT k) (a :: vk exta) (b :: vk extb) :: v exta extb Source Comments #

Instances

Instances details
type Arr (MonK Type) ('CK a :: CATK k exta) ('CK b :: CATK k extb) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched

type Arr (MonK Type) ('CK a :: CATK k exta) ('CK b :: CATK k extb) = 'MK (a ~> b) :: MonK Type exta extb
type Arr (MonK (PRO k k) :: () -> () -> Type) ('BIPARA a :: BIPARAK k exta) ('BIPARA b :: BIPARAK k extb) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched.Bipara

type Arr (MonK (PRO k k) :: () -> () -> Type) ('BIPARA a :: BIPARAK k exta) ('BIPARA b :: BIPARAK k extb) = 'MK (Bipara a b) :: MonK (k -> k -> Type) exta extb
type Arr (kk :: CAT k) (m :: MONADK t a) (n :: MONADK t a) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched

type Arr (kk :: CAT k) (m :: MONADK t a) (n :: MONADK t a) = t

type (%~>) (a :: vk exta) (b :: vk extb) = Arr (V vk) a b Source Comments #

class Bicategory (V vk) => ECategory (vk :: k -> Type) where Source Comments #

Associated Types

type EOb (a :: vk exta) Source Comments #

Methods

eid :: forall (exta :: k) (a :: vk exta). EOb a => (I :: V vk exta exta) ~> (a %~> a) Source Comments #

ecomp :: forall (exta :: k) (a :: vk exta) (extb :: k) (b :: vk extb) (extc :: k) (c :: vk extc). (EOb a, EOb b, EOb c) => O (a %~> b) (b %~> c) ~> (a %~> c) Source Comments #

Instances

Instances details
CategoryOf k => ECategory (CATK k :: () -> Kind) Source Comments #

A regular category as a Type-enriched category

Instance details

Defined in Proarrow.Category.Enriched

Methods

eid :: forall (exta :: ()) (a :: CATK k exta). EOb a => (I :: V (CATK k) exta exta) ~> (a %~> a) Source Comments #

ecomp :: forall (exta :: ()) (a :: CATK k exta) (extb :: ()) (b :: CATK k extb) (extc :: ()) (c :: CATK k extc). (EOb a, EOb b, EOb c) => O (a %~> b) (b %~> c) ~> (a %~> c) Source Comments #

SymMonoidal k => ECategory (BIPARAK k :: () -> Kind) Source Comments #

Bipara as a profunctor enriched category.

Instance details

Defined in Proarrow.Category.Enriched.Bipara

Methods

eid :: forall (exta :: ()) (a :: BIPARAK k exta). EOb a => (I :: V (BIPARAK k) exta exta) ~> (a %~> a) Source Comments #

ecomp :: forall (exta :: ()) (a :: BIPARAK k exta) (extb :: ()) (b :: BIPARAK k extb) (extc :: ()) (c :: BIPARAK k extc). (EOb a, EOb b, EOb c) => O (a %~> b) (b %~> c) ~> (a %~> c) Source Comments #

Monad t => ECategory (MONADK t :: k -> Type) Source Comments #

A monad in a bicategory as a one object enriched category

Instance details

Defined in Proarrow.Category.Enriched

Methods

eid :: forall (exta :: k) (a0 :: MONADK t exta). EOb a0 => (I :: V (MONADK t) exta exta) ~> (a0 %~> a0) Source Comments #

ecomp :: forall (exta :: k) (a0 :: MONADK t exta) (extb :: k) (b :: MONADK t extb) (extc :: k) (c :: MONADK t extc). (EOb a0, EOb b, EOb c) => O (a0 %~> b) (b %~> c) ~> (a0 %~> c) Source Comments #

data CATK k (ext :: ()) where Source Comments #

Constructors

CK :: forall k (ext :: ()). k -> CATK k ext 

Instances

Instances details
CategoryOf k => ECategory (CATK k :: () -> Kind) Source Comments #

A regular category as a Type-enriched category

Instance details

Defined in Proarrow.Category.Enriched

Methods

eid :: forall (exta :: ()) (a :: CATK k exta). EOb a => (I :: V (CATK k) exta exta) ~> (a %~> a) Source Comments #

ecomp :: forall (exta :: ()) (a :: CATK k exta) (extb :: ()) (b :: CATK k extb) (extc :: ()) (c :: CATK k extc). (EOb a, EOb b, EOb c) => O (a %~> b) (b %~> c) ~> (a %~> c) Source Comments #

type V (CATK k :: () -> Kind) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched

type V (CATK k :: () -> Kind) = MonK Type
type EOb (a :: CATK k exta) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched

type EOb (a :: CATK k exta) = (Is ('CK :: k -> CATK k exta) a, Ob (UN ('CK :: k -> CATK k exta) a))
type Arr (MonK Type) ('CK a :: CATK k exta) ('CK b :: CATK k extb) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched

type Arr (MonK Type) ('CK a :: CATK k exta) ('CK b :: CATK k extb) = 'MK (a ~> b) :: MonK Type exta extb
type UN ('CK :: j -> CATK j i) ('CK a :: CATK j i) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched

type UN ('CK :: j -> CATK j i) ('CK a :: CATK j i) = a

data MONADK (t :: kk a a) (ext :: k) where Source Comments #

Constructors

MDK :: forall {k} (kk :: k -> k -> Type) (a :: k) (t :: kk a a) (ext :: k). () -> MONADK t ext 

Instances

Instances details
Monad t => ECategory (MONADK t :: k -> Type) Source Comments #

A monad in a bicategory as a one object enriched category

Instance details

Defined in Proarrow.Category.Enriched

Methods

eid :: forall (exta :: k) (a0 :: MONADK t exta). EOb a0 => (I :: V (MONADK t) exta exta) ~> (a0 %~> a0) Source Comments #

ecomp :: forall (exta :: k) (a0 :: MONADK t exta) (extb :: k) (b :: MONADK t extb) (extc :: k) (c :: MONADK t extc). (EOb a0, EOb b, EOb c) => O (a0 %~> b) (b %~> c) ~> (a0 %~> c) Source Comments #

type V (MONADK t :: k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched

type V (MONADK t :: k -> Type) = kk
type EOb (m :: MONADK t exta) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched

type EOb (m :: MONADK t exta) = (Is ('MDK :: () -> MONADK t exta) m, exta ~ a)
type Arr (kk :: CAT k) (m :: MONADK t a) (n :: MONADK t a) Source Comments # 
Instance details

Defined in Proarrow.Category.Enriched

type Arr (kk :: CAT k) (m :: MONADK t a) (n :: MONADK t a) = t