# 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