Data.Category.KanExtension

Documentation

class (Functor p, Category k) => HasRightKan p k where

An instance of HasRightKan p k says there are right Kan extensions for all functors with codomain k.

Associated Types

type RanFam p k (f :: *) :: *

The right Kan extension of a functor p for functors f with codomain k.

Methods

ran :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f

ran gives the defining natural transformation of the right Kan extension of f along p.

ranFactorizer :: Nat (Dom p) k (h :.: p) f -> Nat (Cod p) k h (RanFam p k f)

ranFactorizer shows that this extension is universal.

Instances

(Category j, Category k) => HasRightKan (Id j) k

Ran id = id

Defined in Data.Category.KanExtension

Associated Types

type RanFam (Id j) k f :: Type

Methods

ran :: Id j -> Obj (Nat (Dom (Id j)) k) f -> Nat (Dom (Id j)) k (RanFam (Id j) k f :.: Id j) f

ranFactorizer :: Nat (Dom (Id j)) k (h :.: Id j) f -> Nat (Cod (Id j)) k h (RanFam (Id j) k f)

Functor p => HasRightKan (Any p) ((->) :: Type -> Type -> Type)

Defined in Data.Category.KanExtension

Associated Types

type RanFam (Any p) (->) f :: Type

Methods

ran :: Any p -> Obj (Nat (Dom (Any p)) (->)) f -> Nat (Dom (Any p)) (->) (RanFam (Any p) (->) f :.: Any p) f

ranFactorizer :: Nat (Dom (Any p)) (->) (h :.: Any p) f -> Nat (Cod (Any p)) (->) h (RanFam (Any p) (->) f)

(HasRightKan q k, HasRightKan p k) => HasRightKan (q :.: p) k

Ran (q . p) = Ran q . Ran p

Defined in Data.Category.KanExtension

Associated Types

type RanFam (q :.: p) k f :: Type

Methods

ran :: (q :.: p) -> Obj (Nat (Dom (q :.: p)) k) f -> Nat (Dom (q :.: p)) k (RanFam (q :.: p) k f :.: (q :.: p)) f

ranFactorizer :: Nat (Dom (q :.: p)) k (h :.: (q :.: p)) f -> Nat (Cod (q :.: p)) k h (RanFam (q :.: p) k f)

HasLimits j k => HasRightKan (Const j Unit ()) k

The right Kan extension of f along a functor to the unit category is the limit of f.

Defined in Data.Category.KanExtension

Associated Types

type RanFam (Const j Unit ()) k f :: Type

Methods

ran :: Const j Unit () -> Obj (Nat (Dom (Const j Unit ())) k) f -> Nat (Dom (Const j Unit ())) k (RanFam (Const j Unit ()) k f :.: Const j Unit ()) f

ranFactorizer :: Nat (Dom (Const j Unit ())) k (h :.: Const j Unit ()) f -> Nat (Cod (Const j Unit ())) k h (RanFam (Const j Unit ()) k f)

type Ran p f = RanFam p (Cod f) f

ranF :: HasRightKan p k => p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (RanFam p k f)

ranF' :: Nat (Dom p) k (RanFam p k f :.: p) f -> Obj (Nat (Cod p) k) (RanFam p k f)

data RanFunctor (p :: *) (k :: * -> * -> *)

Constructors

RanFunctor p

Instances

HasRightKan p k => Functor (RanFunctor p k)

Defined in Data.Category.KanExtension

Associated Types

type Dom (RanFunctor p k) :: Type -> Type -> Type

type Cod (RanFunctor p k) :: Type -> Type -> Type

type (RanFunctor p k) :% a :: Type

Methods

(%) :: RanFunctor p k -> Dom (RanFunctor p k) a b -> Cod (RanFunctor p k) (RanFunctor p k :% a) (RanFunctor p k :% b)

type Dom (RanFunctor p k)

Defined in Data.Category.KanExtension

type Dom (RanFunctor p k) = Nat (Dom p) k

type Cod (RanFunctor p k)

Defined in Data.Category.KanExtension

type Cod (RanFunctor p k) = Nat (Cod p) k

type (RanFunctor p k) :% f

Defined in Data.Category.KanExtension

type (RanFunctor p k) :% f = RanFam p k f

ranAdj :: forall p k. HasRightKan p k => p -> Adjunction (Nat (Dom p) k) (Nat (Cod p) k) (Precompose p k) (RanFunctor p k)

The right Kan extension along p is right adjoint to precomposition with p.

class (Functor p, Category k) => HasLeftKan p k where

An instance of HasLeftKan p k says there are left Kan extensions for all functors with codomain k.

Associated Types

type LanFam (p :: *) (k :: * -> * -> *) (f :: *) :: *

The left Kan extension of a functor p for functors f with codomain k.

Methods

lan :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)

lan gives the defining natural transformation of the left Kan extension of f along p.

lanFactorizer :: Nat (Dom p) k f (h :.: p) -> Nat (Cod p) k (LanFam p k f) h

lanFactorizer shows that this extension is universal.

Instances

(Category j, Category k) => HasLeftKan (Id j) k

Lan id = id

Defined in Data.Category.KanExtension

Associated Types

type LanFam (Id j) k f :: Type

Methods

lan :: Id j -> Obj (Nat (Dom (Id j)) k) f -> Nat (Dom (Id j)) k f (LanFam (Id j) k f :.: Id j)

lanFactorizer :: Nat (Dom (Id j)) k f (h :.: Id j) -> Nat (Cod (Id j)) k (LanFam (Id j) k f) h

Functor p => HasLeftKan (Any p) ((->) :: Type -> Type -> Type)

Defined in Data.Category.KanExtension

Associated Types

type LanFam (Any p) (->) f :: Type

Methods

lan :: Any p -> Obj (Nat (Dom (Any p)) (->)) f -> Nat (Dom (Any p)) (->) f (LanFam (Any p) (->) f :.: Any p)

lanFactorizer :: Nat (Dom (Any p)) (->) f (h :.: Any p) -> Nat (Cod (Any p)) (->) (LanFam (Any p) (->) f) h

(HasLeftKan q k, HasLeftKan p k) => HasLeftKan (q :.: p) k

Lan (q . p) = Lan q . Lan p

Defined in Data.Category.KanExtension

Associated Types

type LanFam (q :.: p) k f :: Type

Methods

lan :: (q :.: p) -> Obj (Nat (Dom (q :.: p)) k) f -> Nat (Dom (q :.: p)) k f (LanFam (q :.: p) k f :.: (q :.: p))

lanFactorizer :: Nat (Dom (q :.: p)) k f (h :.: (q :.: p)) -> Nat (Cod (q :.: p)) k (LanFam (q :.: p) k f) h

HasColimits j k => HasLeftKan (Const j Unit ()) k

The left Kan extension of f along a functor to the unit category is the colimit of f.

Defined in Data.Category.KanExtension

Associated Types

type LanFam (Const j Unit ()) k f :: Type

Methods

lan :: Const j Unit () -> Obj (Nat (Dom (Const j Unit ())) k) f -> Nat (Dom (Const j Unit ())) k f (LanFam (Const j Unit ()) k f :.: Const j Unit ())

lanFactorizer :: Nat (Dom (Const j Unit ())) k f (h :.: Const j Unit ()) -> Nat (Cod (Const j Unit ())) k (LanFam (Const j Unit ()) k f) h

type Lan p f = LanFam p (Cod f) f

lanF :: HasLeftKan p k => p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (LanFam p k f)

lanF' :: Nat (Dom p) k f (LanFam p k f :.: p) -> Obj (Nat (Cod p) k) (LanFam p k f)

data LanFunctor (p :: *) (k :: * -> * -> *)

Constructors

LanFunctor p

Instances

HasLeftKan p k => Functor (LanFunctor p k)

Defined in Data.Category.KanExtension

Associated Types

type Dom (LanFunctor p k) :: Type -> Type -> Type

type Cod (LanFunctor p k) :: Type -> Type -> Type

type (LanFunctor p k) :% a :: Type

Methods

(%) :: LanFunctor p k -> Dom (LanFunctor p k) a b -> Cod (LanFunctor p k) (LanFunctor p k :% a) (LanFunctor p k :% b)

type Dom (LanFunctor p k)

Defined in Data.Category.KanExtension

type Dom (LanFunctor p k) = Nat (Dom p) k

type Cod (LanFunctor p k)

Defined in Data.Category.KanExtension

type Cod (LanFunctor p k) = Nat (Cod p) k

type (LanFunctor p k) :% f

Defined in Data.Category.KanExtension

type (LanFunctor p k) :% f = LanFam p k f

lanAdj :: forall p k. HasLeftKan p k => p -> Adjunction (Nat (Cod p) k) (Nat (Dom p) k) (LanFunctor p k) (Precompose p k)

The left Kan extension along p is left adjoint to precomposition with p.

newtype RanHask p f a

Constructors

RanHask (forall c. Obj (Dom p) c -> Cod p a (p :% c) -> f :% c)

data RanHaskF p f

Constructors

RanHaskF

Instances

Functor p => Functor (RanHaskF p f)

Defined in Data.Category.KanExtension

Associated Types

type Dom (RanHaskF p f) :: Type -> Type -> Type

type Cod (RanHaskF p f) :: Type -> Type -> Type

type (RanHaskF p f) :% a :: Type

Methods

(%) :: RanHaskF p f -> Dom (RanHaskF p f) a b -> Cod (RanHaskF p f) (RanHaskF p f :% a) (RanHaskF p f :% b)

type Dom (RanHaskF p f)

Defined in Data.Category.KanExtension

type Dom (RanHaskF p f) = Cod p

type Cod (RanHaskF p f)

Defined in Data.Category.KanExtension

type Cod (RanHaskF p f) = ((->) :: Type -> Type -> Type)

type (RanHaskF p f) :% a

Defined in Data.Category.KanExtension

type (RanHaskF p f) :% a = RanHask p f a

data LanHask p f a where

Constructors

LanHask :: Obj (Dom p) c -> Cod p (p :% c) a -> (f :% c) -> LanHask p f a

data LanHaskF p f

Constructors

LanHaskF

Instances

Functor p => Functor (LanHaskF p f)

Defined in Data.Category.KanExtension

Associated Types

type Dom (LanHaskF p f) :: Type -> Type -> Type

type Cod (LanHaskF p f) :: Type -> Type -> Type

type (LanHaskF p f) :% a :: Type

Methods

(%) :: LanHaskF p f -> Dom (LanHaskF p f) a b -> Cod (LanHaskF p f) (LanHaskF p f :% a) (LanHaskF p f :% b)

type Dom (LanHaskF p f)

Defined in Data.Category.KanExtension

type Dom (LanHaskF p f) = Cod p

type Cod (LanHaskF p f)

Defined in Data.Category.KanExtension

type Cod (LanHaskF p f) = ((->) :: Type -> Type -> Type)

type (LanHaskF p f) :% a

Defined in Data.Category.KanExtension

type (LanHaskF p f) :% a = LanHask p f a