Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Equipment

Synopsis

class (Bicategory hk, Bicategory vk, forall (k :: c). Ob0 vk k => Ob0' hk k) => HasCompanions (hk :: CAT c) (vk :: CAT c) | hk -> vk where
- type Companion (hk :: CAT c) (f :: vk j k) :: hk j k
- mapCompanion :: forall {j :: c} {k :: c} (f :: vk j k) (g :: vk j k). (f ~> g) -> Companion hk f ~> Companion hk g
- compToId :: forall (k :: c). Ob0 vk k => Companion hk (I :: vk k k) ~> (I :: hk k k)
- compFromId :: forall (k :: c). Ob0 vk k => (I :: hk k k) ~> Companion hk (I :: vk k k)
- compToCompose :: forall {i :: c} {j :: c} {k :: c} (f :: vk j k) (g :: vk i j). Obj f -> Obj g -> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
- compFromCompose :: forall {j1 :: c} {j2 :: c} {k :: c} (f :: vk j2 k) (g :: vk j1 j2). Obj f -> Obj g -> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
class Adjunction (Companion hk f) (Conjoint hk f) => ComConAdjunction (hk :: CAT c) (vk1 :: k) (f :: vk j k1)
class HasCompanions hk vk => Equipment (hk :: CAT c) (vk :: CAT c) | hk -> vk where
- type Conjoint (hk :: CAT c) (f :: vk j k) :: hk k j
- mapConjoint :: forall {j :: c} {k :: c} (f :: vk j k) (g :: vk j k). (f ~> g) -> Conjoint hk g ~> Conjoint hk f
- conjToId :: forall (k :: c). Ob0 vk k => Conjoint hk (I :: vk k k) ~> (I :: hk k k)
- conjFromId :: forall (k :: c). Ob0 vk k => (I :: hk k k) ~> Conjoint hk (I :: vk k k)
- conjToCompose :: forall {k1 :: c} {j :: c} {k2 :: c} (f :: vk j k2) (g :: vk k1 j). Obj f -> Obj g -> Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f)
- conjFromCompose :: forall {j1 :: c} {j2 :: c} {k :: c} (f :: vk j2 k) (g :: vk j1 j2). Obj f -> Obj g -> O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g)
- comConUnit :: forall {j :: c} {k :: c} (f :: vk j k). Obj f -> (I :: hk j j) ~> O (Conjoint hk f) (Companion hk f)
- comConCounit :: forall {j :: c} {k :: c} (f :: vk j k). Obj f -> O (Companion hk f) (Conjoint hk f) ~> (I :: hk k k)
type Cart (p :: hk h j) (f :: vk h i) (g :: vk j k) = O (O (Companion hk g) p) (Conjoint hk f)
type SQ' (hk :: CAT c) (vk :: CAT c) (h :: c) (i :: c) (j :: c) (k :: c) = (hk k i, vk j k) +-> (hk j h, vk h i)
type SQ (hk :: CAT c) (vk :: CAT c) = forall {h :: c} {i :: c} {j :: c} {k :: c}. SQ' hk vk h i j k
data Sq (pf :: (hk j h, vk h i)) (qg :: (hk k i, vk j k)) where
- Sq :: forall {c} {hk :: CAT c} {vk :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k). (Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) => (O (Companion hk f) p ~> O q (Companion hk g)) -> Sq '(p, f) '(q, g)
object :: forall {s} hk vk (k :: s). (HasCompanions hk vk, Ob0 vk k) => Sq '(I :: hk k k, I :: vk k k) '(I :: hk k k, I :: vk k k)
hArr :: forall {s} {hk} {vk} {j :: s} {k :: s} (p :: hk j k) (q :: hk j k). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k) => (p ~> q) -> Sq '(p, I :: vk k k) '(q, I :: vk j j)
hId :: forall {s} hk vk (j :: s) (k :: s) (p :: hk k j). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob p) => Sq '(p, I :: vk j j) '(p, I :: vk k k)
compId :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) => Sq '(Companion hk f, I :: vk k k) '(Companion hk f, I :: vk j j)
conjId :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k). (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) => Sq '(Conjoint hk f, I :: vk j j) '(Conjoint hk f, I :: vk k k)
vArr :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k) (g :: vk j k). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k) => (f ~> g) -> Sq '(I :: hk j j, f) '(I :: hk k k, g)
vId :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) => Sq '(I :: hk j j, f) '(I :: hk k k, f)
(|||) :: forall {c} {j :: c} {k :: c} {i :: c} {hk} {vk} {h :: c} {l :: c} {m :: c} (p :: hk m l) (q :: hk j h) (r :: hk k i) (d :: vk l h) (e :: vk m j) (f :: vk h i) (g :: vk j k). HasCompanions hk vk => Sq '(p, d) '(q, e) -> Sq '(q, f) '(r, g) -> Sq '(p, O f d) '(r, O g e)
(===) :: forall {s1} {k :: s1} {j1 :: s1} {hk} {vk} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1} (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i) (e :: vk h i) (f :: vk j2 j1) (g :: vk l k). HasCompanions hk vk => Sq '(r, e) '(s2, f) -> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
toRight :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k). (HasCompanions hk vk, Ob' f) => Sq '(I :: hk j j, f) '(Companion hk f, I :: vk j j)
fromLeft :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k). (HasCompanions hk vk, Ob' f) => Sq '(Companion hk f, I :: vk k k) '(I :: hk k k, f)
fromRight :: forall {c} {hk} {vk} {j :: c} {k :: c} (f :: vk j k). (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) => Sq '(I :: hk j j, I :: vk j j) '(Conjoint hk f, f)
toLeft :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k). (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) => Sq '(Conjoint hk f, f) '(I :: hk k k, I :: vk k k)
flipCompanion :: forall {s} {i :: s} {j :: s} {k :: s} (hk :: CAT s) (vk :: s -> s -> Type) (f :: vk j k) (p :: hk i j) (q :: hk i k). (Equipment hk vk, Ob p) => Obj f -> (O (Companion hk f) p ~> q) -> p ~> O (Conjoint hk f) q
flipCompanionInv :: forall {s} {i :: s} {j :: s} {k :: s} (hk :: CAT s) (vk :: s -> s -> Type) (f :: vk j k) (p :: hk i j) (q :: hk i k). (Equipment hk vk, Ob q) => Obj f -> (p ~> O (Conjoint hk f) q) -> O (Companion hk f) p ~> q
flipConjoint :: forall {c} {k1 :: c} {j :: c} {k2 :: c} (hk :: CAT c) (vk :: c -> c -> Type) (f :: vk j k2) (p :: hk j k1) (q :: hk k2 k1). (Equipment hk vk, Ob p) => Obj f -> (O p (Conjoint hk f) ~> q) -> p ~> O q (Companion hk f)
flipConjointInv :: forall {c} {k1 :: c} {j :: c} {k2 :: c} (hk :: CAT c) (vk :: c -> c -> Type) (f :: vk j k2) (p :: hk j k1) (q :: hk k2 k1). (Equipment hk vk, Ob q) => Obj f -> (p ~> O q (Companion hk f)) -> O p (Conjoint hk f) ~> q
data RetroSq (pf :: (hk k i, vk j k)) (qg :: (hk j h, vk h i)) where
- RetroSq :: forall {c} {hk :: CAT c} {vk :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k). (Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) => (O q (Companion hk g) ~> O (Companion hk f) p) -> RetroSq '(q, g) '(p, f)
companionFold :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (fs :: Path vk j k2). HasCompanions hk vk => SPath fs -> Companion hk (Fold fs) ~> Fold (Companion (Path hk) fs)
foldCompanion :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (fs :: Path vk j k2). HasCompanions hk vk => SPath fs -> Fold (Companion (Path hk) fs) ~> Companion hk (Fold fs)
mapCompanionSPath :: forall {k1} (hk :: CAT k1) {vk :: CAT k1} {j :: k1} {k2 :: k1} (fs :: Path vk j k2). HasCompanions hk vk => SPath fs -> SPath (Companion (Path hk) fs)
mapConjointSPath :: forall {k1} (hk :: CAT k1) {vk :: CAT k1} {j :: k1} {k2 :: k1} (fs :: Path vk j k2). Equipment hk vk => SPath fs -> SPath (Conjoint (Path hk) fs)
adjVK :: forall {k1} {h :: k1} hk vk (i :: k1) (j :: k1) (k2 :: k1) (f :: vk j k2) (g :: vk h i) (v :: hk j h) (w :: hk k2 i) (x :: hk h j) (y :: hk i k2). (Adjunction x v, Adjunction y w, HasCompanions hk vk, Ob v, Ob w) => RetroSq '(y, g) '(x, f) -> Sq '(v, g) '(w, f)

Documentation

class (Bicategory hk, Bicategory vk, forall (k :: c). Ob0 vk k => Ob0' hk k) => HasCompanions (hk :: CAT c) (vk :: CAT c) | hk -> vk where Source Comments #

A double category with companions.

Associated Types

type Companion (hk :: CAT c) (f :: vk j k) :: hk j k Source Comments #

Methods

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

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

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

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

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

Instances

Instances details

HasCompanions PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Companion PROFK (p :: SUBCAT ProfRep PROFK j k)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Companion PROFK (p :: SUBCAT ProfRep PROFK j k) = 'PK (UNFUN p)

Methods

mapCompanion :: forall {j} {k} (f :: FUNK j k) (g :: FUNK j k). (f ~> g) -> Companion PROFK f ~> Companion PROFK g Source Comments #

compToId :: Ob0 FUNK k => Companion PROFK (I :: FUNK k k) ~> (I :: PROFK k k) Source Comments #

compFromId :: Ob0 FUNK k => (I :: PROFK k k) ~> Companion PROFK (I :: FUNK k k) Source Comments #

compToCompose :: forall {i} {j} {k} (f :: FUNK j k) (g :: FUNK i j). Obj f -> Obj g -> Companion PROFK (O f g) ~> O (Companion PROFK f) (Companion PROFK g) Source Comments #

compFromCompose :: forall {j1} {j2} {k} (f :: FUNK j2 k) (g :: FUNK j1 j2). Obj f -> Obj g -> O (Companion PROFK f) (Companion PROFK g) ~> Companion PROFK (O f g) Source Comments #

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

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

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

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

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

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

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

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 #

Bicategory kk => HasCompanions (QKK kk :: c -> c -> Type) (kk :: CAT c) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Quintet

Methods

mapCompanion :: forall {j :: c} {k :: c} (f :: kk j k) (g :: kk j k). (f ~> g) -> Companion (QKK kk) f ~> Companion (QKK kk) g Source Comments #

compToId :: forall (k :: c). Ob0 kk k => Companion (QKK kk) (I :: kk k k) ~> (I :: QKK kk k k) Source Comments #

compFromId :: forall (k :: c). Ob0 kk k => (I :: QKK kk k k) ~> Companion (QKK kk) (I :: kk k k) Source Comments #

compToCompose :: forall {i :: c} {j :: c} {k :: c} (f :: kk j k) (g :: kk i j). Obj f -> Obj g -> Companion (QKK kk) (O f g) ~> O (Companion (QKK kk) f) (Companion (QKK kk) g) Source Comments #

compFromCompose :: forall {j1 :: c} {j2 :: c} {k :: c} (f :: kk j2 k) (g :: kk j1 j2). Obj f -> Obj g -> O (Companion (QKK kk) f) (Companion (QKK kk) g) ~> Companion (QKK kk) (O f g) Source Comments #

Bicategory kk => HasCompanions (WKK kk :: s -> s -> Type) (DiscreteK (Ob0' kk :: s -> Constraint) :: s -> s -> Type) Source Comments #

A bicategory as a proarrow equipment with only identity arrows vertically.

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

Methods

mapCompanion :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) j k). (f ~> g) -> Companion (WKK kk) f ~> Companion (WKK kk) g Source Comments #

compToId :: forall (k :: s). Ob0 (DiscreteK (Ob0' kk :: s -> Constraint)) k => Companion (WKK kk) (I :: DiscreteK (Ob0' kk :: s -> Constraint) k k) ~> (I :: WKK kk k k) Source Comments #

compFromId :: forall (k :: s). Ob0 (DiscreteK (Ob0' kk :: s -> Constraint)) k => (I :: WKK kk k k) ~> Companion (WKK kk) (I :: DiscreteK (Ob0' kk :: s -> Constraint) k k) Source Comments #

compToCompose :: forall {i :: s} {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) i j). Obj f -> Obj g -> Companion (WKK kk) (O f g) ~> O (Companion (WKK kk) f) (Companion (WKK kk) g) Source Comments #

compFromCompose :: forall {j1 :: s} {j2 :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j2 k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) j1 j2). Obj f -> Obj g -> O (Companion (WKK kk) f) (Companion (WKK kk) g) ~> Companion (WKK kk) (O f g) Source Comments #

(HasCompanions hj vj, HasCompanions hk vk) => HasCompanions (PRODK hj hk :: (j, k) -> (j, k) -> Type) (PRODK vj vk :: (j, k) -> (j, k) -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

mapCompanion :: forall {j0 :: (j, k)} {k0 :: (j, k)} (f :: PRODK vj vk j0 k0) (g :: PRODK vj vk j0 k0). (f ~> g) -> Companion (PRODK hj hk) f ~> Companion (PRODK hj hk) g Source Comments #

compToId :: forall (k0 :: (j, k)). Ob0 (PRODK vj vk) k0 => Companion (PRODK hj hk) (I :: PRODK vj vk k k) ~> (I :: PRODK hj hk k k) Source Comments #

compFromId :: forall (k0 :: (j, k)). Ob0 (PRODK vj vk) k0 => (I :: PRODK hj hk k k) ~> Companion (PRODK hj hk) (I :: PRODK vj vk k k) Source Comments #

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

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

class Adjunction (Companion hk f) (Conjoint hk f) => ComConAdjunction (hk :: CAT c) (vk1 :: k) (f :: vk j k1) Source Comments #

Instances

Instances details

Adjunction (Companion hk f) (Conjoint hk f) => ComConAdjunction (hk :: CAT c) (vk2 :: k2) (f :: vk1 j k1) Source Comments #
Instance details Defined in Proarrow.Category.Equipment

class HasCompanions hk vk => Equipment (hk :: CAT c) (vk :: CAT c) | hk -> vk where Source Comments #

Minimal complete definition

mapConjoint, (conjToId, conjFromId, conjToCompose, conjFromCompose | comConUnit, comConCounit)

Associated Types

type Conjoint (hk :: CAT c) (f :: vk j k) :: hk k j Source Comments #

Methods

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

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

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

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

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

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

default comConUnit :: forall {j :: c} {k :: c} (f :: vk j k). (Ob f => ComConAdjunction hk vk f) => Obj f -> (I :: hk j j) ~> O (Conjoint hk f) (Companion hk f) Source Comments #

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

default comConCounit :: forall {j :: c} {k :: c} (f :: vk j k). (Ob f => ComConAdjunction hk vk f) => Obj f -> O (Companion hk f) (Conjoint hk f) ~> (I :: hk k k) Source Comments #

Instances

Instances details

Equipment PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Conjoint PROFK (p :: SUBCAT ProfRep PROFK k j)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Conjoint PROFK (p :: SUBCAT ProfRep PROFK k j) = 'PK (RepCostar (UNFUN p))

Methods

mapConjoint :: forall {j} {k} (f :: FUNK j k) (g :: FUNK j k). (f ~> g) -> Conjoint PROFK g ~> Conjoint PROFK f Source Comments #

conjToId :: Ob0 FUNK k => Conjoint PROFK (I :: FUNK k k) ~> (I :: PROFK k k) Source Comments #

conjFromId :: Ob0 FUNK k => (I :: PROFK k k) ~> Conjoint PROFK (I :: FUNK k k) Source Comments #

conjToCompose :: forall {k1} {j} {k2} (f :: FUNK j k2) (g :: FUNK k1 j). Obj f -> Obj g -> Conjoint PROFK (O f g) ~> O (Conjoint PROFK g) (Conjoint PROFK f) Source Comments #

conjFromCompose :: forall {j1} {j2} {k} (f :: FUNK j2 k) (g :: FUNK j1 j2). Obj f -> Obj g -> O (Conjoint PROFK g) (Conjoint PROFK f) ~> Conjoint PROFK (O f g) Source Comments #

comConUnit :: forall {j} {k} (f :: FUNK j k). Obj f -> (I :: PROFK j j) ~> O (Conjoint PROFK f) (Companion PROFK f) Source Comments #

comConCounit :: forall {j} {k} (f :: FUNK j k). Obj f -> O (Companion PROFK f) (Conjoint PROFK f) ~> (I :: PROFK k k) Source Comments #

CompactClosed k => Equipment (MonK k :: () -> () -> Type) (MonK k :: () -> () -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

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

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

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

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

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

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

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

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

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

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

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

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

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

Equipment hk vk => 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 #

Bicategory kk => Equipment (WKK kk :: s -> s -> Type) (DiscreteK (Ob0' kk :: s -> Constraint) :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

Methods

mapConjoint :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) j k). (f ~> g) -> Conjoint (WKK kk) g ~> Conjoint (WKK kk) f Source Comments #

conjToId :: forall (k :: s). Ob0 (DiscreteK (Ob0' kk :: s -> Constraint)) k => Conjoint (WKK kk) (I :: DiscreteK (Ob0' kk :: s -> Constraint) k k) ~> (I :: WKK kk k k) Source Comments #

conjFromId :: forall (k :: s). Ob0 (DiscreteK (Ob0' kk :: s -> Constraint)) k => (I :: WKK kk k k) ~> Conjoint (WKK kk) (I :: DiscreteK (Ob0' kk :: s -> Constraint) k k) Source Comments #

conjToCompose :: forall {k1 :: s} {j :: s} {k2 :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k2) (g :: DiscreteK (Ob0' kk :: s -> Constraint) k1 j). Obj f -> Obj g -> Conjoint (WKK kk) (O f g) ~> O (Conjoint (WKK kk) g) (Conjoint (WKK kk) f) Source Comments #

conjFromCompose :: forall {j1 :: s} {j2 :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j2 k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) j1 j2). Obj f -> Obj g -> O (Conjoint (WKK kk) g) (Conjoint (WKK kk) f) ~> Conjoint (WKK kk) (O f g) Source Comments #

comConUnit :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k). Obj f -> (I :: WKK kk j j) ~> O (Conjoint (WKK kk) f) (Companion (WKK kk) f) Source Comments #

comConCounit :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k). Obj f -> O (Companion (WKK kk) f) (Conjoint (WKK kk) f) ~> (I :: WKK kk k k) Source Comments #

(Equipment hj vj, Equipment hk vk) => Equipment (PRODK hj hk :: (j, k) -> (j, k) -> Type) (PRODK vj vk :: (j, k) -> (j, k) -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

mapConjoint :: forall {j0 :: (j, k)} {k0 :: (j, k)} (f :: PRODK vj vk j0 k0) (g :: PRODK vj vk j0 k0). (f ~> g) -> Conjoint (PRODK hj hk) g ~> Conjoint (PRODK hj hk) f Source Comments #

conjToId :: forall (k0 :: (j, k)). Ob0 (PRODK vj vk) k0 => Conjoint (PRODK hj hk) (I :: PRODK vj vk k k) ~> (I :: PRODK hj hk k k) Source Comments #

conjFromId :: forall (k0 :: (j, k)). Ob0 (PRODK vj vk) k0 => (I :: PRODK hj hk k k) ~> Conjoint (PRODK hj hk) (I :: PRODK vj vk k k) Source Comments #

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

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

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

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

type Cart (p :: hk h j) (f :: vk h i) (g :: vk j k) = O (O (Companion hk g) p) (Conjoint hk f) Source Comments #

P(f, g)

type SQ' (hk :: CAT c) (vk :: CAT c) (h :: c) (i :: c) (j :: c) (k :: c) = (hk k i, vk j k) +-> (hk j h, vk h i) Source Comments #

The kind of a square '(q, f) '(p, g).

h--f--i
|  v  |
p--@--q
|  v  |
j--g--k

type SQ (hk :: CAT c) (vk :: CAT c) = forall {h :: c} {i :: c} {j :: c} {k :: c}. SQ' hk vk h i j k Source Comments #

data Sq (pf :: (hk j h, vk h i)) (qg :: (hk k i, vk j k)) where Source Comments #

Constructors

Sq :: forall {c} {hk :: CAT c} {vk :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k). (Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) => (O (Companion hk f) p ~> O q (Companion hk g)) -> Sq '(p, f) '(q, g)

Instances

Instances details

(HasCompanions hk vk, Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k) => Profunctor (Sq :: (hk j h, vk h i) -> (hk k i, vk j k) -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Equipment Methods dimap :: forall (c0 :: (hk j h, vk h i)) (a :: (hk j h, vk h i)) (b :: (hk k i, vk j k)) (d :: (hk k i, vk j k)). (c0 ~> a) -> (b ~> d) -> Sq a b -> Sq c0 d Source Comments # (\\) :: forall (a :: (hk j h, vk h i)) (b :: (hk k i, vk j k)) r. ((Ob a, Ob b) => r) -> Sq a b -> r Source Comments #

object :: forall {s} hk vk (k :: s). (HasCompanions hk vk, Ob0 vk k) => Sq '(I :: hk k k, I :: vk k k) '(I :: hk k k, I :: vk k k) Source Comments #

The empty square for an object.

k-----k
|     |
|     |
|     |
k-----k

hArr :: forall {s} {hk} {vk} {j :: s} {k :: s} (p :: hk j k) (q :: hk j k). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k) => (p ~> q) -> Sq '(p, I :: vk k k) '(q, I :: vk j j) Source Comments #

Make a square from a horizontal arrow

k-----k
|     |
p--@--q
|     |
j-----j

hId :: forall {s} hk vk (j :: s) (k :: s) (p :: hk k j). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob p) => Sq '(p, I :: vk j j) '(p, I :: vk k k) Source Comments #

compId :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) => Sq '(Companion hk f, I :: vk k k) '(Companion hk f, I :: vk j j) Source Comments #

conjId :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k). (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) => Sq '(Conjoint hk f, I :: vk j j) '(Conjoint hk f, I :: vk k k) Source Comments #

vArr :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k) (g :: vk j k). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k) => (f ~> g) -> Sq '(I :: hk j j, f) '(I :: hk k k, g) Source Comments #

Make a square from a vertical arrow

j--f--k
|  v  |
|  @  |
|  v  |
j--g--k

vId :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) => Sq '(I :: hk j j, f) '(I :: hk k k, f) Source Comments #

(|||) :: forall {c} {j :: c} {k :: c} {i :: c} {hk} {vk} {h :: c} {l :: c} {m :: c} (p :: hk m l) (q :: hk j h) (r :: hk k i) (d :: vk l h) (e :: vk m j) (f :: vk h i) (g :: vk j k). HasCompanions hk vk => Sq '(p, d) '(q, e) -> Sq '(q, f) '(r, g) -> Sq '(p, O f d) '(r, O g e) infixl 6 Source Comments #

Horizontal composition

l--d--h     h--f--i     l-f∘d-i
|  v  |     |  v  |     |  v  |
p--@--q ||| q--@--r  =  p--@--r
|  v  |     |  v  |     |  v  |
m--e--j     j--g--k     m-g∘e-k

(===) :: forall {s1} {k :: s1} {j1 :: s1} {hk} {vk} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1} (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i) (e :: vk h i) (f :: vk j2 j1) (g :: vk l k). HasCompanions hk vk => Sq '(r, e) '(s2, f) -> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g) infixl 5 Source Comments #

Vertical composition

 h--e--i
 |  v  |
 r--@--s
 |  v  |
 j--f--k
   ===
 j--f--k
 |  v  |
 p--@--q
 |  v  |
 l--g--m

   v v

 h--e--i
 |  v  |
r∘p-@-s∘q
 |  v  |
 j--g--k

toRight :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k). (HasCompanions hk vk, Ob' f) => Sq '(I :: hk j j, f) '(Companion hk f, I :: vk j j) Source Comments #

fromLeft :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k). (HasCompanions hk vk, Ob' f) => Sq '(Companion hk f, I :: vk k k) '(I :: hk k k, f) Source Comments #

fromRight :: forall {c} {hk} {vk} {j :: c} {k :: c} (f :: vk j k). (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) => Sq '(I :: hk j j, I :: vk j j) '(Conjoint hk f, f) Source Comments #

toLeft :: forall {s} {hk} {vk} {j :: s} {k :: s} (f :: vk j k). (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) => Sq '(Conjoint hk f, f) '(I :: hk k k, I :: vk k k) Source Comments #

flipCompanion :: forall {s} {i :: s} {j :: s} {k :: s} (hk :: CAT s) (vk :: s -> s -> Type) (f :: vk j k) (p :: hk i j) (q :: hk i k). (Equipment hk vk, Ob p) => Obj f -> (O (Companion hk f) p ~> q) -> p ~> O (Conjoint hk f) q Source Comments #

flipCompanionInv :: forall {s} {i :: s} {j :: s} {k :: s} (hk :: CAT s) (vk :: s -> s -> Type) (f :: vk j k) (p :: hk i j) (q :: hk i k). (Equipment hk vk, Ob q) => Obj f -> (p ~> O (Conjoint hk f) q) -> O (Companion hk f) p ~> q Source Comments #

flipConjoint :: forall {c} {k1 :: c} {j :: c} {k2 :: c} (hk :: CAT c) (vk :: c -> c -> Type) (f :: vk j k2) (p :: hk j k1) (q :: hk k2 k1). (Equipment hk vk, Ob p) => Obj f -> (O p (Conjoint hk f) ~> q) -> p ~> O q (Companion hk f) Source Comments #

flipConjointInv :: forall {c} {k1 :: c} {j :: c} {k2 :: c} (hk :: CAT c) (vk :: c -> c -> Type) (f :: vk j k2) (p :: hk j k1) (q :: hk k2 k1). (Equipment hk vk, Ob q) => Obj f -> (p ~> O q (Companion hk f)) -> O p (Conjoint hk f) ~> q Source Comments #

data RetroSq (pf :: (hk k i, vk j k)) (qg :: (hk j h, vk h i)) where Source Comments #

The kind of a retro square '(q, f) '(p, g).

h--f--i
|  v  |
p--§--q
|  v  |
j--g--k

Constructors

RetroSq :: forall {c} {hk :: CAT c} {vk :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k). (Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) => (O q (Companion hk g) ~> O (Companion hk f) p) -> RetroSq '(q, g) '(p, f)

Instances

Instances details

(HasCompanions hk vk, Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k) => Profunctor (RetroSq :: (hk k i, vk j k) -> (hk j h, vk h i) -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Equipment Methods dimap :: forall (c0 :: (hk k i, vk j k)) (a :: (hk k i, vk j k)) (b :: (hk j h, vk h i)) (d :: (hk j h, vk h i)). (c0 ~> a) -> (b ~> d) -> RetroSq a b -> RetroSq c0 d Source Comments # (\\) :: forall (a :: (hk k i, vk j k)) (b :: (hk j h, vk h i)) r. ((Ob a, Ob b) => r) -> RetroSq a b -> r Source Comments #

companionFold :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (fs :: Path vk j k2). HasCompanions hk vk => SPath fs -> Companion hk (Fold fs) ~> Fold (Companion (Path hk) fs) Source Comments #

foldCompanion :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (fs :: Path vk j k2). HasCompanions hk vk => SPath fs -> Fold (Companion (Path hk) fs) ~> Companion hk (Fold fs) Source Comments #

mapCompanionSPath :: forall {k1} (hk :: CAT k1) {vk :: CAT k1} {j :: k1} {k2 :: k1} (fs :: Path vk j k2). HasCompanions hk vk => SPath fs -> SPath (Companion (Path hk) fs) Source Comments #

mapConjointSPath :: forall {k1} (hk :: CAT k1) {vk :: CAT k1} {j :: k1} {k2 :: k1} (fs :: Path vk j k2). Equipment hk vk => SPath fs -> SPath (Conjoint (Path hk) fs) Source Comments #

adjVK :: forall {k1} {h :: k1} hk vk (i :: k1) (j :: k1) (k2 :: k1) (f :: vk j k2) (g :: vk h i) (v :: hk j h) (w :: hk k2 i) (x :: hk h j) (y :: hk i k2). (Adjunction x v, Adjunction y w, HasCompanions hk vk, Ob v, Ob w) => RetroSq '(y, g) '(x, f) -> Sq '(v, g) '(w, f) Source Comments #