I recently had occasion to define the simplex category inside of type theory. For some reason, I decided to use an inductive definition of each type of simplicial operators , 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 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 . The actual reason I wanted to define was to use a different approach that pushes this problem off to the semantic side; see discussion at this post.