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. On Sun, Jan 5, 2025 at 4:31 AM Paul Levy <p.b.levy@bham.ac.uk<mailto:p.b.levy@bham.ac.uk>> wrote: This is really sad news. He was such a great person to talk to and made so many contributions. Martin Escardo said that Thomas knew about the Univalence axiom before it had a name. He also was the first to formulate a version of the WISC axiom: https://ncatlab.org/nlab/show/WISC I would also like to mention his work on control operators, with Martin Hofmann and Bernhard Reus, which I found illuminating in my PhD work. Paul From: Oosten, J. van (Jaap) <J.vanOosten@uu.nl<mailto:J.vanOosten@uu.nl>> Date: Friday, 3 January 2025 at 11:49 To: categories@mq.edu.au<mailto:categories@mq.edu.au> <categories@mq.edu.au<mailto:categories@mq.edu.au>> Cc: Oosten, J. van (Jaap) <J.vanOosten@uu.nl<mailto:J.vanOosten@uu.nl>> Subject: Thomas Streicher CAUTION: This email originated from outside the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe. I just received information that Thomas Streicher passed away yesterday. Thomas fell ill last September, when he could not attend Pino Rosolini's retirement party due to pneumonia; then it turned out he has metastases in the lungs from a pancreatic cancer. After several chemo treatments his situation suddenly worsened, and yesterday he died, peacefully, without pain. Thomas was 66 years old. In Thomas, we mourn a logician and category theorist of exceptional calibre. Let me just recall that in 2011, during an Oberwolfach meeting, Vladimir Voevodsky praised Thomas' work on type theory as a paradigm of precision. But I personally mourn a friend. A warm person with many interests. I wish strength to his wife Eva, and his family. Jaap van Oosten 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 | Leave group | Learn more about Microsoft 365 Groups 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>