Data.Category.Limit

Preliminairies

Diagonal Functor

data Diag where

Constructors

Diag :: Diag j k

Instances

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

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

Cones

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

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)

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

The vertex (or apex) of a cone.

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

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

Limits

type family LimitFam j k f :: *

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

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

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)

limit returns the limiting cone for a functor f.

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

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 k => HasLimits Unit k

The limit of a single object is that object.

HasTerminalObject k => HasLimits Void k

A terminal object is the limit of the functor from 0 to k.

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

(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

Constructors

LimitFunctor

Instances

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)

The limit functor is right adjoint to the diagonal functor.

Colimits

type family ColimitFam j k f :: *

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

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

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)

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

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

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 k => HasColimits Unit k

The colimit of a single object is that object.

HasInitialObject k => HasColimits Void k

An initial object is the colimit of the functor from 0 to k.

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

(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

Constructors

ColimitFunctor

Instances

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)

The colimit functor is left adjoint to the diagonal functor.

Limits of type Void

class Category k => HasTerminalObject k where

Associated Types

type TerminalObject k :: *

Methods

terminalObject :: Obj k (TerminalObject k)

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

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.

HasInitialObject k => HasTerminalObject (Op k)

Terminal objects are the dual of initial objects.

HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f)

Fix f inherits its (co)limits from f (Fix f).

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

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

Associated Types

type InitialObject k :: *

Methods

initialObject :: Obj k (InitialObject k)

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

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.

HasTerminalObject k => HasInitialObject (Op k)

Terminal objects are the dual of initial objects.

HasInitialObject (f (Fix f)) => HasInitialObject (Fix f)

Fix f inherits its (co)limits from f (Fix f).

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

(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)=<A,A>.

data Zero

Limits of type Pair

class Category k => HasBinaryProducts k where

Associated Types

type BinaryProduct k x y :: *

Methods

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

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

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

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

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.

HasBinaryCoproducts k => HasBinaryProducts (Op k)

Binary products are the dual of binary coproducts.

HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f)

Fix f inherits its (co)limits from f (Fix f).

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

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

data ProductFunctor k

Constructors

ProductFunctor

Instances

HasBinaryProducts k => Functor (ProductFunctor k)

Binary product as a bifunctor.

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

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), 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 where

Associated Types

type BinaryCoproduct k x y :: *

Methods

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

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

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

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

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.

HasBinaryProducts k => HasBinaryCoproducts (Op k)

Binary products are the dual of binary coproducts.

HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f)

Fix f inherits its (co)limits from f (Fix f).

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

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

data CoproductFunctor k

Constructors

CoproductFunctor

Instances

HasBinaryCoproducts k => Functor (CoproductFunctor k)

Binary coproduct as a bifunctor.

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

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), 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.