Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory.Bidiscrete

Documentation

data DiscreteK (ob :: OB c) (j :: c) (k :: c) where Source Comments #

Constructors

DK :: forall {c} (ob :: OB c) (j :: c). DiscreteK ob j j

Instances

Instances details

CategoryOf c => Bicategory (DiscreteK ob :: c -> c -> Type) Source Comments #

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

Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

Methods

iObj :: forall (i :: c). Ob0 (DiscreteK ob) i => Obj (I :: DiscreteK ob i i) Source Comments #

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

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

leftUnitor :: forall {i :: c} {j :: c} (a :: DiscreteK ob i j). (Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob a) => O (I :: DiscreteK ob j j) a ~> a Source Comments #

leftUnitorInv :: forall {i :: c} {j :: c} (a :: DiscreteK ob i j). (Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob a) => a ~> O (I :: DiscreteK ob j j) a Source Comments #

rightUnitor :: forall {i :: c} {j :: c} (a :: DiscreteK ob i j). (Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob a) => O a (I :: DiscreteK ob i i) ~> a Source Comments #

rightUnitorInv :: forall {i :: c} {j :: c} (a :: DiscreteK ob i j). (Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob a) => a ~> O a (I :: DiscreteK ob i i) Source Comments #

associator :: forall {h :: c} {i :: c} {j :: c} {k :: c} (a :: DiscreteK ob j k) (b :: DiscreteK ob i j) (c0 :: DiscreteK ob h i). (Ob0 (DiscreteK ob) h, Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob0 (DiscreteK ob) k, Ob a, Ob b, Ob c0) => O (O a b) c0 ~> O a (O b c0) Source Comments #

associatorInv :: forall {h :: c} {i :: c} {j :: c} {k :: c} (a :: DiscreteK ob j k) (b :: DiscreteK ob i j) (c0 :: DiscreteK ob h i). (Ob0 (DiscreteK ob) h, Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob0 (DiscreteK ob) k, Ob a, Ob b, Ob c0) => O a (O b c0) ~> O (O a b) c0 Source Comments #

Bicategory kk => Equipment (WKK kk :: s -> s -> Type) (DiscreteK (Ob0' kk :: s -> Constraint) :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

Methods

mapConjoint :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) j k). (f ~> g) -> Conjoint (WKK kk) g ~> Conjoint (WKK kk) f Source Comments #

conjToId :: forall (k :: s). Ob0 (DiscreteK (Ob0' kk :: s -> Constraint)) k => Conjoint (WKK kk) (I :: DiscreteK (Ob0' kk :: s -> Constraint) k k) ~> (I :: WKK kk k k) Source Comments #

conjFromId :: forall (k :: s). Ob0 (DiscreteK (Ob0' kk :: s -> Constraint)) k => (I :: WKK kk k k) ~> Conjoint (WKK kk) (I :: DiscreteK (Ob0' kk :: s -> Constraint) k k) Source Comments #

conjToCompose :: forall {k1 :: s} {j :: s} {k2 :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k2) (g :: DiscreteK (Ob0' kk :: s -> Constraint) k1 j). Obj f -> Obj g -> Conjoint (WKK kk) (O f g) ~> O (Conjoint (WKK kk) g) (Conjoint (WKK kk) f) Source Comments #

conjFromCompose :: forall {j1 :: s} {j2 :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j2 k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) j1 j2). Obj f -> Obj g -> O (Conjoint (WKK kk) g) (Conjoint (WKK kk) f) ~> Conjoint (WKK kk) (O f g) Source Comments #

comConUnit :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k). Obj f -> (I :: WKK kk j j) ~> O (Conjoint (WKK kk) f) (Companion (WKK kk) f) Source Comments #

comConCounit :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k). Obj f -> O (Companion (WKK kk) f) (Conjoint (WKK kk) f) ~> (I :: WKK kk k k) Source Comments #

Bicategory kk => HasCompanions (WKK kk :: s -> s -> Type) (DiscreteK (Ob0' kk :: s -> Constraint) :: s -> s -> Type) Source Comments #

A bicategory as a proarrow equipment with only identity arrows vertically.

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

Methods

mapCompanion :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) j k). (f ~> g) -> Companion (WKK kk) f ~> Companion (WKK kk) g Source Comments #

compToId :: forall (k :: s). Ob0 (DiscreteK (Ob0' kk :: s -> Constraint)) k => Companion (WKK kk) (I :: DiscreteK (Ob0' kk :: s -> Constraint) k k) ~> (I :: WKK kk k k) Source Comments #

compFromId :: forall (k :: s). Ob0 (DiscreteK (Ob0' kk :: s -> Constraint)) k => (I :: WKK kk k k) ~> Companion (WKK kk) (I :: DiscreteK (Ob0' kk :: s -> Constraint) k k) Source Comments #

compToCompose :: forall {i :: s} {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) i j). Obj f -> Obj g -> Companion (WKK kk) (O f g) ~> O (Companion (WKK kk) f) (Companion (WKK kk) g) Source Comments #

compFromCompose :: forall {j1 :: s} {j2 :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j2 k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) j1 j2). Obj f -> Obj g -> O (Companion (WKK kk) f) (Companion (WKK kk) g) ~> Companion (WKK kk) (O f g) Source Comments #

CategoryOf (DiscreteK ob 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 ob j k -> DiscreteK ob j k -> Type

Promonad (Bidiscrete :: DiscreteK ob j k -> DiscreteK ob j k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

Methods

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

Methods

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

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

type Ob0 (DiscreteK ob :: c -> c -> Type) (k :: c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

type Ob0 (DiscreteK ob :: c -> c -> Type) (k :: c) = ob k

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

type I = 'DK :: DiscreteK ob i i

type O ('DK :: DiscreteK ob i i) ('DK :: DiscreteK ob i i) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

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

type Companion (WKK kk :: s -> s -> Type) ('DK :: DiscreteK (Ob0' kk :: s -> Constraint) j j) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

type Companion (WKK kk :: s -> s -> Type) ('DK :: DiscreteK (Ob0' kk :: s -> Constraint) j j) = 'WK (I :: kk j j)

type Conjoint (WKK kk :: s -> s -> Type) ('DK :: DiscreteK (Ob0' kk :: s -> Constraint) j j) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

type Conjoint (WKK kk :: s -> s -> Type) ('DK :: DiscreteK (Ob0' kk :: s -> Constraint) j j) = 'WK (I :: kk j j)

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

type (~>) = Bidiscrete :: DiscreteK ob j k -> DiscreteK ob j k -> Type

type Ob (a :: DiscreteK ob j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Bidiscrete

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

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

Constructors

Bidiscrete :: forall {c} (ob :: OB c) (j :: c). ob j => Bidiscrete ('DK :: DiscreteK ob j j) ('DK :: DiscreteK ob j j)

Instances

Instances details

Promonad (Bidiscrete :: DiscreteK ob j k -> DiscreteK ob j k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Bidiscrete Methods id :: forall (a :: DiscreteK ob j k). Ob a => Bidiscrete a a Source Comments # (.) :: forall (b :: DiscreteK ob j k) (c0 :: DiscreteK ob j k) (a :: DiscreteK ob j k). Bidiscrete b c0 -> Bidiscrete a b -> Bidiscrete a c0 Source Comments #
Profunctor (Bidiscrete :: DiscreteK ob j k -> DiscreteK ob j k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Bidiscrete Methods dimap :: forall (c0 :: DiscreteK ob j k) (a :: DiscreteK ob j k) (b :: DiscreteK ob j k) (d :: DiscreteK ob j k). (c0 ~> a) -> (b ~> d) -> Bidiscrete a b -> Bidiscrete c0 d Source Comments # (\\) :: forall (a :: DiscreteK ob j k) (b :: DiscreteK ob j k) r. ((Ob a, Ob b) => r) -> Bidiscrete a b -> r Source Comments #