data-category-0.11: Category theory
LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Category.KanExtension

Description

 
Synopsis

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