Post #1846809
2026-04-26 16:08 UTC
@jonmsterling Some other interesting questions: What about propositional resizing? (I guess it isn't neutral?) Also, for those understandably reluctant to call univalence neutral, is propositional univalence neutral?
Replies (2)
-
@carloangiuli@mathstodon.xyz 2026-04-26 16:10
@jonmsterling Cursed follow-up: How many people think function extensionality *isn't* neutral?
-
@jonmsterling@mathstodon.xyz 2026-04-26 16:11
@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.