@amy Not so fast... SProp in OTT is good. Until we know a better setting for mechanized set-truncated math, SProp is a keeper. HoTT is ofc nicer, but not everything works in pure HoTT. When we need the strict equality, I prefer to have it in SProp.
@AndrasKovacs @amy what is something that doesn't work in pure hott? or i think my question is better phrased as, what does "work" mean for you?
The motivating use cases of 2LTT are such that no one knows if they work in pure HoTT. This is a fairly strong sense of "not working" IMO.
There are other 2LTT-like setups, for example when I have non-fibrant types in a cubical TT, and I want to embed them in a fleshed-out language layer.
In my own past research, construction of inductive-inductive types is another good example for something that no on knows how to do without UIP. We had a chunky Agda formalization for "For Finitary Induction-Induction, Induction is Enough". That would have been much nicer to write in OTT. I think that this can be technically written in HoTT, in the sense that MLTT+UIP can be modeled in HoTT where we inductively define universes of sets which are themselves sets. But at point we take no advantage of univalence at all.
This is related to the "HoTT eats itself" complications; when I want to formalize some metatheory of type theories, I can't take advantage of univalence because of the strictness/coherence requirement of my notion of syntax. This happens regardless of my choice of representation of syntax or the chosen internal language for synthetic reasoning. Here I would also much prefer formalizing things in OTT instead of a model of MLTT+UIP embedded in HoTT.
(There are Tachi Uemura's infinity type theories for addressing this, but those are robustly over my head and I can't comment substantially on them.)
Even in the cases where things do work in HoTT, proof assistant users should be given the choice to trade generality of results for formalization convenience. HoTT formalizations are more general (they make sense in higher topoi), the OTT formalizations can be more convenient to write, making use of irrelevance and the powerful identity elimination.
(What we get from identity elimination in OTT: if two types are propositionally equal then they are definitionally isomorphic).
A 2LTT with OTT over HoTT would be pretty nice, and could also serve as "gateway drug" to HoTT. The cost of entry to HoTT is real and shouldn't be ignored. There are many people who work with proof assistants who don't know HoTT, and whose formalizations could immediately benefit from OTT features, but it'd require more effort to adapt them to HoTT.
@AndrasKovacs @amy What you are speaking about is basically true, but it is also not really relevant to the current discussion. We are not talking about HoTT vs. UIP: we are talking about definitional proof irrelevence vs. ITT/HoTT-style weak propositionhood. This is entirely orthogonal to the question of UIP as well as 2LTT, defining simplicial types, etc.
@jonmsterling @amy I find the usability motivations entirely valid by themselves. The tension between HProp and SProp can be mitigated by postulating that every HProp is logically equivalent to an SProp; this I conjecture to still enjoy homotopy canonicity and closed program extraction.
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.
@AndrasKovacs @amy This idea of postulating an equivalence between HProp and SProp is a viable one in my opinion. Ulrik Buchholtz suggested something like this to me a few years ago. I agree with your conjecture about homotopy canonicity... Perhaps we should prove this at some point. As for closed program extraction, perhaps this could work, I am not sure. I think it's definitely an interesting thing to explore.