Lecture outline:
- Girard's paradox with one type of all types;
- difference with Russell's paradox;
- universe as reflection principle;
- algebraic proof of canonicity using the Artin gluing technique and normalization proof;
- application to proof verification.
