License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Category.KanExtension

Description

Synopsis

class (Functor p, Category k) => HasRightKan p k where
- type RanFam p k (f :: Type) :: Type
- ran :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f
- ranFactorizer :: Nat (Dom p) k (h :.: p) f -> Nat (Cod p) k h (RanFam p 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)
newtype RanFunctor (p :: Type) (k :: Type -> Type -> Type) = RanFunctor p
ranAdj :: forall p k. HasRightKan p k => p -> Adjunction (Nat (Dom p) k) (Nat (Cod p) k) (Precompose p k) (RanFunctor p k)
class (Functor p, Category k) => HasLeftKan p k where
- type LanFam (p :: Type) (k :: Type -> Type -> Type) (f :: Type) :: Type
- lan :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)
- lanFactorizer :: Nat (Dom p) k f (h :.: p) -> Nat (Cod p) k (LanFam p 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)
newtype LanFunctor (p :: Type) (k :: Type -> Type -> Type) = LanFunctor p
lanAdj :: forall p k. HasLeftKan p k => p -> Adjunction (Nat (Cod p) k) (Nat (Dom p) k) (LanFunctor p k) (Precompose p k)
newtype RanHask p f a = RanHask (forall c. Obj (Dom p) c -> Cod p a (p :% c) -> f :% c)
data RanHaskF p f = RanHaskF
data LanHask p f a where
- LanHask :: Obj (Dom p) c -> Cod p (p :% c) a -> (f :% c) -> LanHask p f a
data LanHaskF p f = LanHaskF

Documentation

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

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 :: Type) :: Type Source #

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

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) Source #

ranFactorizer shows that this extension is universal.

Instances

Instances details

(Category j, Category k) => HasRightKan (Id j) k Source #	Ran id = id
Instance details Defined in Data.Category.KanExtension Associated Types type RanFam (Id j) k f Source # Methods ran :: Id j -> Obj (Nat (Dom (Id j)) k) f -> Nat (Dom (Id j)) k (RanFam (Id j) k f :.: Id j) f Source # ranFactorizer :: Nat (Dom (Id j)) k (h :.: Id j) f -> Nat (Cod (Id j)) k h (RanFam (Id j) k f) Source #
Functor p => HasRightKan (Any p) (->) Source #
Instance details Defined in Data.Category.KanExtension Associated Types type RanFam (Any p) (->) f Source # Methods ran :: Any p -> Obj (Nat (Dom (Any p)) (->)) f -> Nat (Dom (Any p)) (->) (RanFam (Any p) (->) f :.: Any p) f Source # ranFactorizer :: Nat (Dom (Any p)) (->) (h :.: Any p) f -> Nat (Cod (Any p)) (->) h (RanFam (Any p) (->) f) Source #
(HasRightKan q k, HasRightKan p k) => HasRightKan (q :.: p) k Source #	Ran (q . p) = Ran q . Ran p
Instance details Defined in Data.Category.KanExtension Associated Types type RanFam (q :.: p) k f Source # Methods ran :: (q :.: p) -> Obj (Nat (Dom (q :.: p)) k) f -> Nat (Dom (q :.: p)) k (RanFam (q :.: p) k f :.: (q :.: p)) f Source # ranFactorizer :: Nat (Dom (q :.: p)) k (h :.: (q :.: p)) f -> Nat (Cod (q :.: p)) k h (RanFam (q :.: p) k f) Source #
HasLimits j k => HasRightKan (Const j Unit ()) k Source #	The right Kan extension of `f` along a functor to the unit category is the limit of `f`.
Instance details Defined in Data.Category.KanExtension Associated Types type RanFam (Const j Unit ()) k f Source # 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 Source # 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) Source #

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

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

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

newtype RanFunctor (p :: Type) (k :: Type -> Type -> Type) Source #

Constructors

RanFunctor p

Instances

Instances details

HasRightKan p k => Functor (RanFunctor p k) Source #
Instance details Defined in Data.Category.KanExtension Associated Types type Dom (RanFunctor p k) :: Type -> Type -> Type Source # type Cod (RanFunctor p k) :: Type -> Type -> Type Source # type (RanFunctor p k) :% a Source # Methods (%) :: RanFunctor p k -> Dom (RanFunctor p k) a b -> Cod (RanFunctor p k) (RanFunctor p k :% a) (RanFunctor p k :% b) Source #
type Cod (RanFunctor p k) Source #
Instance details Defined in Data.Category.KanExtension type Cod (RanFunctor p k) = Nat (Cod p) k
type Dom (RanFunctor p k) Source #
Instance details Defined in Data.Category.KanExtension type Dom (RanFunctor p k) = Nat (Dom p) k
type (RanFunctor p k) :% f Source #
Instance details 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) Source #

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

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

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

Associated Types

type LanFam (p :: Type) (k :: Type -> Type -> Type) (f :: Type) :: Type Source #

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) Source #

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

lanFactorizer shows that this extension is universal.

Instances

Instances details

(Category j, Category k) => HasLeftKan (Id j) k Source #	Lan id = id
Instance details Defined in Data.Category.KanExtension Associated Types type LanFam (Id j) k f Source # Methods lan :: Id j -> Obj (Nat (Dom (Id j)) k) f -> Nat (Dom (Id j)) k f (LanFam (Id j) k f :.: Id j) Source # lanFactorizer :: Nat (Dom (Id j)) k f (h :.: Id j) -> Nat (Cod (Id j)) k (LanFam (Id j) k f) h Source #
Functor p => HasLeftKan (Any p) (->) Source #
Instance details Defined in Data.Category.KanExtension Associated Types type LanFam (Any p) (->) f Source # Methods lan :: Any p -> Obj (Nat (Dom (Any p)) (->)) f -> Nat (Dom (Any p)) (->) f (LanFam (Any p) (->) f :.: Any p) Source # lanFactorizer :: Nat (Dom (Any p)) (->) f (h :.: Any p) -> Nat (Cod (Any p)) (->) (LanFam (Any p) (->) f) h Source #
(HasLeftKan q k, HasLeftKan p k) => HasLeftKan (q :.: p) k Source #	Lan (q . p) = Lan q . Lan p
Instance details Defined in Data.Category.KanExtension Associated Types type LanFam (q :.: p) k f Source # Methods lan :: (q :.: p) -> Obj (Nat (Dom (q :.: p)) k) f -> Nat (Dom (q :.: p)) k f (LanFam (q :.: p) k f :.: (q :.: p)) Source # lanFactorizer :: Nat (Dom (q :.: p)) k f (h :.: (q :.: p)) -> Nat (Cod (q :.: p)) k (LanFam (q :.: p) k f) h Source #
HasColimits j k => HasLeftKan (Const j Unit ()) k Source #	The left Kan extension of `f` along a functor to the unit category is the colimit of `f`.
Instance details Defined in Data.Category.KanExtension Associated Types type LanFam (Const j Unit ()) k f Source # 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 ()) Source # 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 Source #

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

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

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

newtype LanFunctor (p :: Type) (k :: Type -> Type -> Type) Source #

Constructors

LanFunctor p

Instances

Instances details

HasLeftKan p k => Functor (LanFunctor p k) Source #
Instance details Defined in Data.Category.KanExtension Associated Types type Dom (LanFunctor p k) :: Type -> Type -> Type Source # type Cod (LanFunctor p k) :: Type -> Type -> Type Source # type (LanFunctor p k) :% a Source # Methods (%) :: LanFunctor p k -> Dom (LanFunctor p k) a b -> Cod (LanFunctor p k) (LanFunctor p k :% a) (LanFunctor p k :% b) Source #
type Cod (LanFunctor p k) Source #
Instance details Defined in Data.Category.KanExtension type Cod (LanFunctor p k) = Nat (Cod p) k
type Dom (LanFunctor p k) Source #
Instance details Defined in Data.Category.KanExtension type Dom (LanFunctor p k) = Nat (Dom p) k
type (LanFunctor p k) :% f Source #
Instance details 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) Source #

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

newtype RanHask p f a Source #

Constructors

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

data RanHaskF p f Source #

Constructors

RanHaskF

Instances

Instances details

Functor p => Functor (RanHaskF p f) Source #
Instance details Defined in Data.Category.KanExtension Associated Types type Dom (RanHaskF p f) :: Type -> Type -> Type Source # type Cod (RanHaskF p f) :: Type -> Type -> Type Source # type (RanHaskF p f) :% a Source # Methods (%) :: RanHaskF p f -> Dom (RanHaskF p f) a b -> Cod (RanHaskF p f) (RanHaskF p f :% a) (RanHaskF p f :% b) Source #
type Cod (RanHaskF p f) Source #
Instance details Defined in Data.Category.KanExtension type Cod (RanHaskF p f) = (->)
type Dom (RanHaskF p f) Source #
Instance details Defined in Data.Category.KanExtension type Dom (RanHaskF p f) = Cod p
type (RanHaskF p f) :% a Source #
Instance details Defined in Data.Category.KanExtension type (RanHaskF p f) :% a = RanHask p f a

data LanHask p f a where Source #

Constructors

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

data LanHaskF p f Source #

Constructors

LanHaskF

Instances

Instances details

Functor p => Functor (LanHaskF p f) Source #
Instance details Defined in Data.Category.KanExtension Associated Types type Dom (LanHaskF p f) :: Type -> Type -> Type Source # type Cod (LanHaskF p f) :: Type -> Type -> Type Source # type (LanHaskF p f) :% a Source # Methods (%) :: LanHaskF p f -> Dom (LanHaskF p f) a b -> Cod (LanHaskF p f) (LanHaskF p f :% a) (LanHaskF p f :% b) Source #
type Cod (LanHaskF p f) Source #
Instance details Defined in Data.Category.KanExtension type Cod (LanHaskF p f) = (->)
type Dom (LanHaskF p f) Source #
Instance details Defined in Data.Category.KanExtension type Dom (LanHaskF p f) = Cod p
type (LanHaskF p f) :% a Source #
Instance details Defined in Data.Category.KanExtension type (LanHaskF p f) :% a = LanHask p f a