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.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s