Copyright | Guillaume Sabbagh 2022 |
---|---|
License | GPL-3 |
Maintainer | guillaumesabbagh@protonmail.com |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Typeclasses for Category
with special properties such as being complete.
A Category
might have products meaning that any discreteDiagram
on it has a limit.
A Category
might have equalizers meaning that any parallelDiagram
on it has a limit.
If a Category
have both products and equalizers, it is complete meaning that it has all small limits.
To compute limits in a custom FiniteCategory
, see limits
in Math.ConeCategory.
Synopsis
- data Limit oIndex t
- = Projection t
- | ProductElement (Map oIndex t)
- unproject :: Limit oIndex t -> Maybe t
- class (Category c m o, Morphism m o, Category cLim mLim oLim, Morphism mLim oLim) => HasProducts c m o cLim mLim oLim oIndex | c -> m, m -> o, cLim -> mLim, mLim -> oLim, c oIndex -> cLim where
- product :: Diagram (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex c m o -> Cone (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex cLim mLim oLim
- class (Category c m o, Morphism m o) => HasEqualizers c m o | c -> m, m -> o where
- equalize :: Diagram Parallel ParallelAr ParallelOb c m o -> Cone Parallel ParallelAr ParallelOb c m o
- limitFromProductsAndEqualizers :: (Category c m o, Morphism m o, Category cLim mLim oLim, Morphism mLim oLim, Eq cLim, Eq mLim, Eq oLim, HasProducts c m o cLim mLim oLim oIndex, HasEqualizers cLim mLim oLim, FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq oIndex, Eq mIndex, Eq cIndex) => (m -> mLim) -> Diagram cIndex mIndex oIndex c m o -> Cone cIndex mIndex oIndex cLim mLim oLim
- class (Category c m o, Morphism m o, Category cLim mLim oLim, Morphism mLim oLim) => CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex | c -> m, m -> o, cLim -> mLim, mLim -> oLim, c cIndex mIndex oIndex -> cLim where
- limit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq cIndex, Eq mIndex, Eq oIndex) => Diagram cIndex mIndex oIndex c m o -> Cone cIndex mIndex oIndex cLim mLim oLim
- projectBase :: Diagram cIndex mIndex oIndex c m o -> Diagram c m o cLim mLim oLim
- unprojectBase :: CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex => Diagram cIndex mIndex oIndex c m o -> Diagram cLim mLim oLim c m o
Limit type
For a Category
parametrized over a type t, the apex of the limit of a diagram indexed by a category parametrized over a type i will contain ProductElement
constructions (a product element is a tuple). A given tuple can be projected onto a Projection
at a given index.
For example, in FinSet
, let's consider a discrete diagram from DiscreteTwo
to (FinSet
Int) which selects {1,2} and {3,4}. The apex of the limit is obviously {(1,3),(1,4),(2,3),(2,4)}, note that it is not an object of (Finset
Int) but an object of (FinSet
(Set (Int,Int))). The Limit
type allows to construct type (FinSet
(Limit
DiscreteTwo
Int)) in which we can consider the original objects with Projection
and the new tuples with ProductElement
. Here, instead of couples, we will consider the limit to be {ProductElement (weakMap [(A,1),(B,3)]),ProductElement (weakMap [(A,1),(B,4)]),ProductElement (weakMap [(A,2),(B,3)]),ProductElement (weakMap [(A,2),(B,4)])}. We can construct projections in the same category, for example along A
, which will map ProductElement
(weakMap [(A,1),(B,3)]) to (Projection
1).
Projection t | A |
ProductElement (Map oIndex t) | A |
Instances
(Eq a, Eq oIndex) => HasProducts (FinSet a) (Function a) (Set a) (FinSet (Limit oIndex a)) (Function (Limit oIndex a)) (Set (Limit oIndex a)) oIndex Source # | |
Defined in Math.Categories.FinSet product :: Diagram (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex (FinSet a) (Function a) (Set a) -> Cone (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex (FinSet (Limit oIndex a)) (Function (Limit oIndex a)) (Set (Limit oIndex a)) Source # | |
(Eq a, Eq mIndex, Eq oIndex) => CompleteCategory (FinSet a) (Function a) (Set a) (FinSet (Limit oIndex a)) (Function (Limit oIndex a)) (Set (Limit oIndex a)) cIndex mIndex oIndex Source # | |
Defined in Math.Categories.FinSet limit :: Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a) -> Cone cIndex mIndex oIndex (FinSet (Limit oIndex a)) (Function (Limit oIndex a)) (Set (Limit oIndex a)) Source # projectBase :: Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a) -> Diagram (FinSet a) (Function a) (Set a) (FinSet (Limit oIndex a)) (Function (Limit oIndex a)) (Set (Limit oIndex a)) Source # | |
Eq a => CartesianClosedCategory (FinSet a) (Function a) (Set a) (FinSet (TwoProduct a)) (Function (TwoProduct a)) (Set (TwoProduct a)) (FinSet (Cartesian a)) (Function (Cartesian a)) (Set (Cartesian a)) Source # | |
(PrettyPrint oIndex, PrettyPrint t, Eq oIndex) => PrettyPrint (Limit oIndex t) Source # | |
Defined in Math.CompleteCategory | |
(Simplifiable t, Simplifiable oIndex, Eq oIndex) => Simplifiable (Limit oIndex t) Source # | |
Defined in Math.CompleteCategory | |
Generic (Limit oIndex t) Source # | |
(Show t, Show oIndex) => Show (Limit oIndex t) Source # | |
(Eq t, Eq oIndex) => Eq (Limit oIndex t) Source # | |
(Morphism m o, Eq m, Eq oIndex) => Morphism (Limit oIndex m) (Limit oIndex o) Source # | |
(Eq n, Eq e, Eq oIndex) => HasProducts (FinGrph n e) (GraphHomomorphism n e) (Graph n e) (FinGrph (Limit oIndex n) (Limit oIndex e)) (GraphHomomorphism (Limit oIndex n) (Limit oIndex e)) (Graph (Limit oIndex n) (Limit oIndex e)) oIndex Source # | |
Defined in Math.Categories.FinGrph product :: Diagram (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex (FinGrph n e) (GraphHomomorphism n e) (Graph n e) -> Cone (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex (FinGrph (Limit oIndex n) (Limit oIndex e)) (GraphHomomorphism (Limit oIndex n) (Limit oIndex e)) (Graph (Limit oIndex n) (Limit oIndex e)) Source # | |
(Eq n, Eq e, Eq mIndex, Eq oIndex) => CompleteCategory (FinGrph n e) (GraphHomomorphism n e) (Graph n e) (FinGrph (Limit oIndex n) (Limit oIndex e)) (GraphHomomorphism (Limit oIndex n) (Limit oIndex e)) (Graph (Limit oIndex n) (Limit oIndex e)) cIndex mIndex oIndex Source # | |
Defined in Math.Categories.FinGrph limit :: Diagram cIndex mIndex oIndex (FinGrph n e) (GraphHomomorphism n e) (Graph n e) -> Cone cIndex mIndex oIndex (FinGrph (Limit oIndex n) (Limit oIndex e)) (GraphHomomorphism (Limit oIndex n) (Limit oIndex e)) (Graph (Limit oIndex n) (Limit oIndex e)) Source # projectBase :: Diagram cIndex mIndex oIndex (FinGrph n e) (GraphHomomorphism n e) (Graph n e) -> Diagram (FinGrph n e) (GraphHomomorphism n e) (Graph n e) (FinGrph (Limit oIndex n) (Limit oIndex e)) (GraphHomomorphism (Limit oIndex n) (Limit oIndex e)) (Graph (Limit oIndex n) (Limit oIndex e)) Source # | |
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o, FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq cIndex, Eq mIndex, Eq oIndex) => CompleteCategory (FinCat c m o) (FinFunctor c m o) c (FinCat (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (FinFunctor (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (LimitCategory cIndex mIndex oIndex c m o) cIndex mIndex oIndex Source # | |
Defined in Math.FiniteCategories.LimitCategory limit :: Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c -> Cone cIndex mIndex oIndex (FinCat (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (FinFunctor (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (LimitCategory cIndex mIndex oIndex c m o) Source # projectBase :: Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c -> Diagram (FinCat c m o) (FinFunctor c m o) c (FinCat (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (FinFunctor (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (LimitCategory cIndex mIndex oIndex c m o) Source # | |
(FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq mIndex, Eq oIndex, Category c m o, Morphism m o, Eq m, Eq o) => Category (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o) Source # | |
Defined in Math.FiniteCategories.LimitCategory identity :: LimitCategory cIndex mIndex oIndex c m o -> Limit oIndex o -> Limit oIndex m Source # ar :: LimitCategory cIndex mIndex oIndex c m o -> Limit oIndex o -> Limit oIndex o -> Set (Limit oIndex m) Source # genAr :: LimitCategory cIndex mIndex oIndex c m o -> Limit oIndex o -> Limit oIndex o -> Set (Limit oIndex m) Source # decompose :: LimitCategory cIndex mIndex oIndex c m o -> Limit oIndex m -> [Limit oIndex m] Source # | |
(FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq mIndex, Eq oIndex, FiniteCategory c m o, Morphism m o, Eq m, Eq o) => FiniteCategory (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o) Source # | |
Defined in Math.FiniteCategories.LimitCategory | |
type Rep (Limit oIndex t) Source # | |
Defined in Math.CompleteCategory type Rep (Limit oIndex t) = D1 ('MetaData "Limit" "Math.CompleteCategory" "FiniteCategories-0.6.2.0-inplace" 'False) (C1 ('MetaCons "Projection" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "ProductElement" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map oIndex t)))) |
unproject :: Limit oIndex t -> Maybe t Source #
Remove the constructor Projection
from an original object t if possible.
Helper typeclasses to define a CompleteCategory
class (Category c m o, Morphism m o, Category cLim mLim oLim, Morphism mLim oLim) => HasProducts c m o cLim mLim oLim oIndex | c -> m, m -> o, cLim -> mLim, mLim -> oLim, c oIndex -> cLim where Source #
The typeclass of categories which have all products.
product :: Diagram (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex c m o -> Cone (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex cLim mLim oLim Source #
Given a discreteDiagram
selecting objects, return the product of the selected objects as a Cone
.
Instances
class (Category c m o, Morphism m o) => HasEqualizers c m o | c -> m, m -> o where Source #
The typeclass of categories which have all equalizers.
equalize :: Diagram Parallel ParallelAr ParallelOb c m o -> Cone Parallel ParallelAr ParallelOb c m o Source #
Given a parallelDiagram
selecting arrows, return the equalizer of the selected arrows as a Cone
.
Instances
limitFromProductsAndEqualizers :: (Category c m o, Morphism m o, Category cLim mLim oLim, Morphism mLim oLim, Eq cLim, Eq mLim, Eq oLim, HasProducts c m o cLim mLim oLim oIndex, HasEqualizers cLim mLim oLim, FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq oIndex, Eq mIndex, Eq cIndex) => (m -> mLim) -> Diagram cIndex mIndex oIndex c m o -> Cone cIndex mIndex oIndex cLim mLim oLim Source #
Computes efficiently limits thanks to products and equalizers. Can be used to instantiate CompleteCategory
.
The first argument is a function to transform an object of the original category into a limit object.
Most of the time, the original category takes one type parameter and the function uses Projection
, when the category does not take any type parameter it is id
.
For example, for FinSet
, the function has to transform a function {1 -> 2} to the function {Projection 1 -> Projection 2}.
CompleteCategory
class (Category c m o, Morphism m o, Category cLim mLim oLim, Morphism mLim oLim) => CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex | c -> m, m -> o, cLim -> mLim, mLim -> oLim, c cIndex mIndex oIndex -> cLim where Source #
The typeclass of categories which have all limits. cLim is the type of the new category in which we can compute limits and their projections. cIndex is the type of the indexing category of the diagrams.
limit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq cIndex, Eq mIndex, Eq oIndex) => Diagram cIndex mIndex oIndex c m o -> Cone cIndex mIndex oIndex cLim mLim oLim Source #
Return the limit of a Diagram
.
projectBase :: Diagram cIndex mIndex oIndex c m o -> Diagram c m o cLim mLim oLim Source #
Instances
(Enum a, Ord a, Eq mIndex, Eq oIndex) => CompleteCategory (OrdinalCategory a) (IsSmallerThan a) a (OrdinalCategory a) (IsSmallerThan a) a cIndex mIndex oIndex Source # | |
Defined in Math.Categories.OrdinalCategory limit :: Diagram cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a -> Cone cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a Source # projectBase :: Diagram cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a -> Diagram (OrdinalCategory a) (IsSmallerThan a) a (OrdinalCategory a) (IsSmallerThan a) a Source # | |
(Ord a, Eq mIndex, Eq oIndex) => CompleteCategory (TotalOrder a) (IsSmallerThan a) a (TotalOrder a) (IsSmallerThan a) a cIndex mIndex oIndex Source # | |
Defined in Math.Categories.TotalOrder limit :: Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a -> Cone cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a Source # projectBase :: Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a -> Diagram (TotalOrder a) (IsSmallerThan a) a (TotalOrder a) (IsSmallerThan a) a Source # | |
(Eq a, Eq mIndex, Eq oIndex) => CompleteCategory (FinSet a) (Function a) (Set a) (FinSet (Limit oIndex a)) (Function (Limit oIndex a)) (Set (Limit oIndex a)) cIndex mIndex oIndex Source # | |
Defined in Math.Categories.FinSet limit :: Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a) -> Cone cIndex mIndex oIndex (FinSet (Limit oIndex a)) (Function (Limit oIndex a)) (Set (Limit oIndex a)) Source # projectBase :: Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a) -> Diagram (FinSet a) (Function a) (Set a) (FinSet (Limit oIndex a)) (Function (Limit oIndex a)) (Set (Limit oIndex a)) Source # | |
(Eq n, Eq e, Eq mIndex, Eq oIndex) => CompleteCategory (FinGrph n e) (GraphHomomorphism n e) (Graph n e) (FinGrph (Limit oIndex n) (Limit oIndex e)) (GraphHomomorphism (Limit oIndex n) (Limit oIndex e)) (Graph (Limit oIndex n) (Limit oIndex e)) cIndex mIndex oIndex Source # | |
Defined in Math.Categories.FinGrph limit :: Diagram cIndex mIndex oIndex (FinGrph n e) (GraphHomomorphism n e) (Graph n e) -> Cone cIndex mIndex oIndex (FinGrph (Limit oIndex n) (Limit oIndex e)) (GraphHomomorphism (Limit oIndex n) (Limit oIndex e)) (Graph (Limit oIndex n) (Limit oIndex e)) Source # projectBase :: Diagram cIndex mIndex oIndex (FinGrph n e) (GraphHomomorphism n e) (Graph n e) -> Diagram (FinGrph n e) (GraphHomomorphism n e) (Graph n e) (FinGrph (Limit oIndex n) (Limit oIndex e)) (GraphHomomorphism (Limit oIndex n) (Limit oIndex e)) (Graph (Limit oIndex n) (Limit oIndex e)) Source # | |
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o, FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq cIndex, Eq mIndex, Eq oIndex) => CompleteCategory (FinCat c m o) (FinFunctor c m o) c (FinCat (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (FinFunctor (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (LimitCategory cIndex mIndex oIndex c m o) cIndex mIndex oIndex Source # | |
Defined in Math.FiniteCategories.LimitCategory limit :: Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c -> Cone cIndex mIndex oIndex (FinCat (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (FinFunctor (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (LimitCategory cIndex mIndex oIndex c m o) Source # projectBase :: Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c -> Diagram (FinCat c m o) (FinFunctor c m o) c (FinCat (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (FinFunctor (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (LimitCategory cIndex mIndex oIndex c m o) Source # |
unprojectBase :: CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex => Diagram cIndex mIndex oIndex c m o -> Diagram cLim mLim oLim c m o Source #