Copyright	Guillaume Sabbagh 2022
License	GPL-3
Maintainer	guillaumesabbagh@protonmail.com
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Math.CompleteCategory

Contents

Limit type
Helper typeclasses to define a CompleteCategory
CompleteCategory

Description

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

data Limit oIndex t Source #

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).

Constructors

Projection t	A `Projection` is the parameter type of the original category to project the limits back to them.
ProductElement (Map oIndex t)	A `ProductElement` is a mapping from the indexing objects to objects of type t.

Instances

Instances details

(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 #
Instance details Defined in Math.Categories.FinSet Methods 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 #
Instance details Defined in Math.Categories.FinSet Methods 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 #
Instance details Defined in Math.Categories.FinSet Methods internalHom :: TwoBase (FinSet a) (Function a) (Set a) -> Tripod (FinSet (Cartesian a)) (Function (Cartesian a)) (Set (Cartesian a)) Source #
(PrettyPrint oIndex, PrettyPrint t, Eq oIndex) => PrettyPrint (Limit oIndex t) Source #
Instance details Defined in Math.CompleteCategory Methods pprint :: Int -> Limit oIndex t -> String Source # pprintWithIndentations :: Int -> Int -> String -> Limit oIndex t -> String Source # pprintIndent :: Int -> Limit oIndex t -> String Source #
(Simplifiable t, Simplifiable oIndex, Eq oIndex) => Simplifiable (Limit oIndex t) Source #
Instance details Defined in Math.CompleteCategory Methods simplify :: Limit oIndex t -> Limit oIndex t #
Generic (Limit oIndex t) Source #
Instance details Defined in Math.CompleteCategory Associated Types type Rep (Limit oIndex t) :: Type -> Type Methods from :: Limit oIndex t -> Rep (Limit oIndex t) x to :: Rep (Limit oIndex t) x -> Limit oIndex t
(Show t, Show oIndex) => Show (Limit oIndex t) Source #
Instance details Defined in Math.CompleteCategory Methods showsPrec :: Int -> Limit oIndex t -> ShowS show :: Limit oIndex t -> String showList :: [Limit oIndex t] -> ShowS
(Eq t, Eq oIndex) => Eq (Limit oIndex t) Source #
Instance details Defined in Math.CompleteCategory Methods (==) :: Limit oIndex t -> Limit oIndex t -> Bool (/=) :: Limit oIndex t -> Limit oIndex t -> Bool
(Morphism m o, Eq m, Eq oIndex) => Morphism (Limit oIndex m) (Limit oIndex o) Source #
Instance details Defined in Math.FiniteCategories.LimitCategory Methods (@) :: Limit oIndex m -> Limit oIndex m -> Limit oIndex m Source # (@?) :: Limit oIndex m -> Limit oIndex m -> Maybe (Limit oIndex m) Source # source :: Limit oIndex m -> Limit oIndex o Source # target :: 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 #
Instance details Defined in Math.Categories.FinGrph Methods 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 #
Instance details Defined in Math.Categories.FinGrph Methods 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 #
Instance details Defined in Math.FiniteCategories.LimitCategory Methods 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 #
Instance details Defined in Math.FiniteCategories.LimitCategory Methods 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 #
Instance details Defined in Math.FiniteCategories.LimitCategory Methods ob :: LimitCategory cIndex mIndex oIndex c m o -> Set (Limit oIndex o) Source #
type Rep (Limit oIndex t) Source #
Instance details Defined in Math.CompleteCategory type Rep (Limit oIndex t) = D1 ('MetaData "Limit" "Math.CompleteCategory" "FiniteCategories-0.6.4.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.

Methods

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

Instances details

(Enum a, Ord a, Eq oIndex) => HasProducts (OrdinalCategory a) (IsSmallerThan a) a (OrdinalCategory a) (IsSmallerThan a) a oIndex Source #
Instance details Defined in Math.Categories.OrdinalCategory Methods product :: Diagram (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex (OrdinalCategory a) (IsSmallerThan a) a -> Cone (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex (OrdinalCategory a) (IsSmallerThan a) a Source #
(Ord a, Eq oIndex) => HasProducts (TotalOrder a) (IsSmallerThan a) a (TotalOrder a) (IsSmallerThan a) a oIndex Source #
Instance details Defined in Math.Categories.TotalOrder Methods product :: Diagram (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex (TotalOrder a) (IsSmallerThan a) a -> Cone (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex (TotalOrder a) (IsSmallerThan a) a Source #
(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 #
Instance details Defined in Math.Categories.FinSet Methods 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 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 #
Instance details Defined in Math.Categories.FinGrph Methods 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 #

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.

Methods

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

Instances details

(Enum a, Ord a) => HasEqualizers (OrdinalCategory a) (IsSmallerThan a) a Source #
Instance details Defined in Math.Categories.OrdinalCategory Methods equalize :: Diagram Parallel ParallelAr ParallelOb (OrdinalCategory a) (IsSmallerThan a) a -> Cone Parallel ParallelAr ParallelOb (OrdinalCategory a) (IsSmallerThan a) a Source #
Ord a => HasEqualizers (TotalOrder a) (IsSmallerThan a) a Source #
Instance details Defined in Math.Categories.TotalOrder Methods equalize :: Diagram Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a -> Cone Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a Source #
Eq a => HasEqualizers (FinSet a) (Function a) (Set a) Source #
Instance details Defined in Math.Categories.FinSet Methods equalize :: Diagram Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a) -> Cone Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a) Source #
(Eq n, Eq e) => HasEqualizers (FinGrph n e) (GraphHomomorphism n e) (Graph n e) Source #
Instance details Defined in Math.Categories.FinGrph Methods equalize :: Diagram Parallel ParallelAr ParallelOb (FinGrph n e) (GraphHomomorphism n e) (Graph n e) -> Cone Parallel ParallelAr ParallelOb (FinGrph n e) (GraphHomomorphism n e) (Graph n e) Source #

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.

Methods

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 #

A partial Diagram to project objects and morphisms of a base like a call of limit would do.

(coneBase (limit diag)) should equal ((projectBase diag) <-@<- (diag))

Instances

Instances details

(Enum a, Ord a, Eq mIndex, Eq oIndex) => CompleteCategory (OrdinalCategory a) (IsSmallerThan a) a (OrdinalCategory a) (IsSmallerThan a) a cIndex mIndex oIndex Source #
Instance details Defined in Math.Categories.OrdinalCategory Methods 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 #
Instance details Defined in Math.Categories.TotalOrder Methods 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 #
Instance details Defined in Math.Categories.FinSet Methods 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 #
Instance details Defined in Math.Categories.FinGrph Methods 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 #
Instance details Defined in Math.FiniteCategories.LimitCategory Methods 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 #

A partial Diagram to unproject object and morphism of the base in a limit cone.

unprojectBase and projectBase returned Diagrams are inverses.

Limit type

Instances

Helper typeclasses to define a CompleteCategory

Instances

Instances

CompleteCategory

Instances

Helper typeclasses to define a `CompleteCategory`