Defining semi-simplicial types in type theory faces identity proof challenges

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

Logic in Computer Science

Summary

This paper discusses attempts to define a mathematical structure called semi-simplicial types within a type theory framework used in computer science and logic. The authors try to build these types using a small syntax and then interpret them into meaningful mathematical objects. However, they find that to make their approach work smoothly, they need a property called uniqueness of identity proofs (UIP), which is not always available. They also explore ways to handle this problem but show that the issue persists either in the syntax or in the interpretation. They provide a formal development and mention plans to explore alternative interpretations that avoid UIP.

What this means in practice

A theory result. No direct application yet.

Authors

Thorsten Altenkirch

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.
View PDFOpen arXiv