[HoTT] Peter Aczel

[HoTT] Peter Aczel

[Steve Awodey]

[-- Attachment #1: Type: text/plain, Size: 2971 bytes --]

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.

[-- Attachment #2: IMG_5698.jpeg --]
[-- Type: image/jpeg, Size: 507427 bytes --]

[-- Attachment #3: Type: text/plain, Size: 1753 bytes --]




> On Aug 3, 2023, at 4:12 AM, Nicola Gambino <Nicola.Gambino@manchester.ac.uk> wrote:
> 
> Dear colleagues and friends,
> 
> I write to let you know of the sad news that Peter Aczel passed away on August 1st.
> 
> As many readers of this list surely know, Peter made many fundamental and deeply influential contributions to Logic, Computer Science, Category Theory, and Constructive Mathematics. He had an active interest in Homotopy Type Theory and Univalent Foundations from the early days of the subjects, participating in the Oberwolfach meeting in 2011 and the Special Year at the Institute for Advanced Study in 2012/13.
> 
> I had the good fortune of having him as PhD supervisor and we remained in contact since then. I always admired his clarity of thinking and his kindness. He will be deeply missed.
> 
> With best regards,
> Nicola
> 
> =
> Dr Nicola Gambino
> Department of Mathematics, University of Manchester
> 
> -- 
> 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/1670F781-BEB6-45D0-9466-DA546711E329%40manchester.ac.uk.
> 

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

Re: [HoTT] Peter Aczel

[Joyal, André]

[-- Attachment #1.1: Type: text/plain, Size: 6301 bytes --]

Dear Nicola,


Sad news.

I wish to express you my condolences for the disparition of Peter Aczel, your mentor.

Aczel was a very original thinker.
He was interested in non-classical logic, in non-classical foundations.
His theory of non-well founded sets is very beautiful.
He showed that circular arguments can be rigorous.

I visited him in Manchester around 1992.
He was interested in category theory.
He also attended the program on univalent foundation of type theory at the IAS in 2013.
He was interested in homotopy type theory.


We will all miss him,

André








________________________________
De : homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> de la part de Steve Awodey <awodey@andrew.cmu.edu>
Envoyé : 3 août 2023 13:49
À : Nicola Gambino <Nicola.Gambino@manchester.ac.uk>
Cc : Andrej Bauer <andrej.bauer@andrej.com>; DANA.SCOTT@cs.cmu.edu <DANA.SCOTT@cs.cmu.edu>; Andrew Pitts <amp12@cam.ac.uk>; Marc Bezem <marc.bezem@uib.no>; Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Objet : [HoTT] Peter Aczel

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.
[cid:bb02386c-211d-4d33-a6c2-d7627c143124@CANPRD01.PROD.OUTLOOK.COM]



> On Aug 3, 2023, at 4:12 AM, Nicola Gambino <Nicola.Gambino@manchester.ac.uk> wrote:
>
> Dear colleagues and friends,
>
> I write to let you know of the sad news that Peter Aczel passed away on August 1st.
>
> As many readers of this list surely know, Peter made many fundamental and deeply influential contributions to Logic, Computer Science, Category Theory, and Constructive Mathematics. He had an active interest in Homotopy Type Theory and Univalent Foundations from the early days of the subjects, participating in the Oberwolfach meeting in 2011 and the Special Year at the Institute for Advanced Study in 2012/13.
>
> I had the good fortune of having him as PhD supervisor and we remained in contact since then. I always admired his clarity of thinking and his kindness. He will be deeply missed.
>
> With best regards,
> Nicola
>
> =
> Dr Nicola Gambino
> Department of Mathematics, University of Manchester
>
> --
> 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/1670F781-BEB6-45D0-9466-DA546711E329%40manchester.ac.uk.
>

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

-- 
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/QB1PR01MB2948568B4EE752780E0E3E96FD08A%40QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM.

[-- Attachment #1.2: Type: text/html, Size: 16759 bytes --]

[-- Attachment #2: IMG_5698.jpeg --]
[-- Type: image/jpeg, Size: 507427 bytes --]

Re: [HoTT] Peter Aczel

[amp]

[-- Attachment #1.1: Type: text/plain, Size: 1085 bytes --]

I was very saddened to read the news of Peter Aczel's death. 

I greatly admired his work, not only for its content but also for its 
clarity. His promotion of informal rigorous reasoning in type theory that 
Andrej Bauer mentioned in another post is an example. He also had very nice 
handwriting! -- I found this out
when he very generously shared some of his unpublished work with me when I 
was a graduate student in the late 70s and early 80s. (He later examined my 
PhD thesis.)

RIP, Peter.

Andrew M. Pitts
Professor of Theoretical Computer Science
Department of Computer Science and Technology
University of Cambridge 
William Gates Building 
15 JJ Thomson Ave
Cambridge CB3 0FD, UK

-- 
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/a1e5f28a-165d-4558-826a-6ccec5c2ecefn%40googlegroups.com.

[-- Attachment #1.2: Type: text/html, Size: 1436 bytes --]

Re: [HoTT] Peter Aczel

[andrej.bauer]

> 
> I write to let you know of the sad news that Peter Aczel passed away on August 1st.
> 

This is sad news indeed. My condolences go to his family.

Let Peter Aczel’s contribution to homotopy type theory be remembered. In 2012 at IAS he initiated a working group on informal rigorous reasoning in type theory, whose activities expanded into the writing of the HoTT book. Without Peter’s initiative there would be no book, nor the ensuing success of homotopy type theory.

With kind regards,

Andrej

-- 
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/40E71FEB-72B6-4FDC-BA7B-C206FDE54717%40andrej.com.

[HoTT] Peter Aczel

[Nicola Gambino]

Dear colleagues and friends,

I write to let you know of the sad news that Peter Aczel passed away on August 1st.

As many readers of this list surely know, Peter made many fundamental and deeply influential contributions to Logic, Computer Science, Category Theory, and Constructive Mathematics. He had an active interest in Homotopy Type Theory and Univalent Foundations from the early days of the subjects, participating in the Oberwolfach meeting in 2011 and the Special Year at the Institute for Advanced Study in 2012/13.

I had the good fortune of having him as PhD supervisor and we remained in contact since then. I always admired his clarity of thinking and his kindness. He will be deeply missed.

With best regards,
Nicola

=
Dr Nicola Gambino
Department of Mathematics, University of Manchester

-- 
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/1670F781-BEB6-45D0-9466-DA546711E329%40manchester.ac.uk.