pl-thesaurus icon indicating copy to clipboard operation
pl-thesaurus copied to clipboard

Is K the same as propositional extensionality?

Open JoeyEremondi opened this issue 4 years ago • 1 comments

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...

JoeyEremondi avatar Oct 10 '19 18:10 JoeyEremondi