Dear Nicola,

Thank you for sharing with us this very sad news about your mentor and friend Peter Aczel.  
My condolences to you, and to his family of course.

Peter was a great logician.  He had a very creative and original mind, which tended toward unconventional topics: the type-theoretic interpretation of constructive set theory, ill-founded set theories, dependently typed theories, unusual modalities.  I welcomed his interest in HoTT when we discussed it in Munich during the two summers that we spent there together, sometime around 2008-9.  He was one of the participants at the original meeting on “the homotopy interpretation of constructive type theory” at Oberwolfach in 2011.

Peter's mathematics, while totally rigorous, was always presented in a simple, clear and informal style.  As Andrej recalled, it was Peter who proposed the idea of “informal type theory” as a WG at the IAS in 2012.  Until then, we had been working in a straight-jacket of formal proofs + categorical semantics, and it was liberating to simply *use* the type theory to reason informally about the intended homotopical interpretation - in a way that could be made formal (e.g. in a proof assistant), and proven to be sound - but just once, and then the formal proofs and their explicit semantics didn’t need to be constantly revisited. 

His experience with categorical logic, and in particular his idea of logic enriched type theory, also influenced the development of the language of HoTT by extending basic MLTT with type-indexed predicate logical operations like disjunctions and existential quantifiers.

Peter was particularly fascinated by univalence (of course), and (if I’m not mistaken) coined the phrase “structure identity principle” for its extension to algebraic structures.  He lectured on this in Munich and later at CMU.  I tried to get him to write a paper on it, but he always said that it was not really his own idea. 

In addition to being a great logician, Peter was a modest and kind person.  I was very grateful for his friendship during a difficult time at the IAS, after a sudden death in my family.  And I enjoyed visiting him and Helen at their house in the Midlands after he retired.  

Here’s Peter’s website, with some unpublished slides and preprints (I recommend the paper "The Russell-Prawitz Modality”):

http://www.cs.man.ac.uk/~petera/

And attached is a photo of Peter from a visit to Pittsburgh in 2016 (note the hat).

We have lost an inspiring intellect and a dear colleague.

In sadness,

Steve

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/3229059E-D300-40BD-9677-B7352CD9DF8F%40andrew.cmu.edu.