data-category-0.3.1.1: Restricted categories

Portability non-portable experimental sjoerd@w3future.com

Data.Category.Limit

Description

Synopsis

# Preliminairies

## Diagonal Functor

data Diag whereSource

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

Constructors

 Diag :: Diag j ~>

Instances

 (Category j, Category ~>) => 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 ~> (HasLimits (Discrete n) ~>, HasBinaryProducts ~>) => HasLimits (Discrete (S n)) ~>

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 ~> (HasColimits (Discrete n) ~>, HasBinaryCoproducts ~>) => HasColimits (Discrete (S n)) ~>

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

 (Category j, Category ~>) => 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

 (Category j, Category ~>) => 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. (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))

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

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

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 HasInitialObject (Peano (->)) (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 (->))) HasInitialObject (Dialg (NatF (->)) (DiagProd (->)))

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

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 (->) HasBinaryProducts Cat HasBinaryProducts Boolean HasBinaryProducts Omega (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (:**: c1 c2) (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d)

data ProductFunctor (~>) Source

Binary product as a bifunctor.

Constructors

 ProductFunctor

Instances

 HasBinaryProducts ~> => Functor (ProductFunctor ~>) (HasTerminalObject ~>, HasBinaryProducts ~>) => HasUnit (ProductFunctor ~>) (HasTerminalObject ~>, HasBinaryProducts ~>) => TensorProduct (ProductFunctor ~>)

data p :*: q whereSource

The product of two functors.

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)

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

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 (->) HasBinaryCoproducts Cat HasBinaryCoproducts Boolean HasBinaryCoproducts Omega (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (:**: c1 c2) (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d)

data CoproductFunctor (~>) Source

Binary coproduct as a bifunctor.

Constructors

 CoproductFunctor

Instances

 HasBinaryCoproducts ~> => Functor (CoproductFunctor ~>) (HasInitialObject ~>, HasBinaryCoproducts ~>) => HasUnit (CoproductFunctor ~>) (HasInitialObject ~>, HasBinaryCoproducts ~>) => TensorProduct (CoproductFunctor ~>)

data p :+: q whereSource

The coproduct of two functors.

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)

## Limits of type Hask

newtype ForAll f Source

Constructors

 ForAll FieldsunForAll :: forall a. f a

data Exists f Source

Constructors

 forall a . Exists (f a)