Data.Category.Limit

Prelimiairies

Diagonal Functor

data Diag where

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)

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

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

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 f

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

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

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

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

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

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

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

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 f

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

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

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

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

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

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

Methods

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

Instances

HasTerminalObject ~> => HasLimits Void ~>

HasBinaryProducts ~> => HasLimits Pair ~>

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

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

Methods

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

Instances

HasInitialObject ~> => HasColimits Void ~>

HasBinaryCoproducts ~> => HasColimits Pair ~>

As a functor

data LimitFunctor where

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 where

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

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

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.

Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f))

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

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

Associated Types

type InitialObject (~>) :: *

Methods

initialObject :: Obj ~> (InitialObject ~>)

initialize :: Obj ~> a -> InitialObject ~> ~> a

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

Any empty data type is an initial object in Hask.

Limits of type Pair

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

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

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

Methods

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

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

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

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

Instances

HasBinaryProducts (->)

HasBinaryProducts Cat

HasBinaryProducts Boolean

HasBinaryProducts Omega

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

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

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

Methods

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

inj :: Obj ~> x -> Obj ~> y -> (x ~> BinaryCoproduct ~> x 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 (->)

HasBinaryCoproducts Boolean

HasBinaryCoproducts Omega

Limits of type Hask

newtype ForAll f

Constructors

ForAll

Fields

unForAll :: forall a. f a

endoHaskLimit :: Functor f => LimitUniversal (EndoHask f)

data Exists f

Constructors

forall a . Exists (f a)

endoHaskColimit :: Functor f => ColimitUniversal (EndoHask f)