Displayed Type Theory and Semisimplicial Types

Prerequisites. Direct starred prerequisites: Chapter 60, Chapter 209. No later core chapter depends on this route.

Opening obstruction

The type of all semisimplicial types cannot be defined by an ordinary finite indexed family, because each dimension depends on an unbounded tower of lower-dimensional boundaries.

Development contract

Develop the discrete/simplicial modes and displayed dependency, construct displayed coinductive semisimplicial types and their Reedy-fibrant semantics, and calculate one finite skeleton. Compare displayed dependency rule-for-rule with the span-parametric calculus of chapter 60. No normalization or canonicity theorem is proved for this calculus.