Portability | non-portable |
---|---|
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
- type LimitUniversal f = TerminalUniversal f (DiagF f) (Limit f)
- limitUniversal :: Cod f ~ ~> => Cone f (Limit f) -> (forall n. Cone f n -> n ~> Limit f) -> LimitUniversal f
- limit :: LimitUniversal f -> Cone f (Limit f)
- limitFactorizer :: Cod f ~ ~> => LimitUniversal f -> forall n. Cone f n -> n ~> Limit f
- type family ColimitFam j (~>) f :: *
- type Colimit f = ColimitFam (Dom f) (Cod f) f
- type ColimitUniversal f = InitialUniversal f (DiagF f) (Colimit f)
- colimitUniversal :: Cod f ~ ~> => Cocone f (Colimit f) -> (forall n. Cocone f n -> Colimit f ~> n) -> ColimitUniversal f
- colimit :: ColimitUniversal f -> Cocone f (Colimit f)
- colimitFactorizer :: Cod f ~ ~> => ColimitUniversal f -> forall n. Cocone f n -> Colimit f ~> n
- class (Category j, Category ~>) => HasLimits j (~>) where
- limitUniv :: Obj (Nat j ~>) f -> LimitUniversal f
- class (Category j, Category ~>) => HasColimits j (~>) where
- colimitUniv :: Obj (Nat j ~>) f -> ColimitUniversal f
- data LimitFunctor where
- LimitFunctor :: HasLimits j ~> => LimitFunctor j ~>
- data ColimitFunctor where
- ColimitFunctor :: HasColimits j ~> => ColimitFunctor 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
- newtype ForAll f = ForAll {
- unForAll :: forall a. f a
- endoHaskLimit :: Functor f => LimitUniversal (EndoHask f)
- data Exists f = forall a . Exists (f a)
- endoHaskColimit :: Functor f => ColimitUniversal (EndoHask f)
Preliminairies
Diagonal Functor
The diagonal functor from (index-) category J to (~>).
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 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
.
limitUniv :: Obj (Nat j ~>) f -> LimitUniversal fSource
HasBinaryProducts ~> => HasLimits Pair ~> | |
HasTerminalObject ~> => HasLimits Void ~> |
class (Category j, Category ~>) => HasColimits j (~>) whereSource
An instance of HasColimits j (~>)
says that (~>)
has all colimits of type j
.
colimitUniv :: Obj (Nat j ~>) f -> ColimitUniversal fSource
HasBinaryCoproducts ~> => HasColimits Pair ~> | |
HasInitialObject ~> => HasColimits Void ~> |
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
LimitFunctor :: HasLimits j ~> => LimitFunctor j ~> |
(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
ColimitFunctor :: HasColimits j ~> => ColimitFunctor j ~> |
(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 (~>).
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. |
(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 (~>).
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 (->)) | |
(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 (~>).
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 (->) | |
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.
HasBinaryProducts ~> => Functor (ProductFunctor ~>) | |
(HasTerminalObject ~>, HasBinaryProducts ~>) => TensorProduct (ProductFunctor ~>) | |
(HasTerminalObject ~>, HasBinaryProducts ~>) => HasUnit (ProductFunctor ~>) |
The product of two functors.
type family BinaryCoproduct (~>) x y :: *Source
class Category ~> => HasBinaryCoproducts (~>) whereSource
The coproduct of 2 objects is the colimit of the functor from Pair to (~>).
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 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.
HasBinaryCoproducts ~> => Functor (CoproductFunctor ~>) | |
(HasInitialObject ~>, HasBinaryCoproducts ~>) => TensorProduct (CoproductFunctor ~>) | |
(HasInitialObject ~>, HasBinaryCoproducts ~>) => HasUnit (CoproductFunctor ~>) |
The coproduct of two functors.
Limits of type Hask
endoHaskLimit :: Functor f => LimitUniversal (EndoHask f)Source
endoHaskColimit :: Functor f => ColimitUniversal (EndoHask f)Source