This is the website for the Lean seminar open to the broad Barcelona Mathematical community.


The most important resource is the Lean Community website. Here is a selection of resources from there, but feel free to look for more.


Starting September 29th 2021, we meet on Wednesdays 15h-16h at room C3B/111 (UAB). Interested participants are encouraged to play the NNG before the first meeting, but we won’t assume they have done it. To communicate we use our own Zuplip chat, you can join it by clicking on the following invitation link:


On April 28, 2021 we had an invited talk by Joachim Kock (UAB). The video is available below.

References after the talk

Thomas Jan Mikhail is providing us with a very good list of references: 1) Joachim mentioned Rijke’s book on HoTT which you can find here: On the same website there are also lecture notes on the same subject. 2) Joachim also mentioned HoTT’s standard reference, the HoTT book: The HoTT book offers much more motivation. However the main body of the book develops type theory in an informal setting. This is a conscious decision; the aim is to present an alternative to the informal set theory used in “everyday mathematics”. Rijke’s book introduces type theory formally right from the start but offers less motivation. The HoTT book also contains a formal treatment, but it’s deferred to the appendix. 3) For a quick overview of HoTT I the following two papers can be helpful: Macor J. – A brief Introduction to Type Theory and the Univalence Axiom Grayson D. – An Introduction to Univalent Foundations for Mathematics Here are some further references on Type Theory. 4) Lambek, Scott – Introduction to Higher Order Categorical Logic 5) Martin-Löf – An Intuitionistic Theory of Types: Martin Löf – Intuitionistic Type Theory (Lecture Notes)

Leave a comment

Your email address will not be published. Required fields are marked *