Safe Haskell	None
Language	GHC2024

Proarrow.Category.Bicategory.Co

Documentation

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

Constructors

CO (kk j k1)

Instances

Instances details

WithObO2 Tight kk => WithObO2 Cotight (COK kk :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

withObO2 :: forall {i :: s} {j :: s} {k :: s} (a :: COK kk j k) (b :: COK kk i j) r. (Ob a, Ob b, IsOb Cotight a, IsOb Cotight b) => ((IsOb Cotight (O a b), Ob (O a b)) => r) -> r Source Comments #

WithObO2 Cotight kk => WithObO2 Tight (COK kk :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

withObO2 :: forall {i :: s} {j :: s} {k :: s} (a :: COK kk j k) (b :: COK kk i j) r. (Ob a, Ob b, IsOb Tight a, IsOb Tight b) => ((IsOb Tight (O a b), Ob (O a b)) => r) -> r Source Comments #

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

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 #

withOb2 :: forall {i :: s} {j :: s} {k :: s} (a :: COK kk j k) (b :: COK kk i j) r. (Ob a, Ob b, Ob0 (COK kk) i, Ob0 (COK kk) j, Ob0 (COK kk) k) => (Ob (O a b) => r) -> r Source Comments #

withOb0s :: forall {j :: s} {k :: s} (a :: COK kk j k) r. Ob a => ((Ob0 (COK kk) j, Ob0 (COK kk) k) => r) -> r 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 #

Equipment kk => Equipment (COK kk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

withCotightAdjoint :: forall {j :: k} {k1 :: k} (f :: COK kk j k1) r. IsTight f => ((Adjunction f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments #

withTightAdjoint :: forall {j :: k} {k1 :: k} (f :: COK kk j k1) r. IsCotight f => ((Adjunction (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r 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 #

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 IsOb Cotight (p :: COK kk i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type IsOb Cotight (p :: COK kk i j) = IsOb Tight (UN ('CO :: kk i j -> COK kk i j) p)

type IsOb Tight (p :: COK kk i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type IsOb Tight (p :: COK kk i j) = IsOb Cotight (UN ('CO :: kk i j -> COK kk i j) p)

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 CotightAdjoint (p :: COK kk k2 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type CotightAdjoint (p :: COK kk k2 j) = 'CO (TightAdjoint (UN ('CO :: kk k2 j -> COK kk k2 j) p))

type TightAdjoint (p :: COK kk k2 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

type TightAdjoint (p :: COK kk k2 j) = 'CO (CotightAdjoint (UN ('CO :: kk k2 j -> COK kk k2 j) p))

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