3. More type theory & Invisible mathematics#
3.1. Outline#
We continue a review of type theory and introduce the following notions:
identity types
universes
natural numbers
We then briefly look at “invisible mathematics”, a collective term for methods that make human mathematics possible, but are not explicitly talked about by mathematicians.
3.2. Reading material#
Please continue reading Egbert Rijke’s textbook to learn more about identity types, universes and natural numbers:
Egbert Rijke, Introduction to homotopy type theory, Chapters 1–4
A talk about invisible mathematics, with slides containing detailed speaker notes, is available at:
Andrej Bauer, Formalizing invisible mathematics, Machine assisted proofs, February 2023, Institute for Pure and Applied Mathematics – UCLA, Los Angeles, USA. (video, slides)
3.3. Homework#
Play the natural numbers game