Peter LeFanu Lumsdaine: Semi-simplicial sets, with an eye to type theory

Simplicial sets give, classically, a wonderful model for homotopy theory, and a very satisfying interpretation of type theory. In constructive settings, however, this theory breaks down in several ways. One candidate for repairing it is to pass to *semi-simplicial sets* — structures like simplicial sets, but with only face operations, not degeneracies. These are in some ways harder to work with than simplicial sets, but constructively, they seem much better-behaved.

I will show how to construct (classically) a right semi-model structure on semi-simplicial sets, and a resulting model of type theory; and I will discuss the issues involved in attempting to constructivise these results.