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 j (Lan j f) Source Comments #

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

Instances

Instances details

(Functor j, Functor f) => LeftKanExtension ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Kan

Associated Types

type Lan ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e)
Instance details Defined in Proarrow.Category.Bicategory.Kan type Lan ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) = 'MK (HaskLan j f) :: MonK (Type -> Type) d e

Methods

lan :: ('MK f :: MonK (Type -> Type) c e) ~> O ('MK j :: MonK (Type -> Type) c d) (Lan ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e)) Source Comments #

lanUniv :: forall (g :: MonK (Type -> Type) d e). Ob g => (('MK f :: MonK (Type -> Type) c e) ~> O ('MK j :: MonK (Type -> Type) c d) g) -> Lan ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) 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 ('CO j2) (Lan ('CO j2) ('CO f)) Source Comments #

lanUniv :: forall (g :: COK kk d e). Ob g => ('CO f ~> O ('CO j2) g) -> 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 ('OP j2) (Lan ('OP j2) ('OP f)) Source Comments #

lanUniv :: forall (g :: OPK kk d e). Ob g => ('OP f ~> O ('OP j2) g) -> 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} {d :: k} {e :: k} (i :: kk c d) (j :: kk c d) (f :: kk c e). (LeftKanExtension j f, LeftKanExtension i f) => (i ~> j) -> Lan j f ~> Lan i f 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 j (Ran j f) ~> f Source Comments #

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

Instances

Instances details

(Functor j, Functor f) => RightKanExtension ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Kan

Associated Types

type Ran ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e)
Instance details Defined in Proarrow.Category.Bicategory.Kan type Ran ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) = 'MK (HaskRan j f) :: MonK (Type -> Type) d e

Methods

ran :: O ('MK j :: MonK (Type -> Type) c d) (Ran ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e)) ~> ('MK f :: MonK (Type -> Type) c e) Source Comments #

ranUniv :: forall (g :: MonK (Type -> Type) d e). Ob g => (O ('MK j :: MonK (Type -> Type) c d) g ~> ('MK f :: MonK (Type -> Type) c e)) -> g ~> Ran ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) Source Comments #

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

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

Methods

ran :: O ('PK j :: ProfK 'ProfC c d) (Ran ('PK j :: ProfK 'ProfC c d) ('PK f :: ProfK 'ProfC c e)) ~> ('PK f :: ProfK 'ProfC c e) Source Comments #

ranUniv :: forall (g :: ProfK 'ProfC d e). Ob g => (O ('PK j :: ProfK 'ProfC c d) g ~> ('PK f :: ProfK 'ProfC c e)) -> g ~> Ran ('PK j :: ProfK 'ProfC c d) ('PK f :: ProfK 'ProfC 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 ('CO j2) (Ran ('CO j2) ('CO f)) ~> 'CO f Source Comments #

ranUniv :: forall (g :: COK kk d e). Ob g => (O ('CO j2) g ~> '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 ('OP j2) (Ran ('OP j2) ('OP f)) ~> 'OP f Source Comments #

ranUniv :: forall (g :: OPK kk d e). Ob g => (O ('OP j2) g ~> '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} {d :: k} {e :: k} (i :: kk c d) (j :: kk c d) (f :: kk c e). (RightKanExtension j f, RightKanExtension i f) => (i ~> j) -> Ran j f ~> Ran i 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 (Lift j f) j Source Comments #

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

Instances

Instances details

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 (Lift ('CO j) ('CO f)) ('CO j) Source Comments #

liftUniv :: forall (g :: COK kk e d). Ob g => ('CO f ~> O g ('CO j)) -> 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 (Lift ('OP j) ('OP f)) ('OP j) Source Comments #

liftUniv :: forall (g :: OPK kk e d). Ob g => ('OP f ~> O g ('OP j)) -> 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} {d :: k} {c :: k} {e :: k} (i :: kk d c) (j :: kk d c) (f :: kk e c). (LeftKanLift j f, LeftKanLift i f) => (i ~> j) -> Lift j f ~> Lift i f 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 (Rift j f) j ~> f Source Comments #

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

Instances

Instances details

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

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

Methods

rift :: O (Rift ('PK j :: ProfK 'ProfC d c) ('PK f :: ProfK 'ProfC e c)) ('PK j :: ProfK 'ProfC d c) ~> ('PK f :: ProfK 'ProfC e c) Source Comments #

riftUniv :: forall (g :: ProfK 'ProfC e d). Ob g => (O g ('PK j :: ProfK 'ProfC d c) ~> ('PK f :: ProfK 'ProfC e c)) -> g ~> Rift ('PK j :: ProfK 'ProfC d c) ('PK f :: ProfK 'ProfC 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 (Rift ('CO j) ('CO f)) ('CO j) ~> 'CO f Source Comments #

riftUniv :: forall (g :: COK kk e d). Ob g => (O g ('CO j) ~> '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 (Rift ('OP j) ('OP f)) ('OP j) ~> 'OP f Source Comments #

riftUniv :: forall (g :: OPK kk e d). Ob g => (O g ('OP j) ~> '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} {d :: k} {c :: k} {e :: k} (i :: kk d c) (j :: kk d c) (f :: kk e c). (RightKanLift j f, RightKanLift i f) => (i ~> j) -> Rift j f ~> Rift i f Source Comments #

newtype HaskRan (g :: k -> Type) (h :: k -> Type) a Source Comments #

Constructors

Ran
Fields runRan :: forall (b :: k). (a -> g b) -> h b

Instances

Instances details

Functor (HaskRan g h :: Type -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Kan Methods map :: (a ~> b) -> HaskRan g h a ~> HaskRan g h b Source Comments #

data HaskLan (j :: k -> Type) (f :: k -> Type) a where Source Comments #

Constructors

Lan :: forall {k} (j :: k -> Type) (b :: k) a (f :: k -> Type). (j b -> a) -> f b -> HaskLan j f a

Instances

Instances details

Functor (HaskLan j f :: Type -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Kan Methods map :: (a ~> b) -> HaskLan j f a ~> HaskLan j f b Source Comments #