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>