Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory.Kan

Documentation

class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Lan j f)) => LeftKanExtension (j :: kk c d) (f :: kk c e) where Source Comments #

Associated Types

type Lan (j :: kk c d) (f :: kk c e) :: kk d e Source Comments #

Methods

lan :: f ~> O (Lan j f) j Source Comments #

lanUniv :: forall (g :: kk d e). Ob g => (f ~> O g j) -> Lan j f ~> g Source Comments #

Instances

Instances details

(Coclosed k, Ob (q <~~ p), Ob p, Ob q) => LeftKanExtension ('MK p :: MonK k c d) ('MK q :: MonK k c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Associated Types

type Lan ('MK p :: MonK k c d) ('MK q :: MonK k c e)
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type Lan ('MK p :: MonK k c d) ('MK q :: MonK k c e) = 'MK (q <~~ p) :: MonK k d e

Methods

lan :: ('MK q :: MonK k c e) ~> O (Lan ('MK p :: MonK k c d) ('MK q :: MonK k c e)) ('MK p :: MonK k c d) Source Comments #

lanUniv :: forall (g :: MonK k d e). Ob g => (('MK q :: MonK k c e) ~> O g ('MK p :: MonK k c d)) -> Lan ('MK p :: MonK k c d) ('MK q :: MonK k c e) ~> g Source Comments #

RightKanExtension j2 f => LeftKanExtension ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type Lan ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e)
Instance details Defined in Proarrow.Category.Bicategory.Co type Lan ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) = 'CO (Ran j2 f)

Methods

lan :: 'CO f ~> O (Lan ('CO j2) ('CO f)) ('CO j2) Source Comments #

lanUniv :: forall (g :: COK kk d e). Ob g => ('CO f ~> O g ('CO j2)) -> Lan ('CO j2) ('CO f) ~> g Source Comments #

LeftKanLift j2 f => LeftKanExtension ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Associated Types

type Lan ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e)
Instance details Defined in Proarrow.Category.Bicategory.Op type Lan ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) = 'OP (Lift j2 f)

Methods

lan :: 'OP f ~> O (Lan ('OP j2) ('OP f)) ('OP j2) Source Comments #

lanUniv :: forall (g :: OPK kk d e). Ob g => ('OP f ~> O g ('OP j2)) -> Lan ('OP j2) ('OP f) ~> g Source Comments #

mapLan :: forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d) (f :: kk c e) (g :: kk c e). (LeftKanExtension j f, LeftKanExtension j g) => (f ~> g) -> Lan j f ~> Lan j g Source Comments #

rebaseLan :: forall {k} {kk :: CAT k} {c :: k} {e :: k} {d :: k} (f :: kk c e) (i :: kk c d) (j :: kk c d). (LeftKanExtension j f, LeftKanExtension i f) => (i ~> j) -> Lan j f ~> Lan i f Source Comments #

dimapLan :: forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (i :: kk c d) (j :: kk c d) (f :: kk c e) (g :: kk c e). (LeftKanExtension j f, LeftKanExtension i g) => (i ~> j) -> (f ~> g) -> Lan j f ~> Lan i g Source Comments #

lanComonadEpsilon :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} (p :: kk c d). LeftKanExtension p p => Lan p p ~> (I :: kk d d) Source Comments #

lanComonadDelta :: forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (p :: kk c d). LeftKanExtension p p => Lan p p ~> O (Lan p p) (Lan p p) Source Comments #

idLan :: forall {s} {kk :: CAT s} {c :: s} {e :: s} (f :: kk c e). (LeftKanExtension (I :: kk c c) f, Ob f) => f ~> Lan (I :: kk c c) f Source Comments #

lanAlongCompanion :: forall {c} {k1 :: c} {i :: c} {k2 :: c} (hk :: CAT c) (vk :: c -> c -> Type) (j :: vk i k2) (f :: hk i k1). (LeftKanExtension (Companion hk j) f, Equipment hk vk) => Obj j -> Lan (Companion hk j) f ~> O f (Conjoint hk j) Source Comments #

lanAlongCompanionInv :: forall {k1} {e :: k1} {i :: k1} {k2 :: k1} (hk :: CAT k1) (vk :: k1 -> k1 -> Type) (j :: vk i k2) (f :: hk i e). (LeftKanExtension (Companion hk j) f, Equipment hk vk) => Obj j -> O f (Conjoint hk j) ~> Lan (Companion hk j) f Source Comments #

type (|>) (j :: kk c d) (p :: kk c e) = Ran j p Source Comments #

class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Ran j f)) => RightKanExtension (j :: kk c d) (f :: kk c e) where Source Comments #

Associated Types

type Ran (j :: kk c d) (f :: kk c e) :: kk d e Source Comments #

Methods

ran :: O (Ran j f) j ~> f Source Comments #

ranUniv :: forall (g :: kk d e). Ob g => (O g j ~> f) -> g ~> Ran j f Source Comments #

Instances

Instances details

(Profunctor f, Profunctor j) => RightKanExtension ('PK j :: PROFK c d) ('PK f :: PROFK c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Ran ('PK j :: PROFK c d) ('PK f :: PROFK c e)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Ran ('PK j :: PROFK c d) ('PK f :: PROFK c e) = 'PK (Ran ('OP j) f)

Methods

ran :: O (Ran ('PK j) ('PK f)) ('PK j) ~> 'PK f Source Comments #

ranUniv :: forall (g :: PROFK d e). Ob g => (O g ('PK j) ~> 'PK f) -> g ~> Ran ('PK j) ('PK f) Source Comments #

(Closed k, Ob (p ~~> q), Ob p, Ob q) => RightKanExtension ('MK p :: MonK k c d) ('MK q :: MonK k c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Associated Types

type Ran ('MK p :: MonK k c d) ('MK q :: MonK k c e)
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type Ran ('MK p :: MonK k c d) ('MK q :: MonK k c e) = 'MK (p ~~> q) :: MonK k d e

Methods

ran :: O (Ran ('MK p :: MonK k c d) ('MK q :: MonK k c e)) ('MK p :: MonK k c d) ~> ('MK q :: MonK k c e) Source Comments #

ranUniv :: forall (g :: MonK k d e). Ob g => (O g ('MK p :: MonK k c d) ~> ('MK q :: MonK k c e)) -> g ~> Ran ('MK p :: MonK k c d) ('MK q :: MonK k c e) Source Comments #

LeftKanExtension j2 f => RightKanExtension ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type Ran ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e)
Instance details Defined in Proarrow.Category.Bicategory.Co type Ran ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) = 'CO (Lan j2 f)

Methods

ran :: O (Ran ('CO j2) ('CO f)) ('CO j2) ~> 'CO f Source Comments #

ranUniv :: forall (g :: COK kk d e). Ob g => (O g ('CO j2) ~> 'CO f) -> g ~> Ran ('CO j2) ('CO f) Source Comments #

RightKanLift j2 f => RightKanExtension ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Associated Types

type Ran ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e)
Instance details Defined in Proarrow.Category.Bicategory.Op type Ran ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) = 'OP (Rift j2 f)

Methods

ran :: O (Ran ('OP j2) ('OP f)) ('OP j2) ~> 'OP f Source Comments #

ranUniv :: forall (g :: OPK kk d e). Ob g => (O g ('OP j2) ~> 'OP f) -> g ~> Ran ('OP j2) ('OP f) Source Comments #

mapRan :: forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d) (f :: kk c e) (g :: kk c e). (RightKanExtension j f, RightKanExtension j g) => (f ~> g) -> Ran j f ~> Ran j g Source Comments #

rebaseRan :: forall {k} {kk :: CAT k} {c :: k} {e :: k} {d :: k} (f :: kk c e) (i :: kk c d) (j :: kk c d). (RightKanExtension j f, RightKanExtension i f) => (i ~> j) -> Ran j f ~> Ran i f Source Comments #

dimapRan :: forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (i :: kk c d) (j :: kk c d) (f :: kk c e) (g :: kk c e). (RightKanExtension j f, RightKanExtension i g) => (i ~> j) -> (f ~> g) -> Ran j f ~> Ran i g Source Comments #

ranMonadEta :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} (p :: kk c d). RightKanExtension p p => (I :: kk d d) ~> Ran p p Source Comments #

ranMonadMu :: forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (p :: kk c d). RightKanExtension p p => O (Ran p p) (Ran p p) ~> Ran p p Source Comments #

composeRan :: forall {k} {kk :: CAT k} {j1 :: k} {d :: k} {c :: k} {e :: k} (i :: kk j1 d) (j2 :: kk c j1) (f :: kk c e). (RightKanExtension j2 f, RightKanExtension i (Ran j2 f), RightKanExtension (O i j2) f) => Ran i (Ran j2 f) ~> Ran (O i j2) f Source Comments #

idRan :: forall {s} {kk :: CAT s} {c :: s} {e :: s} (f :: kk c e). (RightKanExtension (I :: kk c c) f, Ob f) => f ~> Ran (I :: kk c c) f Source Comments #

ranAlongConjoint :: forall {c} {k1 :: c} {i :: c} {k2 :: c} (hk :: CAT c) (vk :: c -> c -> Type) (j :: vk i k2) (f :: hk k2 k1). (RightKanExtension (Conjoint hk j) f, Equipment hk vk) => Obj j -> Ran (Conjoint hk j) f ~> O f (Companion hk j) Source Comments #

ranAlongConjointInv :: forall {k1} {e :: k1} {i :: k1} {k2 :: k1} (hk :: CAT k1) (vk :: k1 -> k1 -> Type) (j :: vk i k2) (f :: hk k2 e). (RightKanExtension (Conjoint hk j) f, Equipment hk vk) => Obj j -> O f (Companion hk j) ~> Ran (Conjoint hk j) f Source Comments #

class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Lift j f)) => LeftKanLift (j :: kk d c) (f :: kk e c) where Source Comments #

Associated Types

type Lift (j :: kk d c) (f :: kk e c) :: kk e d Source Comments #

Methods

lift :: f ~> O j (Lift j f) Source Comments #

liftUniv :: forall (g :: kk e d). Ob g => (f ~> O j g) -> Lift j f ~> g Source Comments #

Instances

Instances details

(Coclosed k, SymMonoidal k, Ob (q <~~ p), Ob p, Ob q) => LeftKanLift ('MK p :: MonK k d c) ('MK q :: MonK k e c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Associated Types

type Lift ('MK p :: MonK k d c) ('MK q :: MonK k e c)
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type Lift ('MK p :: MonK k d c) ('MK q :: MonK k e c) = 'MK (q <~~ p) :: MonK k e d

Methods

lift :: ('MK q :: MonK k e c) ~> O ('MK p :: MonK k d c) (Lift ('MK p :: MonK k d c) ('MK q :: MonK k e c)) Source Comments #

liftUniv :: forall (g :: MonK k e d). Ob g => (('MK q :: MonK k e c) ~> O ('MK p :: MonK k d c) g) -> Lift ('MK p :: MonK k d c) ('MK q :: MonK k e c) ~> g Source Comments #

RightKanLift j f => LeftKanLift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type Lift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2)
Instance details Defined in Proarrow.Category.Bicategory.Co type Lift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) = 'CO (Rift j f)

Methods

lift :: 'CO f ~> O ('CO j) (Lift ('CO j) ('CO f)) Source Comments #

liftUniv :: forall (g :: COK kk e d). Ob g => ('CO f ~> O ('CO j) g) -> Lift ('CO j) ('CO f) ~> g Source Comments #

LeftKanExtension j f => LeftKanLift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Associated Types

type Lift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2)
Instance details Defined in Proarrow.Category.Bicategory.Op type Lift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) = 'OP (Lan j f)

Methods

lift :: 'OP f ~> O ('OP j) (Lift ('OP j) ('OP f)) Source Comments #

liftUniv :: forall (g :: OPK kk e d). Ob g => ('OP f ~> O ('OP j) g) -> Lift ('OP j) ('OP f) ~> g Source Comments #

mapLift :: forall {k} {kk :: CAT k} {d :: k} {c :: k} {e :: k} (j :: kk d c) (f :: kk e c) (g :: kk e c). (LeftKanLift j f, LeftKanLift j g) => (f ~> g) -> Lift j f ~> Lift j g Source Comments #

rebaseLift :: forall {k} {kk :: CAT k} {e :: k} {c :: k} {d :: k} (f :: kk e c) (i :: kk d c) (j :: kk d c). (LeftKanLift j f, LeftKanLift i f) => (i ~> j) -> Lift j f ~> Lift i f Source Comments #

dimapLift :: forall {k} {kk :: CAT k} {d :: k} {c :: k} {e :: k} (i :: kk d c) (j :: kk d c) (f :: kk e c) (g :: kk e c). (LeftKanLift j f, LeftKanLift i g) => (i ~> j) -> (f ~> g) -> Lift j f ~> Lift i g Source Comments #

liftComonadEpsilon :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} (p :: kk d c). LeftKanLift p p => Lift p p ~> (I :: kk d d) Source Comments #

liftComonadDelta :: forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (p :: kk d c). LeftKanLift p p => Lift p p ~> O (Lift p p) (Lift p p) Source Comments #

idLift :: forall {s} {kk :: CAT s} {e :: s} {d :: s} (f :: kk e d). (LeftKanLift (I :: kk d d) f, Ob f) => f ~> Lift (I :: kk d d) f Source Comments #

liftAlongConjoint :: forall {s} {i1 :: s} {i2 :: s} {k :: s} (hk :: CAT s) (vk :: s -> s -> Type) (j :: vk i2 k) (f :: hk i1 i2). (LeftKanLift (Conjoint hk j) f, Equipment hk vk) => Obj j -> Lift (Conjoint hk j) f ~> O (Companion hk j) f Source Comments #

liftAlongConjointInv :: forall {k1} {e :: k1} {i :: k1} {k2 :: k1} (hk :: CAT k1) (vk :: k1 -> k1 -> Type) (j :: vk i k2) (f :: hk e i). (LeftKanLift (Conjoint hk j) f, Equipment hk vk) => Obj j -> O (Companion hk j) f ~> Lift (Conjoint hk j) f Source Comments #

type (<|) (p :: kk e c) (j :: kk d c) = Rift j p Source Comments #

class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Rift j f)) => RightKanLift (j :: kk d c) (f :: kk e c) where Source Comments #

Associated Types

type Rift (j :: kk d c) (f :: kk e c) :: kk e d Source Comments #

Methods

rift :: O j (Rift j f) ~> f Source Comments #

riftUniv :: forall (g :: kk e d). Ob g => (O j g ~> f) -> g ~> Rift j f Source Comments #

Instances

Instances details

(Profunctor f, Profunctor j) => RightKanLift ('PK j :: PROFK d c) ('PK f :: PROFK e c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Rift ('PK j :: PROFK d c) ('PK f :: PROFK e c)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Rift ('PK j :: PROFK d c) ('PK f :: PROFK e c) = 'PK (Rift ('OP j) f)

Methods

rift :: O ('PK j) (Rift ('PK j) ('PK f)) ~> 'PK f Source Comments #

riftUniv :: forall (g :: PROFK e d). Ob g => (O ('PK j) g ~> 'PK f) -> g ~> Rift ('PK j) ('PK f) Source Comments #

(Closed k, SymMonoidal k, Ob (p ~~> q), Ob p, Ob q) => RightKanLift ('MK p :: MonK k d c) ('MK q :: MonK k e c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Associated Types

type Rift ('MK p :: MonK k d c) ('MK q :: MonK k e c)
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type Rift ('MK p :: MonK k d c) ('MK q :: MonK k e c) = 'MK (p ~~> q) :: MonK k e d

Methods

rift :: O ('MK p :: MonK k d c) (Rift ('MK p :: MonK k d c) ('MK q :: MonK k e c)) ~> ('MK q :: MonK k e c) Source Comments #

riftUniv :: forall (g :: MonK k e d). Ob g => (O ('MK p :: MonK k d c) g ~> ('MK q :: MonK k e c)) -> g ~> Rift ('MK p :: MonK k d c) ('MK q :: MonK k e c) Source Comments #

LeftKanLift j f => RightKanLift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type Rift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2)
Instance details Defined in Proarrow.Category.Bicategory.Co type Rift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) = 'CO (Lift j f)

Methods

rift :: O ('CO j) (Rift ('CO j) ('CO f)) ~> 'CO f Source Comments #

riftUniv :: forall (g :: COK kk e d). Ob g => (O ('CO j) g ~> 'CO f) -> g ~> Rift ('CO j) ('CO f) Source Comments #

RightKanExtension j f => RightKanLift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Associated Types

type Rift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2)
Instance details Defined in Proarrow.Category.Bicategory.Op type Rift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) = 'OP (Ran j f)

Methods

rift :: O ('OP j) (Rift ('OP j) ('OP f)) ~> 'OP f Source Comments #

riftUniv :: forall (g :: OPK kk e d). Ob g => (O ('OP j) g ~> 'OP f) -> g ~> Rift ('OP j) ('OP f) Source Comments #

mapRift :: forall {k} {kk :: CAT k} {d :: k} {c :: k} {e :: k} (j :: kk d c) (f :: kk e c) (g :: kk e c). (RightKanLift j f, RightKanLift j g) => (f ~> g) -> Rift j f ~> Rift j g Source Comments #

rebaseRift :: forall {k} {kk :: CAT k} {e :: k} {c :: k} {d :: k} (f :: kk e c) (i :: kk d c) (j :: kk d c). (RightKanLift j f, RightKanLift i f) => (i ~> j) -> Rift j f ~> Rift i f Source Comments #

dimapRift :: forall {k} {kk :: CAT k} {d :: k} {c :: k} {e :: k} (i :: kk d c) (j :: kk d c) (f :: kk e c) (g :: kk e c). (RightKanLift j f, RightKanLift i g) => (i ~> j) -> (f ~> g) -> Rift j f ~> Rift i g Source Comments #

riftMonadEta :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} (p :: kk d c). RightKanLift p p => (I :: kk d d) ~> Rift p p Source Comments #

riftMonadMu :: forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (p :: kk d c). RightKanLift p p => O (Rift p p) (Rift p p) ~> Rift p p Source Comments #

composeRift :: forall {k} {kk :: CAT k} {d :: k} {j1 :: k} {c :: k} {e :: k} (i :: kk d j1) (j2 :: kk j1 c) (f :: kk e c). (RightKanLift j2 f, RightKanLift i (Rift j2 f), RightKanLift (O j2 i) f) => Rift i (Rift j2 f) ~> Rift (O j2 i) f Source Comments #

idRift :: forall {s} {kk :: CAT s} {e :: s} {d :: s} (f :: kk e d). (RightKanLift (I :: kk d d) f, Ob f) => f ~> Rift (I :: kk d d) f Source Comments #

riftAlongCompanion :: forall {s} {i1 :: s} {i2 :: s} {k :: s} (hk :: CAT s) (vk :: s -> s -> Type) (j :: vk i2 k) (f :: hk i1 k). (RightKanLift (Companion hk j) f, Equipment hk vk) => Obj j -> Rift (Companion hk j) f ~> O (Conjoint hk j) f Source Comments #

riftAlongCompanionInv :: forall {k1} {e :: k1} {i :: k1} {k2 :: k1} (hk :: CAT k1) (vk :: k1 -> k1 -> Type) (j :: vk i k2) (f :: hk e k2). (RightKanLift (Companion hk j) f, Equipment hk vk) => Obj j -> O (Conjoint hk j) f ~> Rift (Companion hk j) f Source Comments #