data-category-0.4.1: Category theory

Portabilitynon-portable
Stabilityexperimental
Maintainersjoerd@w3future.com

Data.Category.Limit

Contents

Description

 

Synopsis

Preliminairies

Diagonal Functor

data Diag whereSource

Constructors

Diag :: Diag j ~> 

Instances

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

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

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

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

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

Methods

limit :: Obj (Nat j ~>) f -> Cone f (Limit f)Source

limit returns the limiting cone for a functor f.

limitFactorizer :: Obj (Nat j ~>) f -> forall n. Cone f n -> n ~> Limit fSource

limitFactorizer shows that the limiting cone is universal  i.e. any other cone of f factors through it  by returning the morphism between the vertices of the cones.

Instances

HasTerminalObject ~> => HasLimits Void ~>

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

(HasLimits (Discrete n) ~>, HasBinaryProducts ~>) => HasLimits (Discrete (S n)) ~>

The product of n objects is the limit of the functor from Discrete n to (~>).

data LimitFunctor j (~>) Source

Constructors

LimitFunctor 

Instances

HasLimits j ~> => Functor (LimitFunctor j ~>)

If every diagram of type j has a limit in (~>) there exists a limit functor. It can be seen as a generalisation of (***).

limitAdj :: HasLimits j ~> => Adjunction (Nat j ~>) ~> (Diag j ~>) (LimitFunctor j ~>)Source

The limit functor is right adjoint to the diagonal functor.

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

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

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

Methods

colimit :: Obj (Nat j ~>) f -> Cocone f (Colimit f)Source

colimit returns the limiting co-cone for a functor f.

colimitFactorizer :: Obj (Nat j ~>) f -> forall n. Cocone f n -> Colimit f ~> nSource

colimitFactorizer shows that the limiting co-cone is universal  i.e. any other co-cone of f factors through it  by returning the morphism between the vertices of the cones.

Instances

HasInitialObject ~> => HasColimits Void ~>

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

(HasColimits (Discrete n) ~>, HasBinaryCoproducts ~>) => HasColimits (Discrete (S n)) ~>

The coproduct of n objects is the colimit of the functor from Discrete n to (~>).

data ColimitFunctor j (~>) Source

Constructors

ColimitFunctor 

Instances

HasColimits j ~> => Functor (ColimitFunctor j ~>)

If every diagram of type j has a colimit in (~>) there exists a colimit functor. It can be seen as a generalisation of (+++).

colimitAdj :: HasColimits j ~> => Adjunction ~> (Nat j ~>) (ColimitFunctor j ~>) (Diag j ~>)Source

The colimit functor is left adjoint to the diagonal functor.

Limits of type Void

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

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.

(HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (:**: c1 c2)

The terminal object of the product of 2 categories is the product of their terminal objects.

(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))

FixF also provides the terminal F-coalgebra for endofunctors in Hask.

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

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

Z (zero) is the initial object of omega.

HasInitialObject (Peano (->))

The natural numbers are the initial object for the Peano category.

(HasInitialObject c1, HasInitialObject c2) => HasInitialObject (:**: c1 c2)

The initial object of the product of 2 categories is the product of their initial objects.

(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 (->)))

FixF provides the initial F-algebra for endofunctors in Hask.

HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))

The category for defining the natural numbers and primitive recursion can be described as Dialg(F,G), with F(A)=<1,A> and G(A)=<A,A>.

Limits of type Pair

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

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

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

Instances

HasBinaryProducts (->)

The tuple is the binary product in Hask.

HasBinaryProducts Cat

The product of categories '(:**:)' is the binary product in Cat.

HasBinaryProducts Boolean

Conjunction is the binary product in the Boolean category.

HasBinaryProducts Omega

The product in omega is the minimum.

(HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (:**: c1 c2)

The binary product of the product of 2 categories is the product of their binary products.

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

The functor product '(:*:)' is the binary product in functor categories.

data ProductFunctor (~>) Source

Constructors

ProductFunctor 

Instances

HasBinaryProducts ~> => Functor (ProductFunctor ~>)

Binary product as a bifunctor.

(HasTerminalObject ~>, HasBinaryProducts ~>) => TensorProduct (ProductFunctor ~>)

If a category has all products, then the product functor makes it a monoidal category, with the terminal object as unit.

data p :*: q whereSource

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)

The product of two functors, passing the same object to both functors and taking the product of the results.

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

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

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

Instances

HasBinaryCoproducts (->)

Either is the coproduct in Hask.

HasBinaryCoproducts Cat

The coproduct of categories '(:++:)' is the binary coproduct in Cat.

HasBinaryCoproducts Boolean

Disjunction is the binary coproduct in the Boolean category.

HasBinaryCoproducts Omega

The coproduct in omega is the maximum.

(HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (:**: c1 c2)

The binary coproduct of the product of 2 categories is the product of their binary coproducts.

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

The functor coproduct '(:+:)' is the binary coproduct in functor categories.

data CoproductFunctor (~>) Source

Constructors

CoproductFunctor 

Instances

HasBinaryCoproducts ~> => Functor (CoproductFunctor ~>)

Binary coproduct as a bifunctor.

(HasInitialObject ~>, HasBinaryCoproducts ~>) => TensorProduct (CoproductFunctor ~>)

If a category has all coproducts, then the coproduct functor makes it a monoidal category, with the initial object as unit.

data p :+: q whereSource

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)

The coproduct of two functors, passing the same object to both functors and taking the coproduct of the results.