Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory.Co

Documentation

newtype COK (kk :: CAT k) (j :: k) (k1 :: k) Source Comments #

Constructors

CO (kk j k1)

Instances

Instances details

Bicategory kk => Bicategory (COK kk :: s -> s -> Type) Source Comments #

Create a dual of a bicategory by reversing the 2-cells.

Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

iObj :: forall (i :: s). Ob0 (COK kk) i => Obj (I :: COK kk i i) Source Comments #

o :: forall {i :: s} (j :: s) (k :: s) (a :: COK kk j k) (b :: COK kk j k) (c :: COK kk i j) (d :: COK kk i j). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

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

leftUnitor :: forall {i :: s} {j :: s} (a :: COK kk i j). (Ob0 (COK kk) i, Ob0 (COK kk) j, Ob a) => O (I :: COK kk j j) a ~> a Source Comments #

leftUnitorInv :: forall {i :: s} {j :: s} (a :: COK kk i j). (Ob0 (COK kk) i, Ob0 (COK kk) j, Ob a) => a ~> O (I :: COK kk j j) a Source Comments #

rightUnitor :: forall {i :: s} {j :: s} (a :: COK kk i j). (Ob0 (COK kk) i, Ob0 (COK kk) j, Ob a) => O a (I :: COK kk i i) ~> a Source Comments #

rightUnitorInv :: forall {i :: s} {j :: s} (a :: COK kk i j). (Ob0 (COK kk) i, Ob0 (COK kk) j, Ob a) => a ~> O a (I :: COK kk i i) Source Comments #

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

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

RightKanExtension j2 f => LeftKanExtension ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type Lan ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e)
Instance details Defined in Proarrow.Category.Bicategory.Co type Lan ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) = 'CO (Ran j2 f)

Methods

lan :: 'CO f ~> O (Lan ('CO j2) ('CO f)) ('CO j2) Source Comments #

lanUniv :: forall (g :: COK kk d e). Ob g => ('CO f ~> O g ('CO j2)) -> Lan ('CO j2) ('CO f) ~> g Source Comments #

RightKanLift j f => LeftKanLift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type Lift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2)
Instance details Defined in Proarrow.Category.Bicategory.Co type Lift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) = 'CO (Rift j f)

Methods

lift :: 'CO f ~> O ('CO j) (Lift ('CO j) ('CO f)) Source Comments #

liftUniv :: forall (g :: COK kk e d). Ob g => ('CO f ~> O ('CO j) g) -> Lift ('CO j) ('CO f) ~> g Source Comments #

LeftKanExtension j2 f => RightKanExtension ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type Ran ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e)
Instance details Defined in Proarrow.Category.Bicategory.Co type Ran ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) = 'CO (Lan j2 f)

Methods

ran :: O (Ran ('CO j2) ('CO f)) ('CO j2) ~> 'CO f Source Comments #

ranUniv :: forall (g :: COK kk d e). Ob g => (O g ('CO j2) ~> 'CO f) -> g ~> Ran ('CO j2) ('CO f) Source Comments #

LeftKanLift j f => RightKanLift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type Rift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2)
Instance details Defined in Proarrow.Category.Bicategory.Co type Rift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) = 'CO (Lift j f)

Methods

rift :: O ('CO j) (Rift ('CO j) ('CO f)) ~> 'CO f Source Comments #

riftUniv :: forall (g :: COK kk e d). Ob g => (O ('CO j) g ~> 'CO f) -> g ~> Rift ('CO j) ('CO f) Source Comments #

Adjunction f g => Adjunction ('CO g :: COK kk k2 j) ('CO f :: COK kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

unit :: (I :: COK kk k2 k2) ~> O ('CO f) ('CO g) Source Comments #

counit :: O ('CO g) ('CO f) ~> (I :: COK kk j j) Source Comments #

Monad m => Comonad ('CO m :: COK kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

epsilon :: 'CO m ~> (I :: COK kk a a) Source Comments #

delta :: 'CO m ~> O ('CO m) ('CO m) Source Comments #

Comonad m => Monad ('CO m :: COK kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

eta :: (I :: COK kk a a) ~> 'CO m Source Comments #

mu :: O ('CO m) ('CO m) ~> 'CO m Source Comments #

Equipment hk vk => Equipment (COK hk :: k -> k -> Type) (OPK vk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

mapConjoint :: forall {j :: k} {k0 :: k} (f :: OPK vk j k0) (g :: OPK vk j k0). (f ~> g) -> Conjoint (COK hk) g ~> Conjoint (COK hk) f Source Comments #

conjToId :: forall (k0 :: k). Ob0 (OPK vk) k0 => Conjoint (COK hk) (I :: OPK vk k k) ~> (I :: COK hk k k) Source Comments #

conjFromId :: forall (k0 :: k). Ob0 (OPK vk) k0 => (I :: COK hk k k) ~> Conjoint (COK hk) (I :: OPK vk k k) Source Comments #

conjToCompose :: forall {k1 :: k} {j :: k} {k2 :: k} (f :: OPK vk j k2) (g :: OPK vk k1 j). Obj f -> Obj g -> Conjoint (COK hk) (O f g) ~> O (Conjoint (COK hk) g) (Conjoint (COK hk) f) Source Comments #

conjFromCompose :: forall {j1 :: k} {j2 :: k} {k0 :: k} (f :: OPK vk j2 k0) (g :: OPK vk j1 j2). Obj f -> Obj g -> O (Conjoint (COK hk) g) (Conjoint (COK hk) f) ~> Conjoint (COK hk) (O f g) Source Comments #

comConUnit :: forall {j :: k} {k0 :: k} (f :: OPK vk j k0). Obj f -> (I :: COK hk j j) ~> O (Conjoint (COK hk) f) (Companion (COK hk) f) Source Comments #

comConCounit :: forall {j :: k} {k0 :: k} (f :: OPK vk j k0). Obj f -> O (Companion (COK hk) f) (Conjoint (COK hk) f) ~> (I :: COK hk k k) Source Comments #

Equipment hk vk => Equipment (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

mapConjoint :: forall {j :: k} {k0 :: k} (f :: COK vk j k0) (g :: COK vk j k0). (f ~> g) -> Conjoint (OPK hk) g ~> Conjoint (OPK hk) f Source Comments #

conjToId :: forall (k0 :: k). Ob0 (COK vk) k0 => Conjoint (OPK hk) (I :: COK vk k k) ~> (I :: OPK hk k k) Source Comments #

conjFromId :: forall (k0 :: k). Ob0 (COK vk) k0 => (I :: OPK hk k k) ~> Conjoint (OPK hk) (I :: COK vk k k) Source Comments #

conjToCompose :: forall {k1 :: k} {j :: k} {k2 :: k} (f :: COK vk j k2) (g :: COK vk k1 j). Obj f -> Obj g -> Conjoint (OPK hk) (O f g) ~> O (Conjoint (OPK hk) g) (Conjoint (OPK hk) f) Source Comments #

conjFromCompose :: forall {j1 :: k} {j2 :: k} {k0 :: k} (f :: COK vk j2 k0) (g :: COK vk j1 j2). Obj f -> Obj g -> O (Conjoint (OPK hk) g) (Conjoint (OPK hk) f) ~> Conjoint (OPK hk) (O f g) Source Comments #

comConUnit :: forall {j :: k} {k0 :: k} (f :: COK vk j k0). Obj f -> (I :: OPK hk j j) ~> O (Conjoint (OPK hk) f) (Companion (OPK hk) f) Source Comments #

comConCounit :: forall {j :: k} {k0 :: k} (f :: COK vk j k0). Obj f -> O (Companion (OPK hk) f) (Conjoint (OPK hk) f) ~> (I :: OPK hk k k) Source Comments #

Equipment hk vk => HasCompanions (COK hk :: k -> k -> Type) (OPK vk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

mapCompanion :: forall {j :: k} {k0 :: k} (f :: OPK vk j k0) (g :: OPK vk j k0). (f ~> g) -> Companion (COK hk) f ~> Companion (COK hk) g Source Comments #

compToId :: forall (k0 :: k). Ob0 (OPK vk) k0 => Companion (COK hk) (I :: OPK vk k k) ~> (I :: COK hk k k) Source Comments #

compFromId :: forall (k0 :: k). Ob0 (OPK vk) k0 => (I :: COK hk k k) ~> Companion (COK hk) (I :: OPK vk k k) Source Comments #

compToCompose :: forall {i :: k} {j :: k} {k0 :: k} (f :: OPK vk j k0) (g :: OPK vk i j). Obj f -> Obj g -> Companion (COK hk) (O f g) ~> O (Companion (COK hk) f) (Companion (COK hk) g) Source Comments #

compFromCompose :: forall {j1 :: k} {j2 :: k} {k0 :: k} (f :: OPK vk j2 k0) (g :: OPK vk j1 j2). Obj f -> Obj g -> O (Companion (COK hk) f) (Companion (COK hk) g) ~> Companion (COK hk) (O f g) Source Comments #

Equipment hk vk => HasCompanions (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

mapCompanion :: forall {j :: k} {k0 :: k} (f :: COK vk j k0) (g :: COK vk j k0). (f ~> g) -> Companion (OPK hk) f ~> Companion (OPK hk) g Source Comments #

compToId :: forall (k0 :: k). Ob0 (COK vk) k0 => Companion (OPK hk) (I :: COK vk k k) ~> (I :: OPK hk k k) Source Comments #

compFromId :: forall (k0 :: k). Ob0 (COK vk) k0 => (I :: OPK hk k k) ~> Companion (OPK hk) (I :: COK vk k k) Source Comments #

compToCompose :: forall {i :: k} {j :: k} {k0 :: k} (f :: COK vk j k0) (g :: COK vk i j). Obj f -> Obj g -> Companion (OPK hk) (O f g) ~> O (Companion (OPK hk) f) (Companion (OPK hk) g) Source Comments #

compFromCompose :: forall {j1 :: k} {j2 :: k} {k0 :: k} (f :: COK vk j2 k0) (g :: COK vk j1 j2). Obj f -> Obj g -> O (Companion (OPK hk) f) (Companion (OPK hk) g) ~> Companion (OPK hk) (O f g) Source Comments #

CategoryOf (kk j k2) => CategoryOf (COK kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Bicategory.Co type (~>) = Co :: COK kk j k2 -> COK kk j k2 -> Type

(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k2) => Functor (P kk kk (HK kk) :: COK kk h i -> kk j k2 -> HK kk h j +-> HK kk i k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Hom

Methods

map :: forall (a :: COK kk h i) (b :: COK kk h i). (a ~> b) -> P kk kk (HK kk) a ~> P kk kk (HK kk) b Source Comments #

CategoryOf (kk j k2) => Promonad (Co :: COK kk j k2 -> COK kk j k2 -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

id :: forall (a :: COK kk j k2). Ob a => Co a a Source Comments #

(.) :: forall (b :: COK kk j k2) (c :: COK kk j k2) (a :: COK kk j k2). Co b c -> Co a b -> Co a c Source Comments #

CategoryOf (kk j k2) => Profunctor (Co :: COK kk j k2 -> COK kk j k2 -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

dimap :: forall (c :: COK kk j k2) (a :: COK kk j k2) (b :: COK kk j k2) (d :: COK kk j k2). (c ~> a) -> (b ~> d) -> Co a b -> Co c d Source Comments #

(\\) :: forall (a :: COK kk j k2) (b :: COK kk j k2) r. ((Ob a, Ob b) => r) -> Co a b -> r Source Comments #

type Ob0 (COK kk :: s -> s -> Type) (k2 :: k1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type Ob0 (COK kk :: s -> s -> Type) (k2 :: k1) = Ob0 kk k2

type Lan ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type Lan ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) = 'CO (Ran j2 f)

type Lift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type Lift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) = 'CO (Rift j f)

type Ran ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type Ran ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) = 'CO (Lan j2 f)

type Rift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type Rift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) = 'CO (Lift j f)

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type I = 'CO (I :: kk i i)

type O (a :: COK kk k1 k2) (b :: COK kk j k1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type O (a :: COK kk k1 k2) (b :: COK kk j k1) = 'CO (O (UN ('CO :: kk k1 k2 -> COK kk k1 k2) a) (UN ('CO :: kk j k1 -> COK kk j k1) b))

type Companion (COK hk :: k -> k -> Type) (f :: OPK vk j k1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Companion (COK hk :: k -> k -> Type) (f :: OPK vk j k1) = 'CO (Conjoint hk (UN ('OP :: vk k1 j -> OPK vk j k1) f))

type Companion (OPK hk :: k1 -> k1 -> Type) (f :: COK vk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Companion (OPK hk :: k1 -> k1 -> Type) (f :: COK vk j k2) = 'OP (Conjoint hk (UN ('CO :: vk j k2 -> COK vk j k2) f))

type Conjoint (COK hk :: k -> k -> Type) (f :: OPK vk k1 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Conjoint (COK hk :: k -> k -> Type) (f :: OPK vk k1 j) = 'CO (Companion hk (UN ('OP :: vk j k1 -> OPK vk k1 j) f))

type Conjoint (OPK hk :: k1 -> k1 -> Type) (f :: COK vk k2 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Conjoint (OPK hk :: k1 -> k1 -> Type) (f :: COK vk k2 j) = 'OP (Companion hk (UN ('CO :: vk k2 j -> COK vk k2 j) f))

type UN ('CO :: kk j k2 -> COK kk j k2) ('CO k3 :: COK kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type UN ('CO :: kk j k2 -> COK kk j k2) ('CO k3 :: COK kk j k2) = k3

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type (~>) = Co :: COK kk j k2 -> COK kk j k2 -> Type

type Ob (a :: COK kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type Ob (a :: COK kk j k2) = (Is ('CO :: kk j k2 -> COK kk j k2) a, Ob (UN ('CO :: kk j k2 -> COK kk j k2) a))

data Co (a :: COK kk j k1) (b :: COK kk j k1) where Source Comments #

Constructors

Co :: forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1) (a1 :: kk j k1). (b1 ~> a1) -> Co ('CO a1) ('CO b1)

Instances

Instances details

CategoryOf (kk j k2) => Promonad (Co :: COK kk j k2 -> COK kk j k2 -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Co Methods id :: forall (a :: COK kk j k2). Ob a => Co a a Source Comments # (.) :: forall (b :: COK kk j k2) (c :: COK kk j k2) (a :: COK kk j k2). Co b c -> Co a b -> Co a c Source Comments #
CategoryOf (kk j k2) => Profunctor (Co :: COK kk j k2 -> COK kk j k2 -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Co Methods dimap :: forall (c :: COK kk j k2) (a :: COK kk j k2) (b :: COK kk j k2) (d :: COK kk j k2). (c ~> a) -> (b ~> d) -> Co a b -> Co c d Source Comments # (\\) :: forall (a :: COK kk j k2) (b :: COK kk j k2) r. ((Ob a, Ob b) => r) -> Co a b -> r Source Comments #