License | BSD-style (see the file LICENSE) |
---|---|
Maintainer | sjoerd@w3future.com |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe |
Language | Haskell2010 |
- 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)
- rightAdjointPreservesLimits :: (HasLimits j c, HasLimits j d) => Adjunction c d f g -> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t)
- rightAdjointPreservesLimitsInv :: (HasLimits j c, HasLimits j d) => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% Limit t) (Limit (g :.: t))
- 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)
- leftAdjointPreservesColimits :: (HasColimits j c, HasColimits j d) => Adjunction c d f g -> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t))
- leftAdjointPreservesColimitsInv :: (HasColimits j c, HasColimits j d) => Obj (Nat d c) f -> Obj (Nat j d) t -> c (Colimit (f :.: t)) (f :% Colimit t)
- class Category k => HasTerminalObject k where
- type TerminalObject k :: *
- class Category k => HasInitialObject k where
- type InitialObject k :: *
- data Zero
- class Category k => HasBinaryProducts k where
- type BinaryProduct (k :: * -> * -> *) x y :: *
- 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 :: *
- 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) f Source #
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.
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 where Source #
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.
HasLimits (->) (->) Source # | |
Category k => HasLimits Unit k Source # | The limit of a single object is that object. |
HasTerminalObject k => HasLimits Void k Source # | A terminal object is the limit of the functor from 0 to k. |
(HasInitialObject ((:>>:) i j), Category k) => HasLimits ((:>>:) i j) k Source # | 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 Source # | If |
data LimitFunctor j k Source #
HasLimits j k => Functor (LimitFunctor j k) Source # | If every diagram of type |
type Dom (LimitFunctor j k) Source # | |
type Cod (LimitFunctor j k) Source # | |
type (LimitFunctor j k) :% f Source # | |
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.
rightAdjointPreservesLimits :: (HasLimits j c, HasLimits j d) => Adjunction c d f g -> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t) Source #
rightAdjointPreservesLimitsInv :: (HasLimits j c, HasLimits j d) => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% Limit t) (Limit (g :.: t)) Source #
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 ColimitFam (->) (->) f Source # | |
type ColimitFam Unit k f Source # | |
type ColimitFam Void k f Source # | |
type ColimitFam ((:>>:) i j) k f Source # | |
type ColimitFam ((:++:) i j) k f Source # | |
class (Category j, Category k) => HasColimits j k where Source #
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 co-cone for a functor f
.
colimitFactorizer :: Obj (Nat j k) f -> forall n. Cocone f n -> k (Colimit f) n Source #
colimitFactorizer
shows that the limiting co-cone is universal – i.e. any other co-cone of f
factors through it
by returning the morphism between the vertices of the cones.
HasColimits (->) (->) Source # | |
Category k => HasColimits Unit k Source # | The colimit of a single object is that object. |
HasInitialObject k => HasColimits Void k Source # | An initial object is the colimit of the functor from 0 to k. |
(HasTerminalObject ((:>>:) i j), Category k) => HasColimits ((:>>:) i j) k Source # | 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 Source # | If |
data ColimitFunctor j k Source #
HasColimits j k => Functor (ColimitFunctor j k) Source # | If every diagram of type |
type Dom (ColimitFunctor j k) Source # | |
type Cod (ColimitFunctor j k) Source # | |
type (ColimitFunctor j k) :% f Source # | |
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.
leftAdjointPreservesColimits :: (HasColimits j c, HasColimits j d) => Adjunction c d f g -> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t)) Source #
leftAdjointPreservesColimitsInv :: (HasColimits j c, HasColimits j d) => Obj (Nat d c) f -> Obj (Nat j d) t -> c (Colimit (f :.: t)) (f :% Colimit t) Source #
Limits of type Void
class Category k => HasTerminalObject k where Source #
type TerminalObject k :: * Source #
terminalObject :: Obj k (TerminalObject k) Source #
terminate :: Obj k a -> k a (TerminalObject k) Source #
HasTerminalObject (->) Source # |
|
HasTerminalObject Cat Source # |
|
HasTerminalObject Unit Source # | The category of one object has that object as terminal object. |
HasTerminalObject Cube Source # | |
HasTerminalObject Simplex Source # | The ordinal |
HasTerminalObject Boolean Source # | True is the terminal object in the Boolean category. |
HasInitialObject k => HasTerminalObject (Op k) Source # | Terminal objects are the dual of initial objects. |
HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f) Source # |
|
(HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject ((:**:) c1 c2) Source # | The terminal object of the product of 2 categories is the product of their terminal objects. |
(Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) Source # | The constant functor to the terminal object is itself the terminal object in its functor category. |
(Category c1, HasTerminalObject c2) => HasTerminalObject ((:>>:) c1 c2) Source # | The terminal object of the direct coproduct of categories is the terminal object of the terminal category. |
class Category k => HasInitialObject k where Source #
type InitialObject k :: * Source #
initialObject :: Obj k (InitialObject k) Source #
initialize :: Obj k a -> k (InitialObject k) a Source #
HasInitialObject (->) Source # | Any empty data type is an initial object in |
HasInitialObject Cat Source # | The empty category is the initial object in |
HasInitialObject Unit Source # | The category of one object has that object as initial object. |
HasInitialObject Simplex Source # | The ordinal |
HasInitialObject Boolean Source # | False is the initial object in the Boolean category. |
HasTerminalObject k => HasInitialObject (Op k) Source # | Terminal objects are the dual of initial objects. |
HasInitialObject (f (Fix f)) => HasInitialObject (Fix f) Source # |
|
(HasInitialObject c1, HasInitialObject c2) => HasInitialObject ((:**:) c1 c2) Source # | The initial object of the product of 2 categories is the product of their initial objects. |
(Category c, HasInitialObject d) => HasInitialObject (Nat c d) Source # | The constant functor to the initial object is itself the initial object in its functor category. |
(HasInitialObject c1, Category c2) => HasInitialObject ((:>>:) c1 c2) Source # | The initial object of the direct coproduct of categories is the initial object of the initial category. |
HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) Source # | The category for defining the natural numbers and primitive recursion can be described as
|
Limits of type Pair
class Category k => HasBinaryProducts k where Source #
type BinaryProduct (k :: * -> * -> *) x y :: * Source #
proj1 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) x Source #
proj2 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) y Source #
(&&&) :: k a x -> k a y -> k a (BinaryProduct k x y) infixl 3 Source #
(***) :: k a1 b1 -> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2) infixl 3 Source #
HasBinaryProducts (->) Source # | The tuple is the binary product in |
HasBinaryProducts Cat Source # | The product of categories |
HasBinaryProducts Unit Source # | In the category of one object that object is its own product. |
HasBinaryProducts Boolean Source # | Conjunction is the binary product in the Boolean category. |
HasBinaryCoproducts k => HasBinaryProducts (Op k) Source # | Binary products are the dual of binary coproducts. |
HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) Source # |
|
(HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts ((:**:) c1 c2) Source # | The binary product of the product of 2 categories is the product of their binary products. |
(Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) Source # | The functor product |
(HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts ((:>>:) c1 c2) Source # | |
data ProductFunctor k Source #
HasBinaryProducts k => Functor (ProductFunctor k) Source # | Binary product as a bifunctor. |
(HasTerminalObject k, HasBinaryProducts k) => TensorProduct (ProductFunctor k) Source # | If a category has all products, then the product functor makes it a monoidal category, with the terminal object as unit. |
type Dom (ProductFunctor k) Source # | |
type Cod (ProductFunctor k) Source # | |
type Unit (ProductFunctor k) Source # | |
type (ProductFunctor k) :% (a, b) Source # | |
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 where Source #
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) a infixl 2 Source #
(+++) :: k a1 b1 -> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2) infixl 2 Source #
HasBinaryCoproducts Cat Source # | The coproduct of categories |
HasBinaryCoproducts Unit Source # | In the category of one object that object is its own coproduct. |
HasBinaryCoproducts Boolean Source # | Disjunction is the binary coproduct in the Boolean category. |
HasBinaryProducts k => HasBinaryCoproducts (Op k) Source # | Binary products are the dual of binary coproducts. |
HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) Source # |
|
(HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts ((:**:) c1 c2) Source # | The binary coproduct of the product of 2 categories is the product of their binary coproducts. |
(Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) Source # | The functor coproduct |
(HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts ((:>>:) c1 c2) Source # | |
data CoproductFunctor k Source #
HasBinaryCoproducts k => Functor (CoproductFunctor k) Source # | Binary coproduct as a bifunctor. |
(HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k) Source # | If a category has all coproducts, then the coproduct functor makes it a monoidal category, with the initial object as unit. |
type Dom (CoproductFunctor k) Source # | |
type Cod (CoproductFunctor k) Source # | |
type Unit (CoproductFunctor k) Source # | |
type (CoproductFunctor k) :% (a, b) Source # | |
coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k) Source #
A specialisation of the colimit adjunction to coproducts.