Add simplex category (WIP)

[ScriptRaccoon]

TODO: decide the properties

is balanced
has cofiltered limits
has connected colimits
has coreflexive equalizers
is cosifted
has cosifted limits
has directed colimits
has directed limits
is epi-regular
has filtered colimits
is locally cocartesian coclosed
is mono-regular
has pushouts
has sequential colimits
has sequential limits
has sifted colimits
has a strict terminal object
has wide pushouts

[dschepler]

It is mono-regular: it's easy to see the monos are the injective maps. And any subset of {0,...,n} is the equalizer of the two maps {0,...,n}->{0,...,n+1}, one of which is the inclusion map, and the other sends i to the smallest element of S which is >=i, or to n+1 if i is greater than all elements of S.

Using the same construction on the image, you can see the epis are the surjective maps. So, the category is also balanced.

[dschepler]

It seems clear the directed system [0] -> [1] -> [2] -> [3] -> ... of inclusion maps shouldn't have a colimit. On the other hand, it seems like a codirected system should stabilize at some point and then the value at that point would be the limit.

[dschepler]

My guess would be the inclusion map [0] -> [1] doesn't have a pushout with itself since there's nothing to specify which copy of 1 is less than the other one in the pushout.

[ScriptRaccoon]

Thanks a lot! I will have a look at this in the next days. Do you feel comfortable adding commits to this PR resp. make your own? @dschepler