pl-thesaurus
pl-thesaurus copied to clipboard
Is K the same as propositional extensionality?
Judging from here: https://ncatlab.org/nlab/show/propositional+extensionality
the assertion of this equivalence is a special case of the univalence axiom
But axiom K is incompatible with univalence, because it implies Uniqueness of Identity Proofs (UIP). Wouldn't K be more like "propositional intensionality" i.e. it says two things are equal iff they are intensionally equal, because all proofs of equality are Refl?
Maybe I'm totally misunderstanding...