| Copyright | Guillaume Sabbagh 2021 |
|---|---|
| License | GPL-3 |
| Maintainer | guillaumesabbagh@protonmail.com |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
ConeCategory.LeftCone
Description
A left cone on I is I with another object called the cone point and a single morphism from the cone point to every other object of I.
See Category Theory for the Sciences (2014) David I. Spivak for more details.
An usual cone on C is then a functor from a left cone on I to C.
Synopsis
- data LeftCone c m o = LeftCone c
- inclusionFunctor :: (FiniteCategory c m o, Morphism m o) => LeftCone c m o -> Diagram c m o (LeftCone c m o) (LeftConeMorphism m o) (LeftConeObject o)
- data ConeCategory c1 m1 o1 c2 m2 o2 = ConeCategory (Diagram c1 m1 o1 c2 m2 o2)
Cone related functions and types.
The left cone category associated to a category.
Constructors
| LeftCone c |
inclusionFunctor :: (FiniteCategory c m o, Morphism m o) => LeftCone c m o -> Diagram c m o (LeftCone c m o) (LeftConeMorphism m o) (LeftConeObject o) Source #
Inclusion functor from a category to its left cone category.
data ConeCategory c1 m1 o1 c2 m2 o2 Source #
The category of cones defined according to the left cone definition.
It is less efficient than the ConeCategory implementation. This is only defined for pedagogical purposes.
Constructors
| ConeCategory (Diagram c1 m1 o1 c2 m2 o2) |
Instances
| (Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2) => Eq (ConeCategory c1 m1 o1 c2 m2 o2) Source # | |
Defined in ConeCategory.LeftCone Methods (==) :: ConeCategory c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2 -> Bool (/=) :: ConeCategory c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2 -> Bool | |
| (Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) => Show (ConeCategory c1 m1 o1 c2 m2 o2) Source # | |
Defined in ConeCategory.LeftCone Methods showsPrec :: Int -> ConeCategory c1 m1 o1 c2 m2 o2 -> ShowS show :: ConeCategory c1 m1 o1 c2 m2 o2 -> String showList :: [ConeCategory c1 m1 o1 c2 m2 o2] -> ShowS | |