Portability  nonportable 

Stability  experimental 
Maintainer  sjoerd@w3future.com 
Safe Haskell  SafeInferred 
 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 k f :: *
 type Limit f = LimitFam (Dom f) (Cod f) f
 class (Category j, Category k) => HasLimits j k where
 data LimitFunctor j k = LimitFunctor
 limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
 type family ColimitFam j k f :: *
 type Colimit f = ColimitFam (Dom f) (Cod f) f
 class (Category j, Category k) => HasColimits j k where
 data ColimitFunctor j k = ColimitFunctor
 colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
 class Category k => HasTerminalObject k where
 type TerminalObject k :: *
 terminalObject :: Obj k (TerminalObject k)
 terminate :: Obj k a > k a (TerminalObject k)
 class Category k => HasInitialObject k where
 type InitialObject k :: *
 initialObject :: Obj k (InitialObject k)
 initialize :: Obj k a > k (InitialObject k) a
 data Zero
 class Category k => HasBinaryProducts k where
 type BinaryProduct k x y :: *
 proj1 :: Obj k x > Obj k y > k (BinaryProduct k x y) x
 proj2 :: Obj k x > Obj k y > k (BinaryProduct k x y) y
 (&&&) :: k a x > k a y > k a (BinaryProduct k x y)
 (***) :: k a1 b1 > k a2 b2 > k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
 data ProductFunctor k = ProductFunctor
 data p :*: q where
 prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
 class Category k => HasBinaryCoproducts k where
 type BinaryCoproduct k x y :: *
 inj1 :: Obj k x > Obj k y > k x (BinaryCoproduct k x y)
 inj2 :: Obj k x > Obj k y > k y (BinaryCoproduct k x y)
 () :: k x a > k y a > k (BinaryCoproduct k x y) a
 (+++) :: k a1 b1 > k a2 b2 > k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
 data CoproductFunctor k = CoproductFunctor
 data p :+: q where
 coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)
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 k f :: *Source
Limits in a category k
by means of a diagram of type j
, which is a functor from j
to k
.
class (Category j, Category k) => HasLimits j k whereSource
An instance of HasLimits j k
says that k
has all limits of type j
.
limit :: Obj (Nat j k) f > Cone f (Limit f)Source
limit
returns the limiting cone for a functor f
.
limitFactorizer :: Obj (Nat j k) f > forall n. Cone f n > k n (Limit f)Source
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.
Category k => HasLimits Unit k  The limit of a single object is that object. 
HasTerminalObject k => HasLimits Void k  A terminal object is the limit of the functor from 0 to k. 
(HasInitialObject (:>>: i j), Category k) => HasLimits (:>>: i j) k  The limit of any diagram with an initial object, has the limit at the initial object. 
(HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (:++: i j) k  If 
data LimitFunctor j k Source
HasLimits j k => Functor (LimitFunctor j k)  If every diagram of type 
limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)Source
The limit functor is right adjoint to the diagonal functor.
Colimits
type family ColimitFam j k f :: *Source
Colimits in a category k
by means of a diagram of type j
, which is a functor from j
to k
.
type Colimit f = ColimitFam (Dom f) (Cod f) fSource
class (Category j, Category k) => HasColimits j k whereSource
An instance of HasColimits j k
says that k
has all colimits of type j
.
colimit :: Obj (Nat j k) f > Cocone f (Colimit f)Source
colimit
returns the limiting cocone for a functor f
.
colimitFactorizer :: Obj (Nat j k) f > forall n. Cocone f n > k (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.
Category k => HasColimits Unit k  The colimit of a single object is that object. 
HasInitialObject k => HasColimits Void k  An initial object is the colimit of the functor from 0 to k. 
(HasTerminalObject (:>>: i j), Category k) => HasColimits (:>>: i j) k  The colimit of any diagram with a terminal object, has the limit at the terminal object. 
(HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (:++: i j) k  If 
data ColimitFunctor j k Source
HasColimits j k => Functor (ColimitFunctor j k)  If every diagram of type 
colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)Source
The colimit functor is left adjoint to the diagonal functor.
Limits of type Void
class Category k => HasTerminalObject k whereSource
type TerminalObject k :: *Source
terminalObject :: Obj k (TerminalObject k)Source
terminate :: Obj k a > k a (TerminalObject k)Source
HasTerminalObject (>) 

HasTerminalObject Cat 

HasTerminalObject Unit  The category of one object has that object as terminal object. 
HasTerminalObject Boolean  True is the terminal object in the Boolean category. 
HasTerminalObject Simplex  The ordinal 
HasInitialObject k => HasTerminalObject (Op k)  Terminal objects are the dual of initial objects. 
HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f) 

(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. 
(Category c1, HasTerminalObject c2) => HasTerminalObject (:>>: c1 c2)  The terminal object of the direct coproduct of categories is the terminal object of the terminal category. 
class Category k => HasInitialObject k whereSource
type InitialObject k :: *Source
initialObject :: Obj k (InitialObject k)Source
initialize :: Obj k a > k (InitialObject k) aSource
HasInitialObject (>)  Any empty data type is an initial object in 
HasInitialObject Cat  The empty category is the initial object in 
HasInitialObject Unit  The category of one object has that object as initial object. 
HasInitialObject Boolean  False is the initial object in the Boolean category. 
HasInitialObject Simplex  The ordinal 
HasTerminalObject k => HasInitialObject (Op k)  Terminal objects are the dual of initial objects. 
HasInitialObject (f (Fix f)) => HasInitialObject (Fix f) 

(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. 
(HasInitialObject c1, Category c2) => HasInitialObject (:>>: c1 c2)  The initial object of the direct coproduct of categories is the initial object of the initial category. 
HasInitialObject (Dialg (Tuple1 (>) (>) ()) (DiagProd (>)))  The category for defining the natural numbers and primitive recursion can be described as

Limits of type Pair
class Category k => HasBinaryProducts k whereSource
type BinaryProduct k x y :: *Source
proj1 :: Obj k x > Obj k y > k (BinaryProduct k x y) xSource
proj2 :: Obj k x > Obj k y > k (BinaryProduct k x y) ySource
(&&&) :: k a x > k a y > k a (BinaryProduct k x y)Source
(***) :: k a1 b1 > k a2 b2 > k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)Source
HasBinaryProducts (>)  The tuple is the binary product in 
HasBinaryProducts Cat  The product of categories 
HasBinaryProducts Unit  In the category of one object that object is its own product. 
HasBinaryProducts Boolean  Conjunction is the binary product in the Boolean category. 
HasBinaryCoproducts k => HasBinaryProducts (Op k)  Binary products are the dual of binary coproducts. 
HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) 

(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 
(HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (:>>: c1 c2) 
data ProductFunctor k Source
HasBinaryProducts k => Functor (ProductFunctor k)  Binary product as a bifunctor. 
(HasTerminalObject k, HasBinaryProducts k) => TensorProduct (ProductFunctor k)  If a category has all products, then the product functor makes it a monoidal category, with the terminal object as unit. 
prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)Source
A specialisation of the limit adjunction to products.
class Category k => HasBinaryCoproducts k whereSource
type BinaryCoproduct k x y :: *Source
inj1 :: Obj k x > Obj k y > k x (BinaryCoproduct k x y)Source
inj2 :: Obj k x > Obj k y > k y (BinaryCoproduct k x y)Source
() :: k x a > k y a > k (BinaryCoproduct k x y) aSource
(+++) :: k a1 b1 > k a2 b2 > k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)Source
HasBinaryCoproducts Cat  The coproduct of categories 
HasBinaryCoproducts Unit  In the category of one object that object is its own coproduct. 
HasBinaryCoproducts Boolean  Disjunction is the binary coproduct in the Boolean category. 
HasBinaryProducts k => HasBinaryCoproducts (Op k)  Binary products are the dual of binary coproducts. 
HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) 

(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 
(HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (:>>: c1 c2) 
data CoproductFunctor k Source
HasBinaryCoproducts k => Functor (CoproductFunctor k)  Binary coproduct as a bifunctor. 
(HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k)  If a category has all coproducts, then the coproduct functor makes it a monoidal category, with the initial object as unit. 
coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)Source
A specialisation of the colimit adjunction to coproducts.