The simplex category #
We show that this category is equivalent to
We provide the following functions to work with these objects:
SimplexCategory.mkcreates an object of
SimplexCategoryout of a natural number. Use the notation
SimplexCategory.lengives the "length" of an object of
SimplexCategory, as a natural.
SimplexCategory.Hom.mkmakes a morphism out of a monotone map between
SimplexCategory.Hom.toOrderHomgives the underlying monotone map associated to a term of
Generating maps for the simplex category #
TODO: prove that the simplex category is equivalent to one given by the following generators and relations.
The generic case of the first simplicial identity
The second simplicial identity
The fourth simplicial identity
The fifth simplicial identity