Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory

Contents

Bicategories
More

Synopsis

class (Locally CategoryOf kk, CategoryOf s) => Bicategory (kk :: CAT s) where
- type Ob0 (kk :: CAT s) (j :: k)
- type I :: kk i i
- type O (p :: kk j k) (q :: kk i j) :: kk i k
- iObj :: forall (i :: s). Ob0 kk i => Obj (I :: kk i i)
- o :: forall {i :: s} (j :: s) (k :: s) (a :: kk j k) (b :: kk j k) (c :: kk i j) (d :: kk i j). (a ~> b) -> (c ~> d) -> O a c ~> O b d
- (\\\) :: forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r. ((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
- leftUnitor :: forall {i :: s} {j :: s} (a :: kk i j). (Ob0 kk i, Ob0 kk j, Ob a) => O (I :: kk j j) a ~> a
- leftUnitorInv :: forall {i :: s} {j :: s} (a :: kk i j). (Ob0 kk i, Ob0 kk j, Ob a) => a ~> O (I :: kk j j) a
- rightUnitor :: forall {i :: s} {j :: s} (a :: kk i j). (Ob0 kk i, Ob0 kk j, Ob a) => O a (I :: kk i i) ~> a
- rightUnitorInv :: forall {i :: s} {j :: s} (a :: kk i j). (Ob0 kk i, Ob0 kk j, Ob a) => a ~> O a (I :: kk i i)
- associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: kk j k) (b :: kk i j) (c :: kk h i). (Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b, Ob c) => O (O a b) c ~> O a (O b c)
- associatorInv :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: kk j k) (b :: kk i j) (c :: kk h i). (Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c
(==) :: forall k (a :: k) (b :: k) (c :: k). CategoryOf k => (a ~> b) -> (b ~> c) -> a ~> c
(||) :: forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s) (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2). Bicategory kk => (a ~> b) -> (c ~> d) -> O a c ~> O b d
appendObj :: forall {s} {kk :: s -> s -> Type} {i :: s} {j :: s} {k :: s} (a :: kk j k) (b :: kk i j) r. (Bicategory kk, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b) => (Ob (O a b) => r) -> r
leftUnitor' :: forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j) (b :: kk i j). Bicategory kk => (a ~> b) -> O (I :: kk j j) a ~> b
leftUnitorInv' :: forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j) (b :: kk i j). Bicategory kk => (a ~> b) -> a ~> O (I :: kk j j) b
rightUnitor' :: forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j) (b :: kk i j). Bicategory kk => (a ~> b) -> O a (I :: kk i i) ~> b
rightUnitorInv' :: forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j) (b :: kk i j). Bicategory kk => (a ~> b) -> a ~> O b (I :: kk i i)
associator' :: forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s} {j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1). Bicategory kk => Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associatorInv' :: forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s} {j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1). Bicategory kk => Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
leftUnitorWith :: forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2) (a :: kk i1 i2) (b :: kk i1 i2). Bicategory kk => (c ~> (I :: kk i2 i2)) -> (a ~> b) -> O c a ~> b
leftUnitorInvWith :: forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2) (a :: kk i1 i2) (b :: kk i1 i2). Bicategory kk => ((I :: kk i2 i2) ~> c) -> (a ~> b) -> a ~> O c b
rightUnitorWith :: forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i) (a :: kk i k) (b :: kk i k). Bicategory kk => (c ~> (I :: kk i i)) -> (a ~> b) -> O a c ~> b
rightUnitorInvWith :: forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i) (a :: kk i k) (b :: kk i k). Bicategory kk => ((I :: kk i i) ~> c) -> (a ~> b) -> a ~> O b c
class Ob0 kk j => Ob0' (kk :: CAT s) (j :: k)
class (Ob0 kk j, Ob0 kk k1, Ob a) => Ob' (a :: kk j k1)
class (Bicategory kk, Ob0 kk a) => Monad (t :: kk a a) where
- eta :: (I :: kk a a) ~> t
- mu :: O t t ~> t
class (Bicategory kk, Ob0 kk a) => Comonad (t :: kk a a) where
- epsilon :: t ~> (I :: kk a a)
- delta :: t ~> O t t
class (Bicategory kk, Ob0 kk c, Ob0 kk d) => Adjunction (l :: kk c d) (r :: kk d c) where
- unit :: (I :: kk c c) ~> O r l
- counit :: O l r ~> (I :: kk d d)
leftAdjunct :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s} (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d). (Adjunction l r, Ob a, Ob r, Ob l, Ob0 kk i) => (O l a ~> b) -> a ~> O r b
rightAdjunct :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s} (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d). (Adjunction l r, Ob b, Ob r, Ob l, Ob0 kk i) => (a ~> O r b) -> O l a ~> b
class (Monad s, Monad t) => Bimodule (s :: kk a a) (t :: kk b b) (p :: kk b a) where
- leftAction :: O s p ~> p
- rightAction :: O p t ~> p

Bicategories

class (Locally CategoryOf kk, CategoryOf s) => Bicategory (kk :: CAT s) where Source Comments #

Bicategories.

0-cells are kinds i, j, k... satisfying the Ob0 kk constraint.
1-cells are types of kind kk j k for any 0-cells j and k, satisfying the Ob constraint.
2-cells are values of type p ~> q, where p and q are 1-cells.

Minimal complete definition

o, (\\\), leftUnitor, leftUnitorInv, rightUnitor, rightUnitorInv, associator, associatorInv

Associated Types

type Ob0 (kk :: CAT s) (j :: k) Source Comments #

type Ob0 (kk :: CAT s) (j :: k) = ()

type I :: kk i i Source Comments #

type O (p :: kk j k) (q :: kk i j) :: kk i k Source Comments #

Methods

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

The identity 1-cell (as represented by an identity 2-cell).

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

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

Horizontal composition of 2-cells.

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

Observe constraints from a 2-cell value.

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

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

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

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

associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: kk j k) (b :: kk i j) (c :: kk h i). (Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 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 :: kk j k) (b :: kk i j) (c :: kk h i). (Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

Instances

Instances details

Bicategory Unit Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

Associated Types

type Ob0 Unit (k :: ())
Instance details Defined in Proarrow.Category.Bicategory.Terminal type Ob0 Unit (k :: ()) = k ~ '()
type I
Instance details Defined in Proarrow.Category.Bicategory.Terminal type I = 'Unit
type O (a :: Unit j '()) (b :: Unit '() j)
Instance details Defined in Proarrow.Category.Bicategory.Terminal type O (a :: Unit j '()) (b :: Unit '() j) = 'Unit

Methods

iObj :: forall (i :: ()). Ob0 Unit i => Obj (I :: Unit i i) Source Comments #

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

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

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

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

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

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

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

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

Bicategory PROFK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Ob0 PROFK (k :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Ob0 PROFK (k :: Type) = CategoryOf k
type I
Instance details Defined in Proarrow.Category.Bicategory.Prof type I = 'PK (Id :: i -> i -> Type)
type O (p :: PROFK k1 k2) (q :: PROFK j k1)
Instance details Defined in Proarrow.Category.Bicategory.Prof type O (p :: PROFK k1 k2) (q :: PROFK j k1) = 'PK (UN ('PK :: (k1 +-> k2) -> PROFK k1 k2) p :.: UN ('PK :: (j +-> k1) -> PROFK j k1) q)

Methods

iObj :: Ob0 PROFK i => Obj (I :: PROFK i i) Source Comments #

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

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

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

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

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

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

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

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

Monoidal k => Bicategory (MonK k :: () -> () -> Type) Source Comments #

A monoidal category as a bicategory.

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

iObj :: forall (i :: ()). Ob0 (MonK k) i => Obj (I :: MonK k i i) Source Comments #

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

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

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

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

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

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

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

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

CategoryOf k => Bicategory (PLAINK k :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.CategoryAsBi

Methods

iObj :: forall (i :: k). Ob0 (PLAINK k) i => Obj (I :: PLAINK k i i) Source Comments #

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

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

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

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

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

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

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

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

associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: OPK kk j k) (b :: OPK kk i j) (c :: OPK kk h i). (Ob0 (OPK kk) h, Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob0 (OPK 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 :: OPK kk j k) (b :: OPK kk i j) (c :: OPK kk h i). (Ob0 (OPK kk) h, Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob0 (OPK kk) k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

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

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

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

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

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

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

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

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

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

associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: Path kk j k) (b :: Path kk i j) (c :: Path kk h i). (Ob0 (Path kk) h, Ob0 (Path kk) i, Ob0 (Path kk) j, Ob0 (Path 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 :: Path kk j k) (b :: Path kk i j) (c :: Path kk h i). (Ob0 (Path kk) h, Ob0 (Path kk) i, Ob0 (Path kk) j, Ob0 (Path kk) k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

(Bicategory kk, forall (i :: s). Ob0 kk i => IsObI tag kk i, forall (i :: s) (j :: s) (k :: s) (a :: kk j k) (b :: kk i j). (IsOb tag a, IsOb tag b) => IsObO tag kk i j k a b) => Bicategory (SUBCAT tag kk :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

Methods

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

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

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

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

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

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

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

associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: SUBCAT tag kk j k) (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk h i). (Ob0 (SUBCAT tag kk) h, Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob0 (SUBCAT tag 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 :: SUBCAT tag kk j k) (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk h i). (Ob0 (SUBCAT tag kk) h, Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob0 (SUBCAT tag kk) k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

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

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

Methods

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

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

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

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

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

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

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

associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: WKK kk j k) (b :: WKK kk i j) (c :: WKK kk h i). (Ob0 (WKK kk) h, Ob0 (WKK kk) i, Ob0 (WKK kk) j, Ob0 (WKK 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 :: WKK kk j k) (b :: WKK kk i j) (c :: WKK kk h i). (Ob0 (WKK kk) h, Ob0 (WKK kk) i, Ob0 (WKK kk) j, Ob0 (WKK kk) k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

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

Instance details

Defined in Proarrow.Category.Equipment.Quintet

Methods

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

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

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

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

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

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

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

associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: QKK kk j k) (b :: QKK kk i j) (c :: QKK kk h i). (Ob0 (QKK kk) h, Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob0 (QKK 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 :: QKK kk j k) (b :: QKK kk i j) (c :: QKK kk h i). (Ob0 (QKK kk) h, Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob0 (QKK kk) k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

(Bicategory jj, Bicategory kk) => Bicategory (PRODK jj kk :: (j, k) -> (j, k) -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

iObj :: forall (i :: (j, k)). Ob0 (PRODK jj kk) i => Obj (I :: PRODK jj kk i i) Source Comments #

o :: forall {i :: (j, k)} (j0 :: (j, k)) (k0 :: (j, k)) (a :: PRODK jj kk j0 k0) (b :: PRODK jj kk j0 k0) (c :: PRODK jj kk i j0) (d :: PRODK jj kk i j0). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

(\\\) :: forall (i :: (j, k)) (j0 :: (j, k)) (ps :: PRODK jj kk i j0) (qs :: PRODK jj kk i j0) r. ((Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j0, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r Source Comments #

leftUnitor :: forall {i :: (j, k)} {j0 :: (j, k)} (a :: PRODK jj kk i j0). (Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j0, Ob a) => O (I :: PRODK jj kk j j) a ~> a Source Comments #

leftUnitorInv :: forall {i :: (j, k)} {j0 :: (j, k)} (a :: PRODK jj kk i j0). (Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j0, Ob a) => a ~> O (I :: PRODK jj kk j j) a Source Comments #

rightUnitor :: forall {i :: (j, k)} {j0 :: (j, k)} (a :: PRODK jj kk i j0). (Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j0, Ob a) => O a (I :: PRODK jj kk i i) ~> a Source Comments #

rightUnitorInv :: forall {i :: (j, k)} {j0 :: (j, k)} (a :: PRODK jj kk i j0). (Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j0, Ob a) => a ~> O a (I :: PRODK jj kk i i) Source Comments #

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

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

(==) :: forall k (a :: k) (b :: k) (c :: k). CategoryOf k => (a ~> b) -> (b ~> c) -> a ~> c infixl 7 Source Comments #

(||) :: forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s) (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2). Bicategory kk => (a ~> b) -> (c ~> d) -> O a c ~> O b d infixl 8 Source Comments #

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

leftUnitor' :: forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j) (b :: kk i j). Bicategory kk => (a ~> b) -> O (I :: kk j j) a ~> b Source Comments #

leftUnitorInv' :: forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j) (b :: kk i j). Bicategory kk => (a ~> b) -> a ~> O (I :: kk j j) b Source Comments #

rightUnitor' :: forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j) (b :: kk i j). Bicategory kk => (a ~> b) -> O a (I :: kk i i) ~> b Source Comments #

rightUnitorInv' :: forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j) (b :: kk i j). Bicategory kk => (a ~> b) -> a ~> O b (I :: kk i i) Source Comments #

associator' :: forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s} {j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1). Bicategory kk => Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c) Source Comments #

associatorInv' :: forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s} {j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1). Bicategory kk => Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c Source Comments #

leftUnitorWith :: forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2) (a :: kk i1 i2) (b :: kk i1 i2). Bicategory kk => (c ~> (I :: kk i2 i2)) -> (a ~> b) -> O c a ~> b Source Comments #

leftUnitorInvWith :: forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2) (a :: kk i1 i2) (b :: kk i1 i2). Bicategory kk => ((I :: kk i2 i2) ~> c) -> (a ~> b) -> a ~> O c b Source Comments #

rightUnitorWith :: forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i) (a :: kk i k) (b :: kk i k). Bicategory kk => (c ~> (I :: kk i i)) -> (a ~> b) -> O a c ~> b Source Comments #

rightUnitorInvWith :: forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i) (a :: kk i k) (b :: kk i k). Bicategory kk => ((I :: kk i i) ~> c) -> (a ~> b) -> a ~> O b c Source Comments #

class Ob0 kk j => Ob0' (kk :: CAT s) (j :: k) Source Comments #

Instances

Instances details

Ob0 kk j => Ob0' (kk :: CAT s) (j :: k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory

class (Ob0 kk j, Ob0 kk k1, Ob a) => Ob' (a :: kk j k1) Source Comments #

Instances

Instances details

(Ob0 kk j, Ob0 kk k2, Ob a) => Ob' (a :: kk j k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory

More

class (Bicategory kk, Ob0 kk a) => Monad (t :: kk a a) where Source Comments #

Methods

eta :: (I :: kk a a) ~> t Source Comments #

mu :: O t t ~> t Source Comments #

Instances

Instances details

Monad 'Unit Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Terminal Methods eta :: (I :: Unit '() '()) ~> 'Unit Source Comments # mu :: O 'Unit 'Unit ~> 'Unit Source Comments #
Promonad p => Monad ('PK p :: PROFK k k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods eta :: (I :: PROFK k k) ~> 'PK p Source Comments # mu :: O ('PK p) ('PK p) ~> 'PK p Source Comments #
(Monad m, Comonad c, LaxProfunctor sk tk kk, Ob c, Ob m) => Monad ('PK (P sk tk kk ('CO c) m) :: PROFK (kk i j) (kk i j)) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods eta :: (I :: PROFK (kk i j) (kk i j)) ~> 'PK (P sk tk kk ('CO c) m) Source Comments # mu :: O ('PK (P sk tk kk ('CO c) m)) ('PK (P sk tk kk ('CO c) m)) ~> 'PK (P sk tk kk ('CO c) m) Source Comments #
Monoid m => Monad ('MK m :: MonK k a a) Source Comments #	Monoids in a monoidal category are monads when the monoidal category is seen as a bicategory.
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi Methods eta :: (I :: MonK k a a) ~> ('MK m :: MonK k a a) Source Comments # mu :: O ('MK m :: MonK k a a) ('MK m :: MonK k a a) ~> ('MK m :: MonK k a a) Source Comments #
(Bicategory kk, Ob0 kk a) => Monad ('Nil :: Path kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified Methods eta :: (I :: Path kk a a) ~> ('Nil :: Path kk a a) Source Comments # mu :: O ('Nil :: Path kk a a) ('Nil :: Path kk a a) ~> ('Nil :: Path kk a a) 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 #
Monad t => Monad ('OP t :: OPK kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Op Methods eta :: (I :: OPK kk a a) ~> 'OP t Source Comments # mu :: O ('OP t) ('OP t) ~> 'OP t Source Comments #
(Monad s, Ob s) => Monad (s '::: ('Nil :: Path kk a a) :: Path kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified Methods eta :: (I :: Path kk a a) ~> (s '::: ('Nil :: Path kk a a)) Source Comments # mu :: O (s '::: ('Nil :: Path kk a a)) (s '::: ('Nil :: Path kk a a)) ~> (s '::: ('Nil :: Path kk a a)) Source Comments #
(Adjunction l r, Ob r, Ob l) => Monad (l '::: (r '::: ('Nil :: Path kk a a)) :: Path kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified Methods eta :: (I :: Path kk a a) ~> (l '::: (r '::: ('Nil :: Path kk a a))) Source Comments # mu :: O (l '::: (r '::: ('Nil :: Path kk a a))) (l '::: (r '::: ('Nil :: Path kk a a))) ~> (l '::: (r '::: ('Nil :: Path kk a a))) Source Comments #
(Monad (PRODFST m), Monad (PRODSND m), Ob m) => Monad (m :: PRODK jj kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Product Methods eta :: (I :: PRODK jj kk a a) ~> m Source Comments # mu :: O m m ~> m Source Comments #

class (Bicategory kk, Ob0 kk a) => Comonad (t :: kk a a) where Source Comments #

Methods

epsilon :: t ~> (I :: kk a a) Source Comments #

delta :: t ~> O t t Source Comments #

Instances

Instances details

Procomonad p => Comonad ('PK p :: PROFK k k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods epsilon :: 'PK p ~> (I :: PROFK k k) Source Comments # delta :: 'PK p ~> O ('PK p) ('PK p) Source Comments #
Comonoid m => Comonad ('MK m :: MonK k a a) Source Comments #	Comonoids in a monoidal category are comonads when the monoidal category is seen as a bicategory.
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi Methods epsilon :: ('MK m :: MonK k a a) ~> (I :: MonK k a a) Source Comments # delta :: ('MK m :: MonK k a a) ~> O ('MK m :: MonK k a a) ('MK m :: MonK k a a) Source Comments #
(Bicategory kk, Ob0 kk a) => Comonad ('Nil :: Path kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified Methods epsilon :: ('Nil :: Path kk a a) ~> (I :: Path kk a a) Source Comments # delta :: ('Nil :: Path kk a a) ~> O ('Nil :: Path kk a a) ('Nil :: Path kk a a) 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 t => Comonad ('OP t :: OPK kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Op Methods epsilon :: 'OP t ~> (I :: OPK kk a a) Source Comments # delta :: 'OP t ~> O ('OP t) ('OP t) Source Comments #
(Adjunction l r, Ob r, Ob l) => Comonad (r '::: (l '::: ('Nil :: Path kk a a)) :: Path kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified Methods epsilon :: (r '::: (l '::: ('Nil :: Path kk a a))) ~> (I :: Path kk a a) Source Comments # delta :: (r '::: (l '::: ('Nil :: Path kk a a))) ~> O (r '::: (l '::: ('Nil :: Path kk a a))) (r '::: (l '::: ('Nil :: Path kk a a))) Source Comments #
(Comonad (PRODFST m), Comonad (PRODSND m), Ob m) => Comonad (m :: PRODK jj kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Product Methods epsilon :: m ~> (I :: PRODK jj kk a a) Source Comments # delta :: m ~> O m m Source Comments #

class (Bicategory kk, Ob0 kk c, Ob0 kk d) => Adjunction (l :: kk c d) (r :: kk d c) where Source Comments #

Methods

unit :: (I :: kk c c) ~> O r l Source Comments #

counit :: O l r ~> (I :: kk d d) Source Comments #

Instances

Instances details

Adjunction l r => Adjunction ('PK l :: PROFK c d) ('PK r :: PROFK d c) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods unit :: (I :: PROFK c c) ~> O ('PK r) ('PK l) Source Comments # counit :: O ('PK l) ('PK r) ~> (I :: PROFK d d) Source Comments #
(CompactClosed k, Ob a, b ~ Dual a) => Adjunction ('MK a :: MonK k c d) ('MK b :: MonK k d c) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi Methods unit :: (I :: MonK k c c) ~> O ('MK b :: MonK k d c) ('MK a :: MonK k c d) Source Comments # counit :: O ('MK a :: MonK k c d) ('MK b :: MonK k d c) ~> (I :: MonK k d d) 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 #
Adjunction f g => Adjunction ('OP g :: OPK kk k2 j) ('OP f :: OPK kk j k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Op Methods unit :: (I :: OPK kk k2 k2) ~> O ('OP f) ('OP g) Source Comments # counit :: O ('OP g) ('OP f) ~> (I :: OPK kk j j) Source Comments #
(Adjunction (PRODFST l) (PRODFST r), Adjunction (PRODSND l) (PRODSND r), Ob l, Ob r) => Adjunction (l :: PRODK jj kk c d) (r :: PRODK jj kk d c) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Product Methods unit :: (I :: PRODK jj kk c c) ~> O r l Source Comments # counit :: O l r ~> (I :: PRODK jj kk d d) Source Comments #

leftAdjunct :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s} (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d). (Adjunction l r, Ob a, Ob r, Ob l, Ob0 kk i) => (O l a ~> b) -> a ~> O r b Source Comments #

rightAdjunct :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s} (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d). (Adjunction l r, Ob b, Ob r, Ob l, Ob0 kk i) => (a ~> O r b) -> O l a ~> b Source Comments #

class (Monad s, Monad t) => Bimodule (s :: kk a a) (t :: kk b b) (p :: kk b a) where Source Comments #

Methods

leftAction :: O s p ~> p Source Comments #

rightAction :: O p t ~> p Source Comments #

Instances

Instances details

Monad s => Bimodule (s :: kk b b) (s :: kk b b) (s :: kk b b) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory Methods leftAction :: O s s ~> s Source Comments # rightAction :: O s s ~> s Source Comments #
(Category cj, Category ck, Profunctor p) => Bimodule ('PK ck :: PROFK k k) ('PK cj :: PROFK j j) ('PK p :: PROFK j k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods leftAction :: O ('PK ck) ('PK p) ~> 'PK p Source Comments # rightAction :: O ('PK p) ('PK cj) ~> 'PK p Source Comments #
Bimodule s t p => Bimodule ('OP t :: OPK kk k2 k2) ('OP s :: OPK kk j j) ('OP p :: OPK kk j k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Op Methods leftAction :: O ('OP t) ('OP p) ~> 'OP p Source Comments # rightAction :: O ('OP p) ('OP s) ~> 'OP p Source Comments #