data-category-0.2.0: Restricted categories

Portability non-portable experimental sjoerd@w3future.com

Data.Category.Limit

Description

Synopsis

# Prelimiairies

## Diagonal Functor

data Diag whereSource

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

Constructors

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

Instances

 Functor (Diag j ~>)

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

type LimitUniversal f = TerminalUniversal f (DiagF f) (Limit f)Source

A limit of `f` is a universal morphism from the diagonal functor to `f`.

limitUniversal :: Cod f ~ ~> => Cone f (Limit f) -> (forall n. Cone f n -> n ~> Limit f) -> LimitUniversal fSource

`limitUniversal` is a helper function to create the universal property from the limit and the limit factorizer.

limit :: LimitUniversal f -> Cone f (Limit f)Source

A limit of the diagram `f` is a cone of `f`.

limitFactorizer :: Cod f ~ ~> => LimitUniversal f -> forall n. Cone f n -> n ~> Limit fSource

For any other cone of `f` with vertex `n` there exists a unique morphism from `n` to the limit of `f`.

# 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

type ColimitUniversal f = InitialUniversal f (DiagF f) (Colimit f)Source

A colimit of `f` is a universal morphism from `f` to the diagonal functor.

colimitUniversal :: Cod f ~ ~> => Cocone f (Colimit f) -> (forall n. Cocone f n -> Colimit f ~> n) -> ColimitUniversal fSource

`colimitUniversal` is a helper function to create the universal property from the colimit and the colimit factorizer.

colimit :: ColimitUniversal f -> Cocone f (Colimit f)Source

A colimit of the diagram `f` is a co-cone of `f`.

colimitFactorizer :: Cod f ~ ~> => ColimitUniversal f -> forall n. Cocone f n -> Colimit f ~> nSource

For any other co-cone of `f` with vertex `n` there exists a unique morphism from the colimit of `f` to `n`.

# Limits of a certain type

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

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

Methods

limitUniv :: Obj (Nat j ~>) f -> LimitUniversal fSource

Instances

 HasTerminalObject ~> => HasLimits Void ~> HasBinaryProducts ~> => HasLimits Pair ~>

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

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

Methods

colimitUniv :: Obj (Nat j ~>) f -> ColimitUniversal fSource

Instances

 HasInitialObject ~> => HasColimits Void ~> HasBinaryCoproducts ~> => HasColimits Pair ~>

## As a functor

data LimitFunctor whereSource

If every diagram of type `j` has a limit in `(~>)` there exists a limit functor.

Applied to a natural transformation it is a generalisation of `(***)`:

`l` `***` `r =` `LimitFunctor` `%` `arrowPair` `l r`

Constructors

 LimitFunctor :: HasLimits j ~> => LimitFunctor j ~>

Instances

 Functor (LimitFunctor j ~>)

data ColimitFunctor whereSource

If every diagram of type `j` has a colimit in `(~>)` there exists a colimit functor.

Applied to a natural transformation it is a generalisation of `(+++)`:

`l` `+++` `r =` `ColimitFunctor` `%` `arrowPair` `l r`

Constructors

 ColimitFunctor :: HasColimits j ~> => ColimitFunctor j ~>

Instances

 Functor (ColimitFunctor j ~>)

## Limits of type Void

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

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

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. Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f))

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

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

Associated Types

type InitialObject (~>) :: *Source

Instances

 HasInitialObject (->) HasInitialObject Cat HasInitialObject Boolean False is the initial object in the Boolean category. HasInitialObject Omega HasInitialObject (Peano (->)) Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) HasInitialObject (Dialg (NatF (->)) (DiagProd (->)))

data Zero Source

Any empty data type is an initial object in Hask.

## Limits of type Pair

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

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

The product of 2 objects is the limit of the functor from Pair to (~>).

Methods

product :: Obj ~> x -> Obj ~> y -> Obj ~> (BinaryProduct ~> x y)Source

proj :: Obj ~> x -> Obj ~> y -> (BinaryProduct ~> x y ~> x, BinaryProduct ~> x y ~> y)Source

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

(***) :: (a1 ~> b1) -> (a2 ~> b2) -> BinaryProduct ~> a1 a2 ~> BinaryProduct ~> b1 b2Source

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

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

The coproduct of 2 objects is the colimit of the functor from Pair to (~>).

Methods

coproduct :: Obj ~> x -> Obj ~> y -> Obj ~> (BinaryCoproduct ~> x y)Source

inj :: Obj ~> x -> Obj ~> y -> (x ~> BinaryCoproduct ~> x y, y ~> BinaryCoproduct ~> x y)Source

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

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

Instances

 HasBinaryCoproducts (->) HasBinaryCoproducts Boolean HasBinaryCoproducts Omega