On the axioms for identity types
- Date: Wednesday 26 April 2017, 14:00 – 15:30
- Location: Mathematics Level 8, MALL 1 & 2, School of Mathematics
- Type: Proofs, Constructions and Computations, Seminars, Pure Mathematics
- Cost: Free
Nicola Gambino, University of Leeds. Part of the proofs, constructions and computations seminar series.
I will discuss a few variants of the axioms for identity types. These variations depend on two parameters: one arises from the difference between Martin-Löf’s original formulation and the subsequent Paulin-Mohring formulation; the other depends instead on whether one is working in a type theory with Pi-types or not (similarly to how one formulates the notion of a natural number object in categories). I will explain these variants, outline the equivalence between the Martin-Löf formulation and the Paulin-Mohring formulation (both in the presence of Pi-types and without) and explain the category-theoretic counterparts of these formulations, ending with a discussion of the proof of the existence of the identity type weak factorisation system.
Nicola Gambino, University of Leeds