I've been exploring approaches to defining semisimplicial types in a variation of HoTT (as far as I know, it's equivalent to Book HoTT). If this construction succeeded, it would be a major step towards defining a self-interpreter in HoTT (a function from a syntactic representation of HoTT terms and types, to the actual terms and types; e.g. using HoTT as a metatheory for HoTT).
The main problem in this construction is a coherence requirement (there is a family of equalities for which we must show that a certain composite is equal to a single equality with different parameters). If one tries to write down first few such equalities, it's evident that they're all refl-s. Therefore, one hopes to prove inductively that they're refls. Then, however, one gets stuck at writing down the types for these coherence equalities (refl is not an inhabitant of x = y, even though x and y reduce to the same term at every level).
This problem becomes trivial if one switches to one of:
- Extensional Type Theory
- Intensional Type Theory with Uniqueness of Identity Proofs
- Some more exotic type theory that somehow permits to "defer" typechecking (maybe by some notion of "inductive" well-typedness)
These systems are not HoTT, however. So it occurred to me, since HoTT is a normalizing theory, doesn't that imply it cannot interpret/typecheck itself?