Martin Escardo. Notes originally written for the module Advanced Functional Programming of the University of Birmingham, UK.

Lecture Notes

  1. Introduction
  2. Propositions as types and basic Martin-Löf type theory
    1. Basic Martin-Löf Type Theory
    2. Empty type 𝟘
    3. Unit type 𝟙
    4. Binary type 𝟚
    5. Product types Π
    6. Sum types Σ
    7. Binary products _×_
    8. Binary sums _∔_
    9. Identity types _≡_
    10. Natural numbers ℕ
    11. Negation ¬
    12. Function extensionality
  3. Propositions as types versus propositions as booleans
  4. Isomorphisms ≅
    1. Definition and basic examples
    2. Binary sums as a special case of sums
    3. Binary products as a special case of products
  5. More types, their elimination principles, and their isomorphism with Basic MLTT types
    1. Booleans and their manifestation as a Basic MLTT type
    2. Finite types and their manifestation as a Basic MLTT type
    3. Lists
    4. Vectors
    5. List and vector isomorphisms
  6. More constructions and proofs with the above types:
    1. Natural numbers
    2. Booleans
    3. Finite types
    4. Lists
    5. Vectors
  7. Hedberg’s Theorem

Index of all Agda files

Advanced further reading

  1. Introduction to Homotopy Type Theory and Univalent Foundations (HoTT/UF) with Agda.

Each of the links above will take you to a different Agda module. You can use this to interactively explore the lecture notes: the Agda code is all type-checked (with the exception of some exercises which are left as holes, {! !}), and presented as hypertext. Click on an identifier to be taken to its definition.

HoTTEST School github repository