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

Proarrow.Category.Bicategory.Bidiscrete

Documentation

data DiscreteK j k where Source Comments #

Constructors

DK :: forall j. DiscreteK j j 

Instances

Instances details
Bicategory DiscreteK Source Comments #

The bicategory with only identity 1-cells and identity 2-cells between those.

Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

Associated Types

type Ob0 DiscreteK (j :: k1) 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

type Ob0 DiscreteK (j :: k1) = Any j
type I 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

type I = 'DK :: DiscreteK i i
type O ('DK :: DiscreteK i i) ('DK :: DiscreteK i i) 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

type O ('DK :: DiscreteK i i) ('DK :: DiscreteK i i) = 'DK :: DiscreteK i i

Methods

o :: forall {k1} i j (a :: DiscreteK i j) (b :: DiscreteK i j) (c :: DiscreteK j k1) (d :: DiscreteK j k1). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

(\\\) :: forall i j (ps :: DiscreteK i j) (qs :: DiscreteK i j) r. ((Ob0 DiscreteK i, Ob0 DiscreteK j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r Source Comments #

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

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

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

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

associator :: forall {j1} {k1} i j2 (a :: DiscreteK i j2) (b :: DiscreteK j2 j1) (c :: DiscreteK j1 k1). Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c) Source Comments #

associatorInv :: forall {j1} {k1} i j2 (a :: DiscreteK i j2) (b :: DiscreteK j2 j1) (c :: DiscreteK j1 k1). Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c Source Comments #

CategoryOf (DiscreteK j k) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

type (~>) = Bidiscrete :: DiscreteK j k -> DiscreteK j k -> Type
Promonad (Bidiscrete :: DiscreteK j k -> DiscreteK j k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

Methods

id :: forall (a :: DiscreteK j k). Ob a => Bidiscrete a a Source Comments #

(.) :: forall (b :: DiscreteK j k) (c :: DiscreteK j k) (a :: DiscreteK j k). Bidiscrete b c -> Bidiscrete a b -> Bidiscrete a c Source Comments #

Profunctor (Bidiscrete :: DiscreteK j k -> DiscreteK j k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

Methods

dimap :: forall (c :: DiscreteK j k) (a :: DiscreteK j k) (b :: DiscreteK j k) (d :: DiscreteK j k). (c ~> a) -> (b ~> d) -> Bidiscrete a b -> Bidiscrete c d Source Comments #

(\\) :: forall (a :: DiscreteK j k) (b :: DiscreteK j k) r. ((Ob a, Ob b) => r) -> Bidiscrete a b -> r Source Comments #

type I Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

type I = 'DK :: DiscreteK i i
type Ob0 DiscreteK (j :: k1) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

type Ob0 DiscreteK (j :: k1) = Any j
type O ('DK :: DiscreteK i i) ('DK :: DiscreteK i i) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

type O ('DK :: DiscreteK i i) ('DK :: DiscreteK i i) = 'DK :: DiscreteK i i
type (~>) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

type (~>) = Bidiscrete :: DiscreteK j k -> DiscreteK j k -> Type
type Ob (a :: DiscreteK j k) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

type Ob (a :: DiscreteK j k) = (j ~ k, a ~~ ('DK :: DiscreteK j j))

data Bidiscrete (a :: DiscreteK j k) (b :: DiscreteK j k) where Source Comments #

Constructors

Bidiscrete :: forall {j}. Bidiscrete ('DK :: DiscreteK j j) ('DK :: DiscreteK j j) 

Instances

Instances details
Promonad (Bidiscrete :: DiscreteK j k -> DiscreteK j k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

Methods

id :: forall (a :: DiscreteK j k). Ob a => Bidiscrete a a Source Comments #

(.) :: forall (b :: DiscreteK j k) (c :: DiscreteK j k) (a :: DiscreteK j k). Bidiscrete b c -> Bidiscrete a b -> Bidiscrete a c Source Comments #

Profunctor (Bidiscrete :: DiscreteK j k -> DiscreteK j k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

Methods

dimap :: forall (c :: DiscreteK j k) (a :: DiscreteK j k) (b :: DiscreteK j k) (d :: DiscreteK j k). (c ~> a) -> (b ~> d) -> Bidiscrete a b -> Bidiscrete c d Source Comments #

(\\) :: forall (a :: DiscreteK j k) (b :: DiscreteK j k) r. ((Ob a, Ob b) => r) -> Bidiscrete a b -> r Source Comments #