On the axioms for identity types

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