Post #1846841

@carloangiuli I think propositional resizing is not neutral. Propositional univalence is a more interesting question; I think that somehow it is less neutral than full univalence, but I'm not exactly sure how to support that claim. The concern I have is that 1-toposes don't even satisfy propositional univalence in the mitchell-benabou language. So it is kind of a vacuous axiom, from a semantic point of view, unless you make bigger changes to the way that the system is formulated.