Copyright | Guillaume Sabbagh 2021 |
---|---|
License | GPL-3 |
Maintainer | guillaumesabbagh@protonmail.com |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
A comma category is a category where objects are morphisms of another category C and morphisms are commutative squares in C.
For example, see Examples.ExampleCommaCategory.*
Synopsis
- data CommaObject o1 o2 m3 = CommaObject {}
- data CommaMorphism o1 o2 m1 m2 m3 = CommaMorphism {
- srcCM :: CommaObject o1 o2 m3
- tgtCM :: CommaObject o1 o2 m3
- indexAr1 :: m1
- indexAr2 :: m2
- data CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 = CommaCategory {}
- mkSliceCategory :: (FiniteCategory c m o, Morphism m o, Eq o) => c -> o -> Maybe (CommaCategory c m o One One One c m o)
- mkCosliceCategory :: (FiniteCategory c m o, Morphism m o, Eq o) => c -> o -> Maybe (CommaCategory One One One c m o c m o)
- mkArrowCategory :: (FiniteCategory c m o, Morphism m o, Eq o) => c -> CommaCategory c m o c m o c m o
Documentation
data CommaObject o1 o2 m3 Source #
A CommaObject
in the CommaCategory
(T|S) is a triplet <e,d,f> where f : T(e) -> S(d)
.
See Categories for the working mathematician, Saunders Mac Lane, P.46.
Instances
(Eq o1, Eq o2, Eq m3) => Eq (CommaObject o1 o2 m3) Source # | |
Defined in CommaCategory.CommaCategory (==) :: CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> Bool (/=) :: CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> Bool | |
(Show o1, Show o2, Show m3) => Show (CommaObject o1 o2 m3) Source # | |
Defined in CommaCategory.CommaCategory showsPrec :: Int -> CommaObject o1 o2 m3 -> ShowS show :: CommaObject o1 o2 m3 -> String showList :: [CommaObject o1 o2 m3] -> ShowS | |
(PrettyPrintable o1, PrettyPrintable o2, PrettyPrintable m3) => PrettyPrintable (CommaObject o1 o2 m3) Source # | |
Defined in CommaCategory.CommaCategory pprint :: CommaObject o1 o2 m3 -> String Source # | |
(Morphism m1 o1, Morphism m2 o2, Eq o1, Eq o2, Eq m3) => Morphism (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) Source # | |
Defined in CommaCategory.CommaCategory (@) :: CommaMorphism o1 o2 m1 m2 m3 -> CommaMorphism o1 o2 m1 m2 m3 -> CommaMorphism o1 o2 m1 m2 m3 Source # source :: CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3 Source # target :: CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3 Source # | |
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m3) => GeneratedFiniteCategory (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) Source # | |
Defined in CommaCategory.CommaCategory genAr :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # decompose :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaMorphism o1 o2 m1 m2 m3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # genArrows :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # | |
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m3) => FiniteCategory (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) Source # | |
Defined in CommaCategory.CommaCategory ob :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> [CommaObject o1 o2 m3] Source # identity :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaObject o1 o2 m3 -> CommaMorphism o1 o2 m1 m2 m3 Source # ar :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # arrows :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # |
data CommaMorphism o1 o2 m1 m2 m3 Source #
A CommaMorphism
in the CommaCategory
(T|S) is a couple <k,h>.
See Categories for the working mathematician, Saunders Mac Lane, P.46.
CommaMorphism | |
|
Instances
(Eq o1, Eq o2, Eq m3, Eq m1, Eq m2) => Eq (CommaMorphism o1 o2 m1 m2 m3) Source # | |
Defined in CommaCategory.CommaCategory (==) :: CommaMorphism o1 o2 m1 m2 m3 -> CommaMorphism o1 o2 m1 m2 m3 -> Bool (/=) :: CommaMorphism o1 o2 m1 m2 m3 -> CommaMorphism o1 o2 m1 m2 m3 -> Bool | |
(Show o1, Show o2, Show m3, Show m1, Show m2) => Show (CommaMorphism o1 o2 m1 m2 m3) Source # | |
Defined in CommaCategory.CommaCategory showsPrec :: Int -> CommaMorphism o1 o2 m1 m2 m3 -> ShowS show :: CommaMorphism o1 o2 m1 m2 m3 -> String showList :: [CommaMorphism o1 o2 m1 m2 m3] -> ShowS | |
(PrettyPrintable m1, PrettyPrintable m2) => PrettyPrintable (CommaMorphism o1 o2 m1 m2 m3) Source # | |
Defined in CommaCategory.CommaCategory pprint :: CommaMorphism o1 o2 m1 m2 m3 -> String Source # | |
(Morphism m1 o1, Morphism m2 o2, Eq o1, Eq o2, Eq m3) => Morphism (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) Source # | |
Defined in CommaCategory.CommaCategory (@) :: CommaMorphism o1 o2 m1 m2 m3 -> CommaMorphism o1 o2 m1 m2 m3 -> CommaMorphism o1 o2 m1 m2 m3 Source # source :: CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3 Source # target :: CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3 Source # | |
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m3) => GeneratedFiniteCategory (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) Source # | |
Defined in CommaCategory.CommaCategory genAr :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # decompose :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaMorphism o1 o2 m1 m2 m3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # genArrows :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # | |
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m3) => FiniteCategory (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) Source # | |
Defined in CommaCategory.CommaCategory ob :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> [CommaObject o1 o2 m3] Source # identity :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaObject o1 o2 m3 -> CommaMorphism o1 o2 m1 m2 m3 Source # ar :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # arrows :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # |
data CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 Source #
A CommaCategory
is a couple (T|S) with T and S two diagrams with the same target.
See Categories for the working mathematician, Saunders Mac Lane, P.46.
Instances
(Eq c1, Eq c3, Eq o1, Eq o3, Eq m1, Eq m3, Eq c2, Eq o2, Eq m2) => Eq (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) Source # | |
Defined in CommaCategory.CommaCategory (==) :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool (/=) :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool | |
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2, Show o2, Show m2) => Show (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) Source # | |
Defined in CommaCategory.CommaCategory showsPrec :: Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS show :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String showList :: [CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS | |
(PrettyPrintable c1, PrettyPrintable m1, PrettyPrintable o1, PrettyPrintable c2, PrettyPrintable m2, PrettyPrintable o2, PrettyPrintable c3, PrettyPrintable m3, PrettyPrintable o3, FiniteCategory c1 m1 o1, FiniteCategory c2 m2 o2, FiniteCategory c3 m3 o3, Morphism m1 o1, Morphism m2 o2, Morphism m3 o3, Eq m1, Eq o1, Eq m2, Eq o2) => PrettyPrintable (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) Source # | |
Defined in CommaCategory.CommaCategory pprint :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String Source # | |
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m3) => GeneratedFiniteCategory (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) Source # | |
Defined in CommaCategory.CommaCategory genAr :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # decompose :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaMorphism o1 o2 m1 m2 m3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # genArrows :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # | |
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m3) => FiniteCategory (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) Source # | |
Defined in CommaCategory.CommaCategory ob :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> [CommaObject o1 o2 m3] Source # identity :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaObject o1 o2 m3 -> CommaMorphism o1 o2 m1 m2 m3 Source # ar :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # arrows :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> [CommaMorphism o1 o2 m1 m2 m3] Source # |
mkSliceCategory :: (FiniteCategory c m o, Morphism m o, Eq o) => c -> o -> Maybe (CommaCategory c m o One One One c m o) Source #
Constructs the slice category of a category C over an object o.
Returns Nothing if the object is not in the category.
mkCosliceCategory :: (FiniteCategory c m o, Morphism m o, Eq o) => c -> o -> Maybe (CommaCategory One One One c m o c m o) Source #
Constructs the coslice category of a category C under an object o.
Returns Nothing if the object is not in the category.
mkArrowCategory :: (FiniteCategory c m o, Morphism m o, Eq o) => c -> CommaCategory c m o c m o c m o Source #
Constructs the arrow category of a category C.