i'm beginning to think that universes of strict propositions have no redeeming features 🙃
@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.
@AndrasKovacs @amy So to bring it back home, we are only discussing whether definitional proof irrelevance is worth it, as opposed to working with "mere propositions". The motivations of definitional proof irrelevance are (contrary to your comment) not semantic at all, but rather they have to do with usability. And these are strong motivations indeed, and there is a lot of evidence that people like having definitional proof irrelevance for these reasons.
My comment was that I am increasingly thinking that these advantages of definitional proof irrelevance are not worth it, for two reasons:
1. They have devastating syntactic effects (e.g. ability to do unification, etc.); note that cubical type theory might have the same problem ultimately, but I am not certain.
2. Because the "real" propositions that work for doing math (and computer science: think about acccessibility predicates!) will always be the "mere proposition”/HoTT-style ones, and these can only coincide with the strict ones under equality reflection, there is always a very painful tension between these two things. It may be that SProp can be used judiciously to make some really nice things work (I'm thinking of cool reflection-style strictification results like those of Pujet, Pedrot, etc. where you make the category laws hold definitionally, etc.), and I think this is a very interesting use-case. But this is very different from the idea of (e.g.) Lean and OTT, where the main propositions are proof-irrelevant.
@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.
@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.