Thomas Streicher was honest and patient, and infinitely devoted to the ideas he cared for. Types. He cared for types and he will probably be remembered as long as types are around. Maybe they won't be called types forever, as most ideas get renamed, most writings overwritten, and most names forgotten. But a part of him will live as long as people talk about types in some language because he worked them out so carefully and so honestly. It is not always obvious that honesty is the best strategy, but Thomas demonstrated that it was. I am struggling what to say and this probably sounds terrible from many angles, but Thomas would understand. His patience made him invincible to most of our nonsense, and I am sure even to cancer. -- dusko On Sat, Jan 4, 2025 at 9:43 AM Jonas Frey <jonas743@gmail.com<mailto:jonas743@gmail.com>> wrote: I'm also very sad that Thomas has left us, and thankful for having known him. Like Jonathan, Thomas was my early mentor, and I learned an incredible amount from the two courses of his that I attended, and by reading pretty much all the other lecture notes on his website (which I still highly recommend to all students) and often knocking on his door to ask questions. At these occasions I experienced his patience and generosity that others have already mentioned. Through Thomas I also got in contact with the category theory and logic community, and found a PhD position with Paul-André Melliès in Paris, all of which has changed my life for the better, and for which I am very thankful. I'm also happy to see that he has touched the lives of so many people, and hope that we can retain some of his spirit and style in this community. Finally, regarding Thomas' relationship to constructive logic and mathematics, I think his attitude is well summarized by the following quote of his which left a lasting expression on me (though I'm not sure if he was quoting someone else): "Im Krieg, in der Liebe, und auf der Metaebene sind alle Mittel erlaubt". Jonas On Sat, 4 Jan 2025 at 16:28, Steven Vickers <s.j.vickers.1@bham.ac.uk<mailto:s.j.vickers.1@bham.ac.uk>> wrote: 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<mailto:J.vanOosten@uu.nl>> Sent: Friday, January 3, 2025 9:04 AM 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 | 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>