data-category-0.5.1: Category theory

Portability non-portable experimental sjoerd@w3future.com Safe-Inferred

Data.Category.Limit

Description

Synopsis

# Preliminairies

## Diagonal Functor

data Diag whereSource

Constructors

 Diag :: Diag j k

Instances

 (Category (Dom (Diag j k)), Category (Cod (Diag j k)), Category j, Category k) => Functor (Diag j k) The diagonal functor from (index-) category J to k.

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 k f :: *Source

Limits in a category `k` by means of a diagram of type `j`, which is a functor from `j` to `k`.

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

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

An instance of `HasLimits j k` says that `k` has all limits of type `j`.

Methods

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

`limit` returns the limiting cone for a functor `f`.

limitFactorizer :: Obj (Nat j k) f -> forall n. Cone f n -> k n (Limit f)Source

`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

 (Category Unit, Category k) => HasLimits Unit k The limit of a single object is that object. (Category Void, Category k, HasTerminalObject k) => HasLimits Void k A terminal object is the limit of the functor from 0 to k. (Category (:>>: i j), HasInitialObject (:>>: i j), Category k) => HasLimits (:>>: i j) k The limit of any diagram with an initial object, has the limit at the initial object. (Category (:++: i j), Category k, HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (:++: i j) k If `k` has binary products, we can take the limit of 2 joined diagrams.

data LimitFunctor j k Source

Constructors

 LimitFunctor

Instances

 (Category (Dom (LimitFunctor j k)), Category (Cod (LimitFunctor j k)), HasLimits j k) => Functor (LimitFunctor j k) If every diagram of type `j` has a limit in `k` there exists a limit functor. It can be seen as a generalisation of `(***)`.

limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)Source

The limit functor is right adjoint to the diagonal functor.

# Colimits

type family ColimitFam j k f :: *Source

Colimits in a category `k` by means of a diagram of type `j`, which is a functor from `j` to `k`.

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

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

An instance of `HasColimits j k` says that `k` has all colimits of type `j`.

Methods

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

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

colimitFactorizer :: Obj (Nat j k) f -> forall n. Cocone f n -> k (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

 (Category Unit, Category k) => HasColimits Unit k The colimit of a single object is that object. (Category Void, Category k, HasInitialObject k) => HasColimits Void k An initial object is the colimit of the functor from 0 to k. (Category (:>>: i j), HasTerminalObject (:>>: i j), Category k) => HasColimits (:>>: i j) k The colimit of any diagram with a terminal object, has the limit at the terminal object. (Category (:++: i j), Category k, HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (:++: i j) k If `k` has binary coproducts, we can take the colimit of 2 joined diagrams.

data ColimitFunctor j k Source

Constructors

 ColimitFunctor

Instances

 (Category (Dom (ColimitFunctor j k)), Category (Cod (ColimitFunctor j k)), HasColimits j k) => Functor (ColimitFunctor j k) If every diagram of type `j` has a colimit in `k` there exists a colimit functor. It can be seen as a generalisation of `(+++)`.

colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)Source

The colimit functor is left adjoint to the diagonal functor.

## Limits of type Void

class Category k => HasTerminalObject k whereSource

Associated Types

type TerminalObject k :: *Source

Methods

terminate :: Obj k a -> k a (TerminalObject k)Source

Instances

 HasTerminalObject (->) `()` is the terminal object in `Hask`. HasTerminalObject Cat `Unit` is the terminal category. HasTerminalObject Unit The category of one object has that object as terminal object. HasTerminalObject Boolean True is the terminal object in the Boolean category. HasTerminalObject Simplex The ordinal `1` is the terminal object of the simplex category. (Category (Op k), HasInitialObject k) => HasTerminalObject (Op k) Terminal objects are the dual of initial objects. (Category (Fix f), HasTerminalObject (f (Fix f))) => HasTerminalObject (Fix f) `Fix f` inherits its (co)limits from `f (Fix f)`. (Category (:**: c1 c2), HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (:**: c1 c2) The terminal object of the product of 2 categories is the product of their terminal objects. (Category (Nat c d), Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) The constant functor to the terminal object is itself the terminal object in its functor category. (Category (:>>: c1 c2), Category c1, HasTerminalObject c2) => HasTerminalObject (:>>: c1 c2) The terminal object of the direct coproduct of categories is the terminal object of the terminal category.

class Category k => HasInitialObject k whereSource

Associated Types

type InitialObject k :: *Source

Methods

initialize :: Obj k a -> k (InitialObject k) aSource

Instances

 HasInitialObject (->) Any empty data type is an initial object in `Hask`. HasInitialObject Cat The empty category is the initial object in `Cat`. HasInitialObject Unit The category of one object has that object as initial object. HasInitialObject Boolean False is the initial object in the Boolean category. HasInitialObject Simplex The ordinal `0` is the initial object of the simplex category. (Category (Op k), HasTerminalObject k) => HasInitialObject (Op k) Terminal objects are the dual of initial objects. (Category (Fix f), HasInitialObject (f (Fix f))) => HasInitialObject (Fix f) `Fix f` inherits its (co)limits from `f (Fix f)`. (Category (:**: c1 c2), HasInitialObject c1, HasInitialObject c2) => HasInitialObject (:**: c1 c2) The initial object of the product of 2 categories is the product of their initial objects. (Category (Nat c d), Category c, HasInitialObject d) => HasInitialObject (Nat c d) The constant functor to the initial object is itself the initial object in its functor category. (Category (:>>: c1 c2), HasInitialObject c1, Category c2) => HasInitialObject (:>>: c1 c2) The initial object of the direct coproduct of categories is the initial object of the initial category. 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)=`.

## Limits of type Pair

class Category k => HasBinaryProducts k whereSource

Associated Types

type BinaryProduct k x y :: *Source

Methods

proj1 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) xSource

proj2 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) ySource

(&&&) :: k a x -> k a y -> k a (BinaryProduct k x y)Source

(***) :: k a1 b1 -> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)Source

Instances

 HasBinaryProducts (->) The tuple is the binary product in `Hask`. HasBinaryProducts Cat The product of categories `:**:` is the binary product in `Cat`. HasBinaryProducts Unit In the category of one object that object is its own product. HasBinaryProducts Boolean Conjunction is the binary product in the Boolean category. (Category (Op k), HasBinaryCoproducts k) => HasBinaryProducts (Op k) Binary products are the dual of binary coproducts. (Category (Fix f), HasBinaryProducts (f (Fix f))) => HasBinaryProducts (Fix f) `Fix f` inherits its (co)limits from `f (Fix f)`. (Category (:**: c1 c2), HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (:**: c1 c2) The binary product of the product of 2 categories is the product of their binary products. (Category (Nat c d), Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) The functor product `:*:` is the binary product in functor categories. (Category (:>>: c1 c2), HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (:>>: c1 c2)

data ProductFunctor k Source

Constructors

 ProductFunctor

Instances

 (Category (Dom (ProductFunctor k)), Category (Cod (ProductFunctor k)), HasBinaryProducts k) => Functor (ProductFunctor k) Binary product as a bifunctor. (Functor (ProductFunctor k), ~ (* -> * -> *) (Dom (ProductFunctor k)) (:**: (Cod (ProductFunctor k)) (Cod (ProductFunctor k))), HasTerminalObject k, HasBinaryProducts k) => TensorProduct (ProductFunctor k) 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 ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q

Instances

 (Category (Dom (:*: p q)), Category (Cod (:*: p q)), 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.

class Category k => HasBinaryCoproducts k whereSource

Associated Types

type BinaryCoproduct k x y :: *Source

Methods

inj1 :: Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)Source

inj2 :: Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)Source

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

(+++) :: k a1 b1 -> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)Source

Instances

 HasBinaryCoproducts Cat The coproduct of categories `:++:` is the binary coproduct in `Cat`. HasBinaryCoproducts Unit In the category of one object that object is its own coproduct. HasBinaryCoproducts Boolean Disjunction is the binary coproduct in the Boolean category. HasBinaryCoproducts Simplex The coproduct in the simplex category is a merge operation. (Category (Op k), HasBinaryProducts k) => HasBinaryCoproducts (Op k) Binary products are the dual of binary coproducts. (Category (Fix f), HasBinaryCoproducts (f (Fix f))) => HasBinaryCoproducts (Fix f) `Fix f` inherits its (co)limits from `f (Fix f)`. (Category (:**: c1 c2), HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (:**: c1 c2) The binary coproduct of the product of 2 categories is the product of their binary coproducts. (Category (Nat c d), Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) The functor coproduct `:+:` is the binary coproduct in functor categories. (Category (:>>: c1 c2), HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (:>>: c1 c2)

Constructors

 CoproductFunctor

Instances

 (Category (Dom (CoproductFunctor k)), Category (Cod (CoproductFunctor k)), HasBinaryCoproducts k) => Functor (CoproductFunctor k) Binary coproduct as a bifunctor. (Functor (CoproductFunctor k), ~ (* -> * -> *) (Dom (CoproductFunctor k)) (:**: (Cod (CoproductFunctor k)) (Cod (CoproductFunctor k))), HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k) 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 ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q

Instances

 (Category (Dom (:+: p q)), Category (Cod (:+: p q)), 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.