The first and only time I met Thomas was in September 2019 at the Workshop on Continuity, Computability, Constructivity (CCC) in Ljubljana. I was only a first-year PhD student and earlier that year at TYPES I had felt a little out of place at times, but Thomas immediately made me feel very comfortable and it was very fun to talk with him. We made some tentative plans for me to visit him, but unfortunately, and partly because of the pandemic, I never followed up on these plans. We are fortunate that Thomas has left us with great expository notes on categorical logic, and realizability, as well as his book on domain-theoretic semantics of functional programming, all of which I have found very useful. My condolences to his friends and family, Tom On 03/01/2025 13:53, Jon Sterling wrote:

I am so sad to hear this tragic news about Thomas. Thomas was very kind and encouraging to me over the years, and made me feel welcome in this community; I imagine he had this impact on many other young people finding their way. In addition to his momentous scientific contributions that I owe my career to, Thomas was also a great conservator of important knowledge that might otherwise have been lost had he not intervened.

Sincerely, Jon

On Fri, Jan 3, 2025, at 12:09 PM, Neil Ghani wrote:

...

I'm so gutted. Thomas was an exceptional category theorist but also an exceptional human being. He had a brilliant sense of humour and we loved laughing about the oddities of mathematics.

A terrible start to 2025.

Neil

Sent from Outlook for iOS

domain=aka.ms Z0QTCmO5wZsjPQMPNhQtWSR3MPW?domain=aka.ms>>

...

*From:* Oosten, J. van (Jaap) <J.vanOosten@uu.nl> *Sent:* Friday, January 3, 2025 11:47 am *To:* categories@mq.edu.au <categories@mq.edu.au> *Cc:* Oosten, J. van (Jaap) <J.vanOosten@uu.nl> *Subject:* Thomas Streicher

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>

Very sad news to start the New Year with. Like others, I was greatly influenced by Thomas’s work — I read his “Semantics” book cover to cover early in my PhD, and have had its meticulous proofs and terrible typography burned into my brain ever since. As others have noted, he and Martin Hofmann were the first to discover many of the ideas that later grew into homotopy type theory; I first met him (if I remember right) at the 2011 Oberwolfach meeting which brought Voevodsky’s work together with the established “old guard” of type theorists. Thomas was wonderful to talk maths with over a beer — gruff and opinionated, but always amiable and constructive in his disagreements. I didn’t see him much since Covid, and am sorry that I never got to discuss more recent developments with him, and now never will. With condolences to his family and friends, –Peter. 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>

Because of the last messages that we interchanged, I was also expecting Thomas to recover. I think that I remember meeting him in Como 2000. He was sitting on a bench reading a draft of a paper that I had sent him. The paper was motivated by Thomas' work in collaboration with P. Lietz about the typed PCAs that induce realizability toposes. From the bench he invited me to talk about it. I don't remember the details of our chat, but I still feel grateful for his genuine interest. We did not meet often but each time we did, we disagreed on something about topos theory. As others have stressed, he was very kind, patient, and clever, so it was very informative and constructive to disagree with him. In 2015, the question of whether every pre-cohesive geometric morphism is molecular caught Thomas' attention, and we started to exchange emails more often. He had developed a sophisticated 'fibered view' of geometric morphisms (described “Fibered categories à la Jean Benabou”, Preprint; arxiv:1801.02927), and he attempted to apply it to the problem, but we could not answer the question. Again, we disagreed; he was convinced that there had to be non-molecular pre-cohesive topos and I am still hopeful that there is not. Anyway, since we could not answer the question, he proposed weaker forms of the problem and incited others (including myself) to look for counter-examples. See the 2021 papers by Hemelaer-Rogers, and by Garner-Streicher, and also Remark 3.8 in my 2022 paper edited by Thomas. All these examples show, as Thomas was suggesting, that as soon as you weaken the definition of pre-cohesive map a bit, there are non-molecular examples. Also around 2022 I showed that, over a Boolean base, pre-cohesive does imply molecular. Of course, this had a purely mathematical motivation, but I was very happy to use the result to continue arguing with Thomas about the original question. More recently, after the 2023 workshop on doctrines and fibrations that Thomas organized with Milly in Padova to celebrate Lawvere's life, we started discussing some of Bill's ideas about measurable cardinals. I was humbled to see how much Thomas knew about the classical literature on the subject. Of course, we disagreed on how much that literature should influence our work, and we had fun doing so until he fell ill. So we discussed other things, but he kept his good humour. M. El dom, 12 ene 2025 a las 19:30, Jens Hemelaer (<hemelaerjens@gmail.com<mailto:hemelaerjens@gmail.com>>) escribió: I am grateful for getting in touch with Thomas in 2020 through this mailing list. It was wonderful to care about the same problems and then approach them with different methods, and I will miss the joyfulness and passion that came through in his e-mails. My condolences to his family and friends, Jens On Tue, 7 Jan 2025 at 00:01, Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com<mailto:p.l.lumsdaine@gmail.com>> wrote: Very sad news to start the New Year with. Like others, I was greatly influenced by Thomas’s work — I read his “Semantics” book cover to cover early in my PhD, and have had its meticulous proofs and terrible typography burned into my brain ever since. As others have noted, he and Martin Hofmann were the first to discover many of the ideas that later grew into homotopy type theory; I first met him (if I remember right) at the 2011 Oberwolfach meeting which brought Voevodsky’s work together with the established “old guard” of type theorists. Thomas was wonderful to talk maths with over a beer — gruff and opinionated, but always amiable and constructive in his disagreements. I didn’t see him much since Covid, and am sorry that I never got to discuss more recent developments with him, and now never will. With condolences to his family and friends, –Peter. 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>

Thomas was not only a brilliant type theorist, category theorist and mathematician, as many already pointed out, he was also very generous with his time, happy to discuss any topic he was interested in. He was like a walking lexicon. I am devastated. It was him who introduced me to type theory and constructivism, changing the course of my PhD, eventually co-supervising it. Thomas had a massive impact on my life, more than he will ever know now. I am immensely grateful to have had the privilege to work with him. It was great fun writing papers with him, then afterwards going for a nice meal. Those were good times, back then in Passau and Munich in the 90es. As a PhD student, I remember going into his office to ask a question, coming out, hours later, with many new questions to think about. Amazed and bedazzled by what I just heard. His great sense of humour and passion for the subject was second to none. At conferences, there were always colleagues queueing to have a chat with him. When they made Thomas, they broke the mould. Like Jaap, I mourn a great friend. My heart goes out to Eva, his wife, and all his friends and family. Bernhard ________________________________ From: Oosten, J. van (Jaap) <J.vanOosten@uu.nl<mailto:J.vanOosten@uu.nl>> Sent: Friday, January 3, 2025 11:47 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 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>

Dear Jaap, I was not closed to Thomas Streicher but I remember a warm person with a great passion for logic and category theory. His work with Martin Hofmann on the groupoid model of Martin-Lof type theory was a precursor of the homotopy models of Awodey-Warren and Voevodsky. He took seriously the work of Benabou on fibered categories and he applied it successfully to type theory. Jonathan Weinberger, his last student, has great contributions to simplicial homotopy theory. We will miss him. André Joyal ________________________________ De : Bernhard Reus <bernhard@sussex.ac.uk> Envoyé : 3 janvier 2025 09:36 À : Oosten, J. van (Jaap) <J.vanOosten@uu.nl>; categories@mq.edu.au <categories@mq.edu.au> Objet : Re: Thomas Streicher Thomas was not only a brilliant type theorist, category theorist and mathematician, as many already pointed out, he was also very generous with his time, happy to discuss any topic he was interested in. He was like a walking lexicon. I am devastated. It was him who introduced me to type theory and constructivism, changing the course of my PhD, eventually co-supervising it. Thomas had a massive impact on my life, more than he will ever know now. I am immensely grateful to have had the privilege to work with him. It was great fun writing papers with him, then afterwards going for a nice meal. Those were good times, back then in Passau and Munich in the 90es. As a PhD student, I remember going into his office to ask a question, coming out, hours later, with many new questions to think about. Amazed and bedazzled by what I just heard. His great sense of humour and passion for the subject was second to none. At conferences, there were always colleagues queueing to have a chat with him. When they made Thomas, they broke the mould. Like Jaap, I mourn a great friend. My heart goes out to Eva, his wife, and all his friends and family. Bernhard ________________________________ From: Oosten, J. van (Jaap) <J.vanOosten@uu.nl<mailto:J.vanOosten@uu.nl>> Sent: Friday, January 3, 2025 11:47 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 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>

Thomas was the inspiration why I took up category theory when I started my PhD. I had not encountered CT before. I started my PhD on modal and temporal logic, moving from the TU Munich to the LMU, which is where I met Thomas as he was still at the LMU at the chair of Martin Wirsing at the time, working with Bernhard Reus. This was in 1995. A highlight I remember well, in April 1999, we organized a Spring School in Munich where Thomas lectured on Fibered Categories (and Giuseppe Rosolini on Sheaves and Martin Hyland on Categorical Logic and Type Theory). Over the years, every now and then, I had a question on CT and Thomas always took the time to explain everything. He once even added sth to his notes on fibred category as an answer. Last time I met him was less than a year ago on zoom and I still remember vividly the inspiration and energy I got from talking to him. My thoughts go to all who have been much closer to Thomas than me. Alexander ---------- You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. Leave group: https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27

What sad news! Thomas was a very good friend. He was not one for big hugs or other effusiveness, but someone to count on and trust. I will miss him dearly, and I wish I had shown more affection when I last saw him in the meeting celebrating Bill Lawvere. Thomas could be pretty intimidating because of the abilities mentioned by others, but once you got over that, he was a lovely teddy bear-like friend. My sentiments to his family and friends. Thank you, Jaap, for conveying the bad news. Valeria On Fri, Jan 3, 2025 at 8:45 AM Graham White <g.graham.white@gmail.com<mailto:g.graham.white@gmail.com>> wrote: Such a loss. Graham On Fri, Jan 3, 2025 at 3:42 PM Joyal, André <joyal.andre@uqam.ca<mailto:joyal.andre@uqam.ca>> wrote: Dear Jaap, I was not closed to Thomas Streicher but I remember a warm person with a great passion for logic and category theory. His work with Martin Hofmann on the groupoid model of Martin-Lof type theory was a precursor of the homotopy models of Awodey-Warren and Voevodsky. He took seriously the work of Benabou on fibered categories and he applied it successfully to type theory. Jonathan Weinberger, his last student, has great contributions to simplicial homotopy theory. We will miss him. André Joyal ________________________________ De : Bernhard Reus <bernhard@sussex.ac.uk<mailto:bernhard@sussex.ac.uk>> Envoyé : 3 janvier 2025 09:36 À : Oosten, J. van (Jaap) <J.vanOosten@uu.nl<mailto:J.vanOosten@uu.nl>>; categories@mq.edu.au<mailto:categories@mq.edu.au> <categories@mq.edu.au<mailto:categories@mq.edu.au>> Objet : Re: Thomas Streicher Thomas was not only a brilliant type theorist, category theorist and mathematician, as many already pointed out, he was also very generous with his time, happy to discuss any topic he was interested in. He was like a walking lexicon. I am devastated. It was him who introduced me to type theory and constructivism, changing the course of my PhD, eventually co-supervising it. Thomas had a massive impact on my life, more than he will ever know now. I am immensely grateful to have had the privilege to work with him. It was great fun writing papers with him, then afterwards going for a nice meal. Those were good times, back then in Passau and Munich in the 90es. As a PhD student, I remember going into his office to ask a question, coming out, hours later, with many new questions to think about. Amazed and bedazzled by what I just heard. His great sense of humour and passion for the subject was second to none. At conferences, there were always colleagues queueing to have a chat with him. When they made Thomas, they broke the mould. Like Jaap, I mourn a great friend. My heart goes out to Eva, his wife, and all his friends and family. Bernhard ________________________________ From: Oosten, J. van (Jaap) <J.vanOosten@uu.nl<mailto:J.vanOosten@uu.nl>> Sent: Friday, January 3, 2025 11:47 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 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 -- Graham White London 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>

Thomas has been my mentor, on from my second semester as an undergraduate in Darmstadt more than 15 years ago, all through the years of a pandemic PhD, and up until these last months. In the summer/fall 2009, shortly after his eager and very warm reply to me cold-emailing him about some questions for references in category theory and the course curriculum, I had the immense pleasure to starting to attend his course cycle on category theory, categorical logic, realizability, and domain theory. His direct style in lectures and conversations were immediately compelling to me. I am grateful for the countless hours in which Thomas taught me (fibered) category theory, type theory, and logic from his unique point of view, always with tireless, joyful enthusiasm. Being such a curious person himself, he taught me to never stop asking questions, be it in mathematics or other aspects of life. When possible, our discussions would lead from his office to a café, and then to a bar. His calm but lively demeanor and very Austrian humor always provided joy and relief, particularly during stressful phases. As an advisor, he would not get tired answering any (repeated) question that I had, and he would always foster my academic autonomy. I cannot imagine how my academic life would have turned out without such a brilliant, supportive, encouraging, attentive, passionate, generous, patient, funny, and heartfelt mentor such as Thomas. I am deeply sad for the loss of such an inspiring and dear person for Eva, the community, and anyone who knew or was close to him. Thomas, I hope you got to see some light in these last dark months. I will miss you forever. Jonathan Am Fr., 3. Jan. 2025 um 22:10 Uhr schrieb Robin Cockett <robin@ucalgary.ca<mailto:robin@ucalgary.ca>>: This is indeed a tragic loss to the category theory community ... I did not know Thomas Streicher well. However, I do remember being on a bus with him from Luminy to Marseille and falling into conversation with him: it left a lasting impression. It was a bit like falling into a black hole consisting of a unique mixture of humor and totally encyclopedic knowledge. The bus trip was altogether too short ... My condolences to his family. -robin (Robin Cockett) ________________________________ 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>

That's extremely sad news. It was always a privilege to meet Thomas at conferences and other events. He had an amazing sense of humour and was extremely patient and generous with his time. The influence he had on HoTT (which he wasn't even convinced of) is hard to overestimate. I send my sincere condolences to his family. Nicolai On Fri, Jan 3, 2025 at 11:02 PM Maria Emilia Maietti <maietti@math.unipd.it<mailto:maietti@math.unipd.it>> wrote: Dear all I would like to thank life for having met Thomas Streicher and having found in him a unique expert in solving problems in type theory with categorical methods. In particular, as a last thing of collaboration, I am very grateful to him for joining us in organizing the workshop on Doctrines and Fibrations, dedicated to Lawvere, in May 2023 in Padova https://events.math.unipd.it/WDF2023/#com. Deep condolences to Eva. Milly On 03/01/25 10:04, Oosten, J. van (Jaap) wrote: 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>

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<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>

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>

Dear all, Like so many of you I am deeply saddened by Thomas’ passing. As part of his position in Darmstadt, he could always hire a PhD or postdoc, and from 2006 - 2011 I was the lucky one. I arrived just after finishing my PhD and through Thomas I discovered many new areas of logic and category theory. I could walk into his office at any time and start talking about anything and before you knew it, hours had passed and we had touched upon anything from mathematics to philosophy, politics, food, literature and life in general. You got the impression he had studied everything. And not just that, he had also developed his own distinctive opinion about the topic. He would be very fond of unorthodox ideas and would often start a discussion with ``It is probably a complete waste of time, but…’’ and then launch into another fascinating digression. I start this year with the feeling that I have lost a dear colleague and a dear friend. I will miss his deep knowledge of the areas of mathematics he was so fond of and I came to love as well. I will miss the diners, the drinks and the conversation. I am glad to have been given the opportunity to have spent all these happy times with Thomas, but also very sad to realise these have now come to the end. I offer my condolences to all his colleagues, friends and family, and especially his wife Eva. Best wishes, Benno Op zo 5 jan 2025 om 14:55 schreef Paul Levy <p.b.levy@bham.ac.uk<mailto:p.b.levy@bham.ac.uk>>: Correction: it was not Martin Escardo but Steve Awodey who said “He knew about univalence before it was called that.” Paul From: Paul Levy <p.b.levy@bham.ac.uk<mailto:p.b.levy@bham.ac.uk>> Date: Sunday, 5 January 2025 at 00:31 To: categories@mq.edu.au<mailto:categories@mq.edu.au> <categories@mq.edu.au<mailto:categories@mq.edu.au>> Subject: Re: Thomas Streicher 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>