proarrow-0: Category theory with a central role for profunctors
Safe HaskellNone
LanguageHaskell2010

Proarrow.Category.Bicategory.Strictified

Synopsis

Documentation

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

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

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

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

Equipment hk vk => Equipment (Path hk :: k -> k -> Type) (Path vk :: k -> k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment

Methods

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

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

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

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

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

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

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

HasCompanions hk vk => HasCompanions (Path hk :: k -> k -> Type) (Path vk :: k -> k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment

Methods

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

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

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

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

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

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

Defined in Proarrow.Category.Bicategory.Strictified

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type (~>) = Strictified :: Path kk j k2 -> Path kk j k2 -> Type
(CategoryOf (kk j k2), Bicategory kk) => Promonad (Strictified :: Path kk j k2 -> Path kk j k2 -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

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), Bicategory kk) => Profunctor (Strictified :: Path kk j k2 -> Path kk j k2 -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

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 :: s -> s -> Type) (j :: k) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type Ob0 (Path kk :: s -> s -> Type) (j :: k) = Ob0 kk j
type I Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type I = 'Nil :: Path kk i i
type O (ps :: Path kk b c) (qs :: Path kk a b) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type O (ps :: Path kk b c) (qs :: Path kk a b) = qs +++ ps
type Companion (Path hk :: k -> k -> Type) ('Nil :: Path vk j j) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment

type Companion (Path hk :: k -> k -> Type) ('Nil :: Path vk j j) = 'Nil :: Path hk j j
type Conjoint (Path hk :: k -> k -> Type) ('Nil :: Path vk j j) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment

type Conjoint (Path hk :: k -> k -> Type) ('Nil :: Path vk j j) = 'Nil :: Path hk j j
type Companion (Path hk :: k -> k -> Type) (p '::: ps :: Path vk j1 k1) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment

type Companion (Path hk :: k -> k -> Type) (p '::: ps :: Path vk j1 k1) = Companion hk p '::: Companion (Path hk) ps
type Conjoint (Path hk :: k -> k -> Type) (p '::: ps :: Path vk c a) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment

type Conjoint (Path hk :: k -> k -> Type) (p '::: ps :: Path vk c a) = Conjoint (Path hk) ps +++ (Conjoint hk p '::: ('Nil :: Path hk c c))
type (~>) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

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.Strictified

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

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.Strictified

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.Strictified

type (p '::: ps :: Path kk i b) +++ (qs :: Path kk b k2) = p '::: (ps +++ qs)

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} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k} (p :: kk j j1) (ps1 :: Path kk j1 k1). Ob0 kk j => Obj p -> SPath ps1 -> SPath (p '::: ps1) 

class ((as +++ bs) +++ cs) ~ (as +++ (bs +++ cs)) => Assoc (as :: Path kk a a1) (bs :: Path kk a1 b) (cs :: Path kk b c) Source Comments #

Instances

Instances details
(as +++ (bs +++ cs)) ~ ((as +++ bs) +++ cs) => Assoc (as :: Path kk a1 a2) (bs :: Path kk a2 b) (cs :: Path kk b c) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

class (Bicategory kk, Ob0 kk j, Ob0 kk k1, (ps +++ ('Nil :: Path kk k1 k1)) ~ ps, forall (i :: k) (h :: k) (qs :: Path kk k1 h) (rs :: Path kk h i). Assoc ps qs rs) => IsPath (ps :: Path kk j k1) where Source Comments #

Methods

singPath :: SPath ps Source Comments #

Instances

Instances details
(Bicategory kk, Ob0 kk k2) => IsPath ('Nil :: Path kk k2 k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

singPath :: SPath ('Nil :: Path kk k2 k2) Source Comments #

(Ob0 kk i, Ob p, IsPath ps) => IsPath (p '::: ps :: Path kk i k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

singPath :: SPath (p '::: ps) Source Comments #

withIsPath :: forall {k1} (kk :: CAT k1) (j :: k1) (k2 :: k1) (ps :: Path kk j k2) r. Bicategory kk => SPath ps -> ((IsPath ps, Ob0 kk j, Ob0 kk k2) => r) -> r Source Comments #

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 #

singleton :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j) (q :: kk i j). Bicategory kk => (p ~> q) -> (p '::: ('Nil :: Path kk j j)) ~> (q '::: ('Nil :: Path kk j j)) 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 #

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 #

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 #

concatFold :: forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1} (as :: Path kk i j) (bs :: Path kk j k2). Bicategory kk => SPath as -> SPath bs -> O (Fold bs) (Fold as) ~> 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). Bicategory kk => SPath as -> SPath bs -> Fold (as +++ bs) ~> O (Fold bs) (Fold as) 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.Strictified

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.Strictified

type Fold (p '::: (q '::: ps) :: Path kk i k2) = O (Fold (q '::: ps)) p
type Fold (p '::: ('Nil :: Path kk k2 k2) :: Path kk j k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

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 #

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). (Ob0 kk j, Ob0 kk k1) => SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs 

Instances

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

Defined in Proarrow.Category.Bicategory.Strictified

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), Bicategory kk) => Profunctor (Strictified :: Path kk j k2 -> Path kk j k2 -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

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 #

str :: forall {k1} (kk :: CAT k1) (j :: k1) (k2 :: k1) (ps :: Path kk j k2) (qs :: Path kk j k2). Bicategory kk => Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs Source Comments #

unStr :: forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path kk j k2) (qs :: Path kk j k2). Strictified ps qs -> Fold ps ~> Fold qs 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 {s} {kk :: CAT s} {j :: s}. (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 q p '::: ('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 q p '::: ('Nil :: Path kk k2 k2)) ~> (p '::: (q '::: ('Nil :: Path kk k2 k2))) Source Comments #