First, an interesting feature of the upcoming SProp sort is the ability to add axioms in SProp that will not endanger canonicity of the computational part of Coq (funext for example), while having built-in definitional proof-irrelevance (somehow, giving the same axiomatic freedom in Prop as OTT prefigured). The current setup of Prop + proof-irrelevance + funext is mostly fine though: it is compatible with extraction and provides a good base line for verification of programs / systems (when you don’t need univalence), and is backed up by the Set theoretic models we know of. UIP, which is implied by proof irrelevance, is really not necessary in practice to do dependent pattern-matching, so I’d rather advocate staying away from it when writing programs. It is a fine shortcut when reasoning about programs though, for which SProp will provide a better story in the future (when we’ll allow an equality in SProp that you can eliminate to Type, soundly). Consistent classical axioms could be added the same way in SProp, and it’s an interesting research question to see if each one really “adds” something to the theory or not (in terms of the class of definable computable functions for example).

Second, the axioms you list force you into a particular model indeed, so always have to be added with care. Even functional extensionality: it essentially says that functions have no effect, but one can give models of the theory where they do: see Boulier et al’s “The next 700 syntactic models of type theory”.

Third, Univalence provides a kind of mother-of-all axioms: funext, propext, proof-irrelevance, UIP for sets (where it should really live) all follow from it, some “by definition”. One can add classical axioms in hProp as well like excluded middle, but contrarily to Prop/Sprop, this will have an effect on the computational content of computational things in Type: the hProp/computational type interface is richer than what Prop’s singleton elimination allows. In particular, hProp enjoys the unique choice principle which says that on can extract witnesses of propositional unique existence proofs, e.g `|| Sigma ! x : A, P x || -> A`

. For that to work computationally, one needs to keep witnesses of such proofs: if you used excluded middle to build the unique existence proof, the use of unique choice will get stuck. In other words, all proofs are now relevant computationally / intentionally, even if they are irrelevant propositionally. Accordingly, we can no longer have an interesting proof-erasure procedure like the one that exists for Prop/SProp, where such a principle of unique choice cannot be defined.