Dear all, some years back I put out a call for any information about Joyal's lecture(s) containing his arithmetic universe proof of Gödel's incompleteness theorem. It was suggested I ask Anders Kock, and he was able to give me if not that lecture, but a related lecture from 1974, with the above title. It contained a rough definition of an arithmetic universe, namely a pretopos in which the free category on any internal graph exists. There was also some good material on classifying toposes. For historical interest I have made the notes available, with Anders' permission, here: https://thehighergeometer.wordpress.com/2019/05/08/joyal-arithmetisation-dan... Others may be interested as to the state of the art at the time. I hope that one day we will see details of the incompleteness proof that still eludes my grasp! Best regards, David David Roberts Webpage: https://ncatlab.org/nlab/show/David+Roberts Blog: https://thehighergeometer.wordpress.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]