Like so many others, I too was sad to learn of Thomas's death. Martin Escardo, who knew Thomas better than I did, wrote that he was very much against constructive mathematics yet was fond of studying its classical metatheory. That to me was a paradox. Once in our many discussions I remember him pulling me up to explain that he was a logician, not a constructive mathematician. Yet the discussions were fertile. In one, at the Formal Topology workshop in Stockholm, he gave his opinion that defining real exponentiation using a point-free definition of the reals would be too tedious for anyone ever to do it. That's obviously true if you go about it the wrong way (for example, using frame homomorphisms), but it spurred me to thinking how to make the task more tractable, and later my student Ming Ng worked out the details. In our paper we acknowledged Thomas's stimulation. Steve Vickers. ________________________________ From: Oosten, J. van (Jaap) <J.vanOosten@uu.nl> Sent: Friday, January 3, 2025 9:04 AM To: categories@mq.edu.au <categories@mq.edu.au> Cc: Oosten, J. van (Jaap) <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<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>