On Sun, Jan 5, 2025 at 5:54 AM Urs Schreiber <urs.schreiber@googlemail.com<mailto:urs.schreiber@googlemail.com>> wrote:
Martin Escardo said that Thomas knew about the Univalence axiom before it had a name.
Yes, the idea is essentially the "universe extensionality" in section 5.4 of "The groupoid interpretation of type theory" (83-111 in ISBN:9780198501275, pdf), which is where vv will have seen it. Keeping the term "universe extensionality" would have been the right thing to do. The main issue is that the definition of equivalence of types used there is subtly wrong, and vv's contribution really was to fix this part. To be fair to Martin and Thomas, it's not wrong in the context where they used it, namely a universe of discrete groupoids. It *would* be wrong if the same definition were also used for higher types. After the definition of universe extensionality, that paper also contains a prescient definition of what are now called "univalent categories", arguably the best way to formulate category theory in homotopy type theory. You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>