Shall we strictify some homotopy propositions? › Implications for Project Pterodactyl [01IC]

In the proposals above, we obtain an axiomatic way to strictify homotopy propositions; this operation does not satisfy any definitional laws beyond what is implied by definition. As a result, it is not the case that the round-trip \(P\to [P] \to P\) is definitionally equal to the identity function; in some sense, avoiding this definitional equality is precisely the thing that gets us out of the kind of trouble faced by Lean. This is the trade-off: sufficient expressivity demands a map \([P]\to P\), but this map cannot satisfy any interesting definitional equalities under pain of destroying the reliability of all other definitional properties of the language.

The second proposal is attractive to me because I can interpret it today in any Grothendieck \(\infty \)-topos model of HoTT, but I do not know how to interpret it in non-Grothendieck models (which are only just emerging now). On the other hand, the first proposal is far stronger but there is a pretty good chance that it will be shown to be conservative. That would certainly satisfy my design constraints.

What would we do with it? I think it would be good to explore a new variation on abstraction boundaries in proof assistants. In traditional systems, you can make a definition abstract, which means that it has no identity other than its name. We often do this when we have a complicated proof that we will never want to look at again, and when we know that if we ever need to identify it with some other proof of the same type, it will be better to deduce that from its type than from the specifics of the proof. It is possible in cases like this that we might prefer to use strictification as a kind of proof-irrelevant sealing, in which we not only ensure that we never can look at the proof again, but we also ensure that it will be definitionally equal to any other sealed proof.

Such a facility must be used with care. There is, however, an interesting opportunity here for improving the usability of homotopy type theory and univalent foundations without trading away literally every other advantage in return.