data-category-0.4.1: Category theory

Portability non-portable experimental sjoerd@w3future.com

Data.Category.Limit

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

Methods

terminate :: Obj ~> a -> a ~> 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)=`.

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