Portability  nonportable 

Stability  experimental 
Maintainer  sjoerd@w3future.com 
 data Diag where
 type DiagF f = Diag (Dom f) (Cod f)
 type Cone f n = Nat (Dom f) (Cod f) (ConstF f n) f
 type Cocone f n = Nat (Dom f) (Cod f) f (ConstF f n)
 coneVertex :: Cone f n > Obj (Cod f) n
 coconeVertex :: Cocone f n > Obj (Cod f) n
 type family LimitFam j (~>) f :: *
 type Limit f = LimitFam (Dom f) (Cod f) f
 class (Category j, Category ~>) => HasLimits j (~>) where
 data LimitFunctor j (~>) = LimitFunctor
 limitAdj :: HasLimits j ~> => Adjunction (Nat j ~>) ~> (Diag j ~>) (LimitFunctor j ~>)
 type family ColimitFam j (~>) f :: *
 type Colimit f = ColimitFam (Dom f) (Cod f) f
 class (Category j, Category ~>) => HasColimits j (~>) where
 data ColimitFunctor j (~>) = ColimitFunctor
 colimitAdj :: HasColimits j ~> => Adjunction ~> (Nat j ~>) (ColimitFunctor j ~>) (Diag j ~>)
 class Category ~> => HasTerminalObject (~>) where
 type TerminalObject (~>) :: *
 terminalObject :: Obj ~> (TerminalObject ~>)
 terminate :: Obj ~> a > a ~> TerminalObject ~>
 class Category ~> => HasInitialObject (~>) where
 type InitialObject (~>) :: *
 initialObject :: Obj ~> (InitialObject ~>)
 initialize :: Obj ~> a > InitialObject ~> ~> a
 data Zero
 type family BinaryProduct (~>) x y :: *
 class Category ~> => HasBinaryProducts (~>) where
 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
 data ProductFunctor (~>) = ProductFunctor
 data p :*: q where
 type family BinaryCoproduct (~>) x y :: *
 class Category ~> => HasBinaryCoproducts (~>) where
 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
 data CoproductFunctor (~>) = CoproductFunctor
 data p :+: q where
Preliminairies
Diagonal Functor
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 cocone 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 cocone.
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 (~>)
.
class (Category j, Category ~>) => HasLimits j (~>) whereSource
An instance of HasLimits j (~>)
says that (~>)
has all limits of type j
.
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.
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 
data LimitFunctor j (~>) Source
HasLimits j ~> => Functor (LimitFunctor j ~>)  If every diagram of type 
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
.
colimit :: Obj (Nat j ~>) f > Cocone f (Colimit f)Source
colimit
returns the limiting cocone for a functor f
.
colimitFactorizer :: Obj (Nat j ~>) f > forall n. Cocone f n > Colimit f ~> nSource
colimitFactorizer
shows that the limiting cocone is universal i.e. any other cocone of f
factors through it
by returning the morphism between the vertices of the cones.
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 
data ColimitFunctor j (~>) Source
HasColimits j ~> => Functor (ColimitFunctor j ~>)  If every diagram of type 
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
type TerminalObject (~>) :: *Source
terminalObject :: Obj ~> (TerminalObject ~>)Source
terminate :: Obj ~> a > a ~> TerminalObject ~>Source
HasTerminalObject (>) 

HasTerminalObject Cat 

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
type InitialObject (~>) :: *Source
initialObject :: Obj ~> (InitialObject ~>)Source
initialize :: Obj ~> a > InitialObject ~> ~> aSource
HasInitialObject (>)  Any empty data type is an initial object in 
HasInitialObject Cat  The empty category is the initial object in 
HasInitialObject Boolean  False is the initial object in the Boolean category. 
HasInitialObject Omega 

HasInitialObject (Peano (>))  The natural numbers are the initial object for the 
(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 (Tuple1 (>) (>) ()) (DiagProd (>)))  The category for defining the natural numbers and primitive recursion can be described as

Limits of type Pair
type family BinaryProduct (~>) x y :: *Source
class Category ~> => HasBinaryProducts (~>) whereSource
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
HasBinaryProducts (>)  The tuple is the binary product in 
HasBinaryProducts Cat  The product of categories '(:**:)' is the binary product in 
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
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. 
type family BinaryCoproduct (~>) x y :: *Source
class Category ~> => HasBinaryCoproducts (~>) whereSource
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
HasBinaryCoproducts (>) 

HasBinaryCoproducts Cat  The coproduct of categories '(:++:)' is the binary coproduct in 
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
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. 