# Timeline for How does axiom K contradict univalence?

### Current License: CC BY-SA 4.0

6 events
when toggle format what by license comment
Oct 9 '21 at 6:22 comment @GrantJurgensen Your are right, my answer is elliptic on that point. The univalence axiom says more precisely that the map from identity to isomorphism is an equivalence (HoTT book A.3.1), that is to say it postulates a map from isomorphism to identity which is an inverse of the natural map from identity to isomorphism.
Sep 26 '21 at 0:39 comment It's also worth noting that I originally referred to univalence as a "a map from an isomorphism on types to an equality of the same types", i.e. a term of type Π A B: Type, A ≃ B -> A = B. This was perhaps a mistake; I believe univalence typically refers to the stronger claim Π A B: Type, (A ≃ B) ≃ (A = B), which I used to finish the above proof.
Sep 26 '21 at 0:25 comment Oh, I see now. It was not immediately clear to me how we could construct a contradiction from the different isomorphisms, but I worked it out. For anyone else as slow as me: Let x, y: A ≃ B, where x ≠ y, and ϕ: (A ≃ B) ≃ (A = B) the isomorphism obtained by specializing the univalence axiom to types A and B. By UIP, we have ϕ x = ϕ y, which cancels to x = y, a contradiction.
Sep 25 '21 at 8:43 comment The OP explicitly asked whether Axiom K and UIP are equivalent. Your answer is a bit misleading in that regard, so it is better to clarify: Axiom K is indeed an instance of UIP, but from that instance we can derive the rest of UIP.
S Sep 25 '21 at 8:23 review
Sep 25 '21 at 11:34
S Sep 25 '21 at 8:23 history answered