data-category-0.3.0.2: Restricted categories

Portabilitynon-portable
Stabilityexperimental
Maintainersjoerd@w3future.com

Data.Category.Limit

Contents

Description

 

Synopsis

Preliminairies

Diagonal Functor

data Diag whereSource

The diagonal functor from (index-) category J to (~>).

Constructors

Diag :: Diag j ~> 

Instances

(Category j, Category ~>) => Functor (Diag j ~>) 

type DiagF f = Diag (Dom f) (Cod f)Source

The diagonal functor with the same domain and codomain as f.

Cones

type Cone f n = Nat (Dom f) (Cod f) (ConstF f n) fSource

A cone from N to F is a natural transformation from the constant functor to N to F.

type Cocone f n = Nat (Dom f) (Cod f) f (ConstF f n)Source

A co-cone from F to N is a natural transformation from F to the constant functor to N.

coneVertex :: Cone f n -> Obj (Cod f) nSource

The vertex (or apex) of a cone.

coconeVertex :: Cocone f n -> Obj (Cod f) nSource

The vertex (or apex) of a co-cone.

Limits

type family LimitFam j (~>) f :: *Source

Limits in a category (~>) by means of a diagram of type j, which is a functor from j to (~>).

type Limit f = LimitFam (Dom f) (Cod f) fSource

type LimitUniversal f = TerminalUniversal f (DiagF f) (Limit f)Source

A limit of f is a universal morphism from the diagonal functor to f.

limitUniversal :: Cod f ~ ~> => Cone f (Limit f) -> (forall n. Cone f n -> n ~> Limit f) -> LimitUniversal fSource

limitUniversal is a helper function to create the universal property from the limit and the limit factorizer.

limit :: LimitUniversal f -> Cone f (Limit f)Source

A limit of the diagram f is a cone of f.

limitFactorizer :: Cod f ~ ~> => LimitUniversal f -> forall n. Cone f n -> n ~> Limit fSource

For any other cone of f with vertex n there exists a unique morphism from n to the limit of f.

Colimits

type family ColimitFam j (~>) f :: *Source

Colimits in a category (~>) by means of a diagram of type j, which is a functor from j to (~>).

type Colimit f = ColimitFam (Dom f) (Cod f) fSource

type ColimitUniversal f = InitialUniversal f (DiagF f) (Colimit f)Source

A colimit of f is a universal morphism from f to the diagonal functor.

colimitUniversal :: Cod f ~ ~> => Cocone f (Colimit f) -> (forall n. Cocone f n -> Colimit f ~> n) -> ColimitUniversal fSource

colimitUniversal is a helper function to create the universal property from the colimit and the colimit factorizer.

colimit :: ColimitUniversal f -> Cocone f (Colimit f)Source

A colimit of the diagram f is a co-cone of f.

colimitFactorizer :: Cod f ~ ~> => ColimitUniversal f -> forall n. Cocone f n -> Colimit f ~> nSource

For any other co-cone of f with vertex n there exists a unique morphism from the colimit of f to n.

Limits of a certain type

class (Category j, Category ~>) => HasLimits j (~>) whereSource

An instance of HasLimits j (~>) says that (~>) has all limits of type j.

Methods

limitUniv :: Obj (Nat j ~>) f -> LimitUniversal fSource

class (Category j, Category ~>) => HasColimits j (~>) whereSource

An instance of HasColimits j (~>) says that (~>) has all colimits of type j.

Methods

colimitUniv :: Obj (Nat j ~>) f -> ColimitUniversal fSource

As a functor

data LimitFunctor whereSource

If every diagram of type j has a limit in (~>) there exists a limit functor.

Applied to a natural transformation it is a generalisation of (***):

l *** r = LimitFunctor % arrowPair l r

Constructors

LimitFunctor :: HasLimits j ~> => LimitFunctor j ~> 

Instances

data ColimitFunctor whereSource

If every diagram of type j has a colimit in (~>) there exists a colimit functor.

Applied to a natural transformation it is a generalisation of (+++):

l +++ r = ColimitFunctor % arrowPair l r

Constructors

ColimitFunctor :: HasColimits j ~> => ColimitFunctor j ~> 

Instances

Limits of type Void

class Category ~> => HasTerminalObject (~>) whereSource

A terminal object is the limit of the functor from 0 to (~>).

Associated Types

type TerminalObject (~>) :: *Source

Instances

HasTerminalObject (->)

() is the terminal object in Hask.

HasTerminalObject Cat

Unit is the terminal category.

HasTerminalObject Boolean

True is the terminal object in the Boolean category.

(Category c, HasTerminalObject d) => HasTerminalObject (Nat c d)

The constant functor to the terminal object is itself the terminal object in its functor category.

Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) 

class Category ~> => HasInitialObject (~>) whereSource

An initial object is the colimit of the functor from 0 to (~>).

Associated Types

type InitialObject (~>) :: *Source

Instances

HasInitialObject (->)

Any empty data type is an initial object in Hask.

HasInitialObject Cat

The empty category is the initial object in Cat.

HasInitialObject Boolean

False is the initial object in the Boolean category.

HasInitialObject Omega 
HasInitialObject (Peano (->)) 
(Category c, HasInitialObject d) => HasInitialObject (Nat c d)

The constant functor to the initial object is itself the initial object in its functor category.

Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) 
HasInitialObject (Dialg (NatF (->)) (DiagProd (->))) 

Limits of type Pair

type family BinaryProduct (~>) x y :: *Source

class Category ~> => HasBinaryProducts (~>) whereSource

The product of 2 objects is the limit of the functor from Pair to (~>).

Methods

proj1 :: Obj ~> x -> Obj ~> y -> BinaryProduct ~> x y ~> xSource

proj2 :: Obj ~> x -> Obj ~> y -> BinaryProduct ~> x y ~> ySource

(&&&) :: (a ~> x) -> (a ~> y) -> a ~> BinaryProduct ~> x ySource

(***) :: (a1 ~> b1) -> (a2 ~> b2) -> BinaryProduct ~> a1 a2 ~> BinaryProduct ~> b1 b2Source

data p :*: q whereSource

The product of two functors.

Constructors

:*: :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ ~>, Cod q ~ ~>, HasBinaryProducts ~>) => p -> q -> p :*: q 

Instances

(Category (Dom p), Category (Cod p)) => Functor (:*: p q) 

type family BinaryCoproduct (~>) x y :: *Source

class Category ~> => HasBinaryCoproducts (~>) whereSource

The coproduct of 2 objects is the colimit of the functor from Pair to (~>).

Methods

inj1 :: Obj ~> x -> Obj ~> y -> x ~> BinaryCoproduct ~> x ySource

inj2 :: Obj ~> x -> Obj ~> y -> y ~> BinaryCoproduct ~> x ySource

(|||) :: (x ~> a) -> (y ~> a) -> BinaryCoproduct ~> x y ~> aSource

(+++) :: (a1 ~> b1) -> (a2 ~> b2) -> BinaryCoproduct ~> a1 a2 ~> BinaryCoproduct ~> b1 b2Source

data p :+: q whereSource

The coproduct of two functors.

Constructors

:+: :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ ~>, Cod q ~ ~>, HasBinaryCoproducts ~>) => p -> q -> p :+: q 

Instances

(Category (Dom p), Category (Cod p)) => Functor (:+: p q) 

Limits of type Hask

newtype ForAll f Source

Constructors

ForAll 

Fields

unForAll :: forall a. f a
 

data Exists f Source

Constructors

forall a . Exists (f a)