ConeCategory.LeftCone

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.

Cone related functions and types.

data LeftCone c m o

The left cone category associated to a category.

Constructors

LeftCone c

Instances

Eq c => Eq (LeftCone c m o)

Defined in ConeCategory.LeftCone

Methods

(==) :: LeftCone c m o -> LeftCone c m o -> Bool

(/=) :: LeftCone c m o -> LeftCone c m o -> Bool

Show c => Show (LeftCone c m o)

Defined in ConeCategory.LeftCone

Methods

showsPrec :: Int -> LeftCone c m o -> ShowS

show :: LeftCone c m o -> String

showList :: [LeftCone c m o] -> ShowS

PrettyPrintable c => PrettyPrintable (LeftCone c m o)

Defined in ConeCategory.LeftCone

Methods

pprint :: LeftCone c m o -> String

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)

Inclusion functor from a category to its left cone category.

data ConeCategory c1 m1 o1 c2 m2 o2

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)

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)

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