Thoughts on Semisimplicial Types

(This post assumes prior knowledge of the problem of semisimplicial types in homotopy type theory.)

This blog post describes an attempt to implement homotopy type theory in itself, all the way from untyped syntax. It failed for the same reasons as most approaches to semisimplicial types; dependence on an infinite regress of more and more complicated conditions.

I think the focus on untyped syntax may be a red herring.

Suppose we had a reasonable typed syntax for homotopy type theory. Then, we would be able to:

• Interpret it in \(\mathrm{Type}\).
• Interpret it in the arrow category, \((A : \mathrm{Type}) \times (B : \mathrm{Type}) \times (A \to B)\).
• By internalizing the above construction, transform any interpretation into the corresponding arrow category.
• Iterate this, and take a limit.

The same applies if we could correctly define the concept of a model of HoTT, even if we couldn't construct the initial model.

The result is a coherent infinite cube of sets and functions. It's not semisimplicial types, exactly, but it has similarly complex coherence structure. And I know I've run into issues trying to implement this structure directly.