6 events
when toggle format what by license comment
Oct 9 '21 at 6:22 comment added L. Garde @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 added Grant Jurgensen 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 added Grant Jurgensen 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 added Andrej Bauer 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 First answers
Sep 25 '21 at 11:34
S Sep 25 '21 at 8:23 history answered L. Garde CC BY-SA 4.0