Any colour you like, as long as it's UIP: Semi-simplicial types from weakenings and thinnings

Abstract

We explain an attempt to define semi-simplicial types (SST) in homotopy type theory by first defining a small type theory whose contexts are exactly the data of semi-simplicial types, constructing $\mathrm{SST}\,n$ uniformly in that syntax, and then interpreting the syntax in the universe. The syntax can be defined without any truncation and without K, and the construction of $\mathrm{SST}\,n$ goes through. The naive interpretation does not: it transports along the semantic images of equations that hold only propositionally, and making these transports agree needs uniqueness of identity proofs (UIP) for the semantic types. Moving the problem into the syntax, by making composition a constructor of a higher inductive-inductive type (HIIT), does not remove it either: it reappears as a coherence problem in the syntax. Fording the HIIT (storing equations instead of computed indices), with conditional rules, makes the syntax provably a set. This is UIP for the syntax, obtained by encode-decode, and it does not by itself restrict the semantics; but the naive interpretation of the conditional rules again needs UIP for the semantic types. A semantics into groupoids that avoids UIP will be discussed in a separate note. The Agda development accompanying this note is in the repository https://github.com/txa/sst-new.