Amélia Liao 🍊😈 on Nostr: i find univalence appealing because it greatly increases the amount of things i can ...

i find univalence appealing because it greatly increases the amount of things i can not care about. definitional proof irrelevance— and this includes the limited case of definitional UIP— is appealing at first because now there are things you totally don't have to care about, but in reality it forces you to care extra hard about so many more things, even at the set-level, than you would have to had you gone for a proper, semantic notion of proposition.

as an example, inverses in a group are unique, but not in general not definitionally so, so if all your infrastructure for not caring about things is built around strict propositions, you have successfully conned yourself into caring about you shouldn't have to (especially if you're trying to beat a system for inferring properties into coming up with something you've made into structure... 💎). and sure, you could put the inverses behind a truncation, so now they totally don't need caring about... but everyone agrees that would be silly, right? since that's a strict truncation, there's no getting out of it, not without implying full equality reflection. it wouldn't be unjustified to postulate unique choice, and use that to "get back" an inverse-assigning map, but... that's not gonna compute. regardless of how concrete your group implementations actually are.

mathlib is extremely concerned with the distinction between finite-products categories and cartesian monoidal categories. to a comparable extreme i do not want to care about that. any theorem of category theory is insensitive to the set-theoretic identity of your product-assigning map. you should not need a truncation here. if you ask me, the observable difference between "having products" and "being equipped with an operation that assigns products" on strict categories speaks to nothing more to the pathology of any foundation that insists on K.

(as a note, a category having products is exactly analogous to a semigroup having identities: they needn't be preserved by arbitrary maps but they are preserved by all the invertible maps, in the appropriate sense.)

to be clear, for this latter example, even if you've moved past not-caring being an artificial syntactic thing you have to choose ahead of time, even if you know how to not-care about things that happen to be unique, at the set-level, you're still boned! there's not many univalent categories to go around when that necessarily implies that objects have no automorphisms, and uniqueness of limits, like other cases of structure identity, genuinely needs univalence— not only do you need to turn an iso into an identification, you have to show that this identification takes the iso to the identity.

and all of that is setting aside the actual no-go theorems like in section 8.2 of "A Cubical Language for Bishop Sets" that, and i hope i can get away with this paraphrasing when i know all the authors on here, imply (a) the ad-hoc purely syntactic notion of strict proposition is Bad, Actually (b) these end up in an utterly privileged position in your type theory, e.g. only strict can propositions have effective quotients, so everything gets Worse, Actually