Data.Category.Limit

Preliminairies

Diagonal Functor

data Diag where

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)

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 (~>) f :: *

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

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

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

Methods

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

limit returns the limiting cone for a functor f.

limitFactorizer :: Obj (Nat j ~>) f -> forall n. Cone f n -> 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

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

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

The limit functor is right adjoint to the diagonal functor.

Colimits

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

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

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

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

Methods

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

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

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

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

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

The colimit functor is left adjoint to the diagonal functor.

Limits of type Void

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

Associated Types

type TerminalObject (~>) :: *

Methods

terminalObject :: Obj ~> (TerminalObject ~>)

terminate :: Obj ~> a -> a ~> TerminalObject ~>

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

Associated Types

type InitialObject (~>) :: *

Methods

initialObject :: Obj ~> (InitialObject ~>)

initialize :: Obj ~> a -> InitialObject ~> ~> 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 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>.

data Zero

Limits of type Pair

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

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

Methods

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

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

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

(***) :: (a1 ~> b1) -> (a2 ~> b2) -> BinaryProduct ~> a1 a2 ~> BinaryProduct ~> 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 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 (~>)

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 where

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 :: *

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

Methods

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

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

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

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

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

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 where

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.