Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory

Contents

Bicategories
Paths
More

Synopsis

class BicategoryConstraints kk => Bicategory (kk :: CAT k) where
- type Ob0 (kk :: CAT k) (j :: k1)
- type I :: kk i i
- type O (p :: kk i j) (q :: kk j k1) :: kk i k1
- o :: forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j) (c :: kk j k1) (d :: kk j k1). (a ~> b) -> (c ~> d) -> O a c ~> O b d
- (\\\) :: forall (i :: k) (j :: k) (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 :: k) (j :: k) (a :: kk i j). Obj a -> O (I :: kk i i) a ~> a
- leftUnitorInv :: forall (i :: k) (j :: k) (a :: kk i j). Obj a -> a ~> O (I :: kk i i) a
- rightUnitor :: forall (i :: k) (j :: k) (a :: kk i j). Obj a -> O a (I :: kk j j) ~> a
- rightUnitorInv :: forall (i :: k) (j :: k) (a :: kk i j). Obj a -> a ~> O a (I :: kk j j)
- associator :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1). Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
- associatorInv :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1). Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
class (forall (j :: k) (k1 :: k). (Ob0 kk j, Ob0 kk k1) => CategoryOf (kk j k1), forall (i :: k). Ob0 kk i => IIsOb kk i) => BicategoryConstraints (kk :: CAT k)
class Ob (I :: kk i i) => IIsOb (kk :: k -> k -> Type) (i :: k)
appendObj :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (a :: kk i j) (b :: kk j k2) r. (Bicategory kk, Ob0 kk i, Ob0 kk j, Ob0 kk k2, Ob a, Ob b) => (Ob (O a b) => r) -> r
data Path (kk :: CAT k) (j :: k) (k1 :: k) where
- Nil :: forall {k} (kk :: CAT k) (j :: k). Path kk j j
- (:::) :: forall {k} (kk :: CAT k) (j :: k) (j1 :: k) (k1 :: k). kk j j1 -> Path kk j1 k1 -> Path kk j k1
data SPath (ps :: Path kk j k1) where
- SNil :: forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath ('Nil :: Path kk j j)
- SCons :: forall {k} {k1 :: k} {kk :: CAT k} {j :: k} {k2 :: k} (p :: kk j k2) (ps1 :: Path kk k2 k1). (Ob0 kk j, Ob0 kk k2) => Obj p -> SPath ps1 -> SPath (p '::: ps1)
class IsPath (ps :: Path kk j k1) where
- singPath :: SPath ps
asObj :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j). Bicategory kk => SPath ps -> Obj ps
asSPath :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j). Bicategory kk => Obj ps -> SPath ps
type family (ps :: Path kk a b) +++ (qs :: Path kk b c) :: Path kk a c
append :: forall {k1} {kk :: CAT k1} {j :: k1} {b :: k1} {k2 :: k1} (ps :: Path kk j b) (qs :: Path kk b k2). SPath ps -> SPath qs -> SPath (ps +++ qs)
withAssoc :: forall {k1} {kk :: CAT k1} {h :: k1} {i :: k1} {j :: k1} {k2 :: k1} (a :: Path kk h i) (b :: Path kk i j) (c :: Path kk j k2) r. Bicategory kk => Obj a -> Obj b -> Obj c -> (((a +++ b) +++ c) ~ (a +++ (b +++ c)) => r) -> r
withUnital :: forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} (a :: Path kk j k2) r. Bicategory kk => Obj a -> ((a +++ ('Nil :: Path kk k2 k2)) ~ a => r) -> r
data Strictified (ps :: Path kk j k1) (qs :: Path kk j k1) where
- Str :: forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1) (qs :: Path kk j k1). (Ob ps, Ob qs, Ob0 kk j, Ob0 kk k1) => (Fold ps ~> Fold qs) -> Strictified ps qs
type family Fold (as :: Path kk j k1) :: kk j k1
fold :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j). Bicategory kk => SPath as -> Fold as ~> Fold as
obj1 :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j). (Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) => Obj (p '::: ('Nil :: Path kk j j))
concatFold :: forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1} (as :: Path kk i j) (bs :: Path kk j k2). (Ob as, Ob bs, Ob0 kk i, Ob0 kk j, Ob0 kk k2, Bicategory kk) => O (Fold as) (Fold bs) ~> Fold (as +++ bs)
splitFold :: forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1} (as :: Path kk i j) (bs :: Path kk j k2). (Ob as, Ob bs, Ob0 kk i, Ob0 kk j, Ob0 kk k2, Bicategory kk) => Fold (as +++ bs) ~> O (Fold as) (Fold bs)
introI :: forall {k} {kk :: CAT k} {j :: k}. (Ob0 kk j, Bicategory kk) => ('Nil :: Path kk j j) ~> ((I :: kk j j) '::: ('Nil :: Path kk j j))
elimI :: forall {k} {kk :: CAT k} {j :: k}. (Ob0 kk j, Bicategory kk) => ((I :: kk j j) '::: ('Nil :: Path kk j j)) ~> ('Nil :: Path kk j j)
introO :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (p :: kk i j) (q :: kk j k2). (Ob0 kk i, Ob0 kk j, Ob0 kk k2, Bicategory kk, Ob p, Ob q) => (p '::: (q '::: ('Nil :: Path kk k2 k2))) ~> (O p q '::: ('Nil :: Path kk k2 k2))
elimO :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (p :: kk i j) (q :: kk j k2). (Ob0 kk i, Ob0 kk j, Ob0 kk k2, Bicategory kk, Ob p, Ob q) => (O p q '::: ('Nil :: Path kk k2 k2)) ~> (p '::: (q '::: ('Nil :: Path kk k2 k2)))
class (Bicategory kk, Ob0 kk a, Ob t) => Monad (t :: kk a a) where
- eta :: (I :: kk a a) ~> t
- mu :: O t t ~> t
class (Bicategory kk, Ob0 kk a, Ob t) => 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, Ob l, Ob r) => Adjunction (l :: kk c d) (r :: kk d c) where
- unit :: (I :: kk d d) ~> O r l
- counit :: O l r ~> (I :: kk c c)
class (Monad s, Monad t) => Bimodule (s :: kk a a) (t :: kk b b) (p :: kk a b) where
- leftAction :: O s p ~> p
- rightAction :: O p t ~> p

Bicategories

class BicategoryConstraints kk => Bicategory (kk :: CAT k) 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.

Associated Types

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

type Ob0 (kk :: CAT k) (j :: k1) = Any j

type I :: kk i i Source Comments #

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

Methods

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

Horizontal composition of 2-cells.

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

Observe constraints from a 2-cell value.

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

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

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

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

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

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

Instances

Instances details

Bicategory TERMK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Terminal

Associated Types

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

Methods

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

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

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

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

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

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

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

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

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 #

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

A monoidal category as a bicategory.

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

o :: forall {k1 :: ()} (i :: ()) (j :: ()) (a :: MonK k i j) (b :: MonK k i j) (c :: MonK k j k1) (d :: MonK k j k1). (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). Obj a -> O (I :: MonK k i i) a ~> a Source Comments #

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

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

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

associator :: forall {j1 :: ()} {k1 :: ()} (i :: ()) (j2 :: ()) (a :: MonK k i j2) (b :: MonK k j2 j1) (c :: MonK k 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 :: MonK k i j2) (b :: MonK k j2 j1) (c :: MonK k j1 k1). Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c Source Comments #

(forall i j k (p :: PRO i j) (q :: PRO j k). (ProfConstraint cl p, ProfConstraint cl q) => ComposeConstraint cl i j k p q) => Bicategory (ProfK cl :: Type -> Type -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

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

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

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

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

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

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

associator :: forall {j1} {k1} i j2 (a :: ProfK cl i j2) (b :: ProfK cl j2 j1) (c :: ProfK cl 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 :: ProfK cl i j2) (b :: ProfK cl j2 j1) (c :: ProfK cl j1 k1). Obj a -> Obj b -> Obj 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

o :: forall {k1 :: k} (i :: k) (j :: k) (a :: PLAINK k i j) (b :: PLAINK k i j) (c :: PLAINK k j k1) (d :: PLAINK k j k1). (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). Obj a -> O (I :: PLAINK k i i) a ~> a Source Comments #

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory

Methods

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

(\\\) :: forall (i :: k) (j :: k) (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 :: k) (j :: k) (a :: Path kk i j). Obj a -> O (I :: Path kk i i) a ~> a Source Comments #

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

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

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

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

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

Bicategory kk => Bicategory (COK kk :: k -> k -> 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 {k1 :: k} (i :: k) (j :: k) (a :: COK kk i j) (b :: COK kk i j) (c :: COK kk j k1) (d :: COK kk j k1). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

(\\\) :: forall (i :: k) (j :: k) (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 :: k) (j :: k) (a :: COK kk i j). Obj a -> O (I :: COK kk i i) a ~> a Source Comments #

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

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

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

(\\\) :: forall (i :: k) (j :: k) (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 :: k) (j :: k) (a :: OPK kk i j). Obj a -> O (I :: OPK kk i i) a ~> a Source Comments #

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Sub

Methods

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

(\\\) :: forall (i :: k) (j :: k) (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 :: k) (j :: k) (a :: SUBCAT tag kk i j). Obj a -> O (I :: SUBCAT tag kk i i) a ~> a Source Comments #

leftUnitorInv :: forall (i :: k) (j :: k) (a :: SUBCAT tag kk i j). Obj a -> a ~> O (I :: SUBCAT tag kk i i) a Source Comments #

rightUnitor :: forall (i :: k) (j :: k) (a :: SUBCAT tag kk i j). Obj a -> O a (I :: SUBCAT tag kk j j) ~> a Source Comments #

rightUnitorInv :: forall (i :: k) (j :: k) (a :: SUBCAT tag kk i j). Obj a -> a ~> O a (I :: SUBCAT tag kk j j) Source Comments #

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

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

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

Instance details

Defined in Proarrow.Category.Double.Quintet

Methods

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

(\\\) :: forall (i :: k) (j :: k) (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 :: k) (j :: k) (a :: QKK kk i j). Obj a -> O (I :: QKK kk i i) a ~> a Source Comments #

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

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

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

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

associatorInv :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: QKK kk i j2) (b :: QKK kk j2 j1) (c :: QKK kk j1 k1). Obj a -> Obj b -> Obj 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

o :: forall {k1 :: (j, k)} (i :: (j, k)) (j0 :: (j, k)) (a :: PRODK jj kk i j0) (b :: PRODK jj kk i j0) (c :: PRODK jj kk j0 k1) (d :: PRODK jj kk j0 k1). (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). Obj a -> O (I :: PRODK jj kk i i) a ~> a Source Comments #

leftUnitorInv :: forall (i :: (j, k)) (j0 :: (j, k)) (a :: PRODK jj kk i j0). Obj a -> a ~> O (I :: PRODK jj kk i i) a Source Comments #

rightUnitor :: forall (i :: (j, k)) (j0 :: (j, k)) (a :: PRODK jj kk i j0). Obj a -> O a (I :: PRODK jj kk j j) ~> a Source Comments #

rightUnitorInv :: forall (i :: (j, k)) (j0 :: (j, k)) (a :: PRODK jj kk i j0). Obj a -> a ~> O a (I :: PRODK jj kk j j) Source Comments #

associator :: forall {j1 :: (j, k)} {k1 :: (j, k)} (i :: (j, k)) (j2 :: (j, k)) (a :: PRODK jj kk i j2) (b :: PRODK jj kk j2 j1) (c :: PRODK jj kk j1 k1). Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c) Source Comments #

associatorInv :: forall {j1 :: (j, k)} {k1 :: (j, k)} (i :: (j, k)) (j2 :: (j, k)) (a :: PRODK jj kk i j2) (b :: PRODK jj kk j2 j1) (c :: PRODK jj kk j1 k1). Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c Source Comments #

class (forall (j :: k) (k1 :: k). (Ob0 kk j, Ob0 kk k1) => CategoryOf (kk j k1), forall (i :: k). Ob0 kk i => IIsOb kk i) => BicategoryConstraints (kk :: CAT k) Source Comments #

Instances

Instances details

(forall (j :: k) (k1 :: k). (Ob0 kk j, Ob0 kk k1) => CategoryOf (kk j k1), forall (i :: k). Ob0 kk i => IIsOb kk i) => BicategoryConstraints (kk :: CAT k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory

class Ob (I :: kk i i) => IIsOb (kk :: k -> k -> Type) (i :: k) Source Comments #

Instances

Instances details

Ob (I :: kk i i) => IIsOb (kk :: k -> k -> Type) (i :: k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory

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

Paths

data Path (kk :: CAT k) (j :: k) (k1 :: k) where Source Comments #

The type of 2-parameter kind constructors.

A type-level kind-threaded list. Used to strictify the bicategory and double category definitions. kk is a kind constructor, which creates a kind given two other kinds. (Each kind representing a 0-cell.)

Constructors

Nil :: forall {k} (kk :: CAT k) (j :: k). Path kk j j
(:::) :: forall {k} (kk :: CAT k) (j :: k) (j1 :: k) (k1 :: k). kk j j1 -> Path kk j1 k1 -> Path kk j k1 infixr 5

Instances

Instances details

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

Instance details

Defined in Proarrow.Category.Bicategory

Methods

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

(\\\) :: forall (i :: k) (j :: k) (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 :: k) (j :: k) (a :: Path kk i j). Obj a -> O (I :: Path kk i i) a ~> a Source Comments #

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

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

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

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

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

(Bicategory (Path kk), Ob0 kk a) => Comonad ('Nil :: Path kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory

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 #

(Bicategory (Path kk), Ob0 kk a) => Monad ('Nil :: Path kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory

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 #

(Adjunction l r, Ob (O l r)) => Comonad (l '::: (r '::: ('Nil :: Path kk a a)) :: Path kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory

Methods

epsilon :: (l '::: (r '::: ('Nil :: Path kk a a))) ~> (I :: Path kk a a) Source Comments #

delta :: (l '::: (r '::: ('Nil :: Path kk a a))) ~> O (l '::: (r '::: ('Nil :: Path kk a a))) (l '::: (r '::: ('Nil :: Path kk a a))) Source Comments #

(Adjunction l r, Ob (O r l)) => Monad (r '::: (l '::: ('Nil :: Path kk a a)) :: Path kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory

Methods

eta :: (I :: Path kk a a) ~> (r '::: (l '::: ('Nil :: Path kk a a))) Source Comments #

mu :: O (r '::: (l '::: ('Nil :: Path kk a a))) (r '::: (l '::: ('Nil :: Path kk a a))) ~> (r '::: (l '::: ('Nil :: Path kk a a))) Source Comments #

(CategoryOf (kk j k2), Ob0 kk j, Ob0 kk k2, Bicategory kk) => CategoryOf (Path kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory

Associated Types

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

(CategoryOf (kk j k2), Ob0 kk j, Ob0 kk k2, Bicategory kk) => Promonad (Strictified :: Path kk j k2 -> Path kk j k2 -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory

Methods

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

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

(CategoryOf (kk j k2), Ob0 kk j, Ob0 kk k2, Bicategory kk) => Profunctor (Strictified :: Path kk j k2 -> Path kk j k2 -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory

Methods

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

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

type Ob0 (Path kk :: k2 -> k2 -> Type) (j :: k1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory

type Ob0 (Path kk :: k2 -> k2 -> Type) (j :: k1) = Ob0 kk j

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory

type I = 'Nil :: Path kk i i

type O (ps :: Path kk a b) (qs :: Path kk b c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory

type O (ps :: Path kk a b) (qs :: Path kk b c) = ps +++ qs

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory

type (~>) = Strictified :: Path kk j k2 -> Path kk j k2 -> Type

type Ob (ps :: Path kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory

type Ob (ps :: Path kk j k2) = (IsPath ps, Ob (Fold ps))

data SPath (ps :: Path kk j k1) where Source Comments #

Constructors

SNil :: forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath ('Nil :: Path kk j j)
SCons :: forall {k} {k1 :: k} {kk :: CAT k} {j :: k} {k2 :: k} (p :: kk j k2) (ps1 :: Path kk k2 k1). (Ob0 kk j, Ob0 kk k2) => Obj p -> SPath ps1 -> SPath (p '::: ps1)

class IsPath (ps :: Path kk j k1) where Source Comments #

Methods

singPath :: SPath ps Source Comments #

Instances

Instances details

Ob0 kk k2 => IsPath ('Nil :: Path kk k2 k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory Methods singPath :: SPath ('Nil :: Path kk k2 k2) Source Comments #
(Ob0 kk i, Ob0 kk j, Ob0 kk k2, Ob p, IsPath ps, Bicategory kk) => IsPath (p '::: ps :: Path kk i k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory Methods singPath :: SPath (p '::: ps) Source Comments #

asObj :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j). Bicategory kk => SPath ps -> Obj ps Source Comments #

asSPath :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j). Bicategory kk => Obj ps -> SPath ps Source Comments #

type family (ps :: Path kk a b) +++ (qs :: Path kk b c) :: Path kk a c infixl 5 Source Comments #

Instances

Instances details

type ('Nil :: Path kk b b) +++ (qs :: Path kk b c) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory type ('Nil :: Path kk b b) +++ (qs :: Path kk b c) = qs
type (p '::: ps :: Path kk i b) +++ (qs :: Path kk b k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory type (p '::: ps :: Path kk i b) +++ (qs :: Path kk b k2) = p '::: (ps +++ qs)

append :: forall {k1} {kk :: CAT k1} {j :: k1} {b :: k1} {k2 :: k1} (ps :: Path kk j b) (qs :: Path kk b k2). SPath ps -> SPath qs -> SPath (ps +++ qs) Source Comments #

withAssoc :: forall {k1} {kk :: CAT k1} {h :: k1} {i :: k1} {j :: k1} {k2 :: k1} (a :: Path kk h i) (b :: Path kk i j) (c :: Path kk j k2) r. Bicategory kk => Obj a -> Obj b -> Obj c -> (((a +++ b) +++ c) ~ (a +++ (b +++ c)) => r) -> r Source Comments #

withUnital :: forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} (a :: Path kk j k2) r. Bicategory kk => Obj a -> ((a +++ ('Nil :: Path kk k2 k2)) ~ a => r) -> r Source Comments #

data Strictified (ps :: Path kk j k1) (qs :: Path kk j k1) where Source Comments #

Constructors

Str :: forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1) (qs :: Path kk j k1). (Ob ps, Ob qs, Ob0 kk j, Ob0 kk k1) => (Fold ps ~> Fold qs) -> Strictified ps qs

Instances

Instances details

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

type family Fold (as :: Path kk j k1) :: kk j k1 Source Comments #

Instances

Instances details

type Fold ('Nil :: Path kk j j) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory type Fold ('Nil :: Path kk j j) = I :: kk j j
type Fold (p '::: (q '::: ps) :: Path kk i k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory type Fold (p '::: (q '::: ps) :: Path kk i k2) = O p (Fold (q '::: ps))
type Fold (p '::: ('Nil :: Path kk k2 k2) :: Path kk j k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory type Fold (p '::: ('Nil :: Path kk k2 k2) :: Path kk j k2) = p

fold :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j). Bicategory kk => SPath as -> Fold as ~> Fold as Source Comments #

obj1 :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j). (Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) => Obj (p '::: ('Nil :: Path kk j j)) Source Comments #

concatFold :: forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1} (as :: Path kk i j) (bs :: Path kk j k2). (Ob as, Ob bs, Ob0 kk i, Ob0 kk j, Ob0 kk k2, Bicategory kk) => O (Fold as) (Fold bs) ~> Fold (as +++ bs) Source Comments #

splitFold :: forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1} (as :: Path kk i j) (bs :: Path kk j k2). (Ob as, Ob bs, Ob0 kk i, Ob0 kk j, Ob0 kk k2, Bicategory kk) => Fold (as +++ bs) ~> O (Fold as) (Fold bs) Source Comments #

introI :: forall {k} {kk :: CAT k} {j :: k}. (Ob0 kk j, Bicategory kk) => ('Nil :: Path kk j j) ~> ((I :: kk j j) '::: ('Nil :: Path kk j j)) Source Comments #

elimI :: forall {k} {kk :: CAT k} {j :: k}. (Ob0 kk j, Bicategory kk) => ((I :: kk j j) '::: ('Nil :: Path kk j j)) ~> ('Nil :: Path kk j j) Source Comments #

introO :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (p :: kk i j) (q :: kk j k2). (Ob0 kk i, Ob0 kk j, Ob0 kk k2, Bicategory kk, Ob p, Ob q) => (p '::: (q '::: ('Nil :: Path kk k2 k2))) ~> (O p q '::: ('Nil :: Path kk k2 k2)) Source Comments #

elimO :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (p :: kk i j) (q :: kk j k2). (Ob0 kk i, Ob0 kk j, Ob0 kk k2, Bicategory kk, Ob p, Ob q) => (O p q '::: ('Nil :: Path kk k2 k2)) ~> (p '::: (q '::: ('Nil :: Path kk k2 k2))) Source Comments #

More

class (Bicategory kk, Ob0 kk a, Ob t) => 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 'T1 Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Terminal Methods eta :: (I :: TERMK 'T0 'T0) ~> 'T1 Source Comments # mu :: O 'T1 'T1 ~> 'T1 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 #
Promonad p => Monad ('PK p :: ProfK 'ProfC k k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods eta :: (I :: ProfK 'ProfC k k) ~> ('PK p :: ProfK 'ProfC k k) Source Comments # mu :: O ('PK p :: ProfK 'ProfC k k) ('PK p :: ProfK 'ProfC k k) ~> ('PK p :: ProfK 'ProfC k k) Source Comments #
(Bicategory (Path kk), Ob0 kk a) => Monad ('Nil :: Path kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory 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 #
(Adjunction l r, Ob (O r l)) => Monad (r '::: (l '::: ('Nil :: Path kk a a)) :: Path kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory Methods eta :: (I :: Path kk a a) ~> (r '::: (l '::: ('Nil :: Path kk a a))) Source Comments # mu :: O (r '::: (l '::: ('Nil :: Path kk a a))) (r '::: (l '::: ('Nil :: Path kk a a))) ~> (r '::: (l '::: ('Nil :: Path kk a a))) Source Comments #

class (Bicategory kk, Ob0 kk a, Ob t) => 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

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 (Path kk), Ob0 kk a) => Comonad ('Nil :: Path kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory 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 #
(Adjunction l r, Ob (O l r)) => Comonad (l '::: (r '::: ('Nil :: Path kk a a)) :: Path kk a a) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory Methods epsilon :: (l '::: (r '::: ('Nil :: Path kk a a))) ~> (I :: Path kk a a) Source Comments # delta :: (l '::: (r '::: ('Nil :: Path kk a a))) ~> O (l '::: (r '::: ('Nil :: Path kk a a))) (l '::: (r '::: ('Nil :: Path kk a a))) Source Comments #

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

Methods

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

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

Instances

Instances details

Adjunction l r => Adjunction ('PK l :: ProfK 'ProfC c d) ('PK r :: ProfK 'ProfC d c) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods unit :: (I :: ProfK 'ProfC d d) ~> O ('PK r :: ProfK 'ProfC d c) ('PK l :: ProfK 'ProfC c d) Source Comments # counit :: O ('PK l :: ProfK 'ProfC c d) ('PK r :: ProfK 'ProfC d c) ~> (I :: ProfK 'ProfC c c) Source Comments #

class (Monad s, Monad t) => Bimodule (s :: kk a a) (t :: kk b b) (p :: kk a b) 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 #
(IsCategoryOf j cj, IsCategoryOf k ck, Profunctor p) => Bimodule ('PK cj :: ProfK 'ProfC j j) ('PK ck :: ProfK 'ProfC k k) ('PK p :: ProfK 'ProfC j k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods leftAction :: O ('PK cj :: ProfK 'ProfC j j) ('PK p :: ProfK 'ProfC j k) ~> ('PK p :: ProfK 'ProfC j k) Source Comments # rightAction :: O ('PK p :: ProfK 'ProfC j k) ('PK ck :: ProfK 'ProfC k k) ~> ('PK p :: ProfK 'ProfC j k) Source Comments #