## The Simplex Category

I recently had occasion to define the simplex category $\Delta$ inside of type theory. For some reason, I decided to use an inductive definition of each type of simplicial operators $[n] \to [m]$, rather than defining them as order-preserving maps of finite totally ordered sets in the more common way. I’m no longer sure that that was a good choice, but in case anyone is interested to have a look, the definition is here.

One might think that defining $\Delta$ is a first step towards defining “simplicial types”, but the big problem is how to deal with all the coherence conditions that would be required of a “coherent diagram” of types over $\Delta$. The actual reason I wanted to define $\Delta$ was to use a different approach that pushes this problem off to the semantic side; see discussion at this post.

This entry was posted in Uncategorized. Bookmark the permalink.