An Agda formalization companion to the Type Theory master course at the University of Padova, taught by Maria Emilia Maietti (theory) and Ingo Blechschmidt (practice), 2023/2024 edition.
The course itself uses Agda in Blechschmidt's half. More decisively: Agda
with --without-K is Martin-Löf intensional type theory (MLTT) with no
extra axioms — the exact system Maietti builds from scratch in the lectures.
Rocq's Calculus of Inductive Constructions adds an impredicative Prop sort
and a tactic language that obscure the direct correspondence. Every module
here maps one-to-one onto a section of extyp24.pdf.
src/MLTT/
├── Foundations/
│ ├── Judgments.agda §2 — four judgment forms, contexts
│ └── StructuralRules.agda §2.1–2.2 — weakening, substitution, exchange
├── TypeFormers/
│ ├── Singleton.agda §3.1 — N₁, trivial, ElN₁
│ ├── Natural.agda §3.2 — Nat, zero, succ, ElNat
│ ├── Lists.agda §3.4 — List A, [], _∷_, ElList
│ ├── Empty.agda §5 — N₀, ElN₀ (introduced with ⊥)
│ ├── Sum.agda §3.5 — A + B, inl, inr, ElSum
│ ├── Sigma.agda §3.8 — Σ x∈A.B(x), <_,_>, fst, snd, ElSig
│ ├── Pi.agda §3.9 — Π x∈A.B(x), λ, ap
│ ├── Cartesian.agda §3.11 — A × B as special Σ
│ └── Arrow.agda §3.12 — A → B as special Π
├── Equality/
│ ├── Intensional.agda §3.6 — Id(A,a,b), id, ElId (J-rule)
│ ├── Properties.agda §3.6 — sym, trans, cong, subst
│ ├── PathInduction.agda §3.7 — E-Idprog ↔ E-Id derivability
│ └── DefinitionalVsProp.agda §4 — Prop 4.1, 4.2, Corollary 4.3
├── Logic/
│ ├── PropositionsAsTypes.agda §5 — full Curry-Howard table
│ ├── Connectives.agda §5 — ⊤ ⊥ ∧ ∨ → ¬ ∀ ∃
│ └── Classical.agda §5 — LEM, DNE, ¬¬(A ∨ ¬A), stability
├── Universes/
│ ├── Tarski.agda §6.1 — U₀ à la Tarski, T : U₀ → Set
│ ├── Russell.agda §6.2 — U₀ à la Russell
│ └── Girard.agda §12 — U₀ : U₀ leads to contradiction
├── Programs/
│ ├── BooleanEquality.agda Blechschmidt §4 — eq? soundness + completeness
│ ├── InsertionSort.agda Blechschmidt §5 — sort, verify, correct-by-construction
│ └── Decidability.agda — Dec A, decidable equality, stable propositions
└── Exercises/
├── Chapter3.agda — §3 exercises (type former rules)
├── Chapter4.agda — §4 exercises (definitional vs propositional eq.)
├── Chapter5.agda — §5 exercises (logic translation, Peano axioms)
└── Summary.agda — §13 summary exercise
Every module uses:
{-# OPTIONS --without-K --safe #-}--without-Kdisables Streicher's K axiom, enforcing intensional MLTT (no proof-irrelevance, no UIP by default). This is exactly Maietti's ML₀.--safeprohibitspostulate,BUILTIN REWRITE, and other escape hatches that would silently extend the theory.
Exercises with open holes ({! !}) use --allow-unsolved-metas locally.
- Agda ≥ 2.6.4 (
agda --version) - No external library dependencies — everything is self-contained
Type-check everything at once:
agda src/MLTT/Everything.agdaOr load any individual file in Emacs/VS Code with the Agda plugin.
| Maietti § | Module | Key content |
|---|---|---|
| §2 | Foundations/Judgments | 4 judgment forms + Γ cont |
| §2.1–2.2 | Foundations/StructuralRules | weakening, substitution, exchange |
| §3.1 | TypeFormers/Singleton | N₁ |
| §3.2 | TypeFormers/Natural | Nat, ElNat, +, ×, ^ |
| §3.4 | TypeFormers/Lists | List, length, append, reverse |
| §3.5 | TypeFormers/Sum | A + B |
| §3.6–3.7 | Equality/Intensional | Id, J, E-Idprog |
| §3.8 | TypeFormers/Sigma | Σ-type |
| §3.9 | TypeFormers/Pi | Π-type |
| §4 | Equality/DefinitionalVsProp | Prop 4.1–4.3 |
| §5 | Logic/PropositionsAsTypes | Curry-Howard, ⊥, ∀, ∃, = |
| §6 | Universes/Tarski, Russell | U₀, codes |
| §12 | Universes/Girard | inconsistency of U₀ : U₀ |
- M.E. Maietti, Notes on Type Theory 2024, Università di Padova
- I. Blechschmidt, Let's play Agda, Padova 2024/2025 exercises
- P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis, 1984
- The Agda Team, Agda documentation, https://agda.readthedocs.io