Path induction and the indiscernibility of identicals

Add to your list(s) Download to your calendar using vCal

• Emily Riehl (John Hopkins University, Baltimore)
• Monday 30 June 2025, 16:00-17:00
• The Chapel Churchill College, Storey’s Way, Cambridge, CB3 0DS.

If you have a question about this talk, please contact HoD Secretary, DPMMS.

Mathematics students learn a powerful technique for proving theorems about an arbitrary natural number: the principle of mathematical induction. This talk introduces a closely related proof technique called path induction, which can be thought of as an expression of Leibniz’s indiscernibility of identicals: if two objects are identified, then they must have the same properties, and conversely. What makes this interesting is that the notion of identification referenced here is given by Per Martin-Löf’s intensional identity types, which encode a more flexible notion of sameness than the traditional equality predicate in that an identification can carry data, for instance of an explicit isomorphism or equivalence. The nickname “path induction” for the elimination rule for identity types derives from a new homotopical interpretation of type theory, in which the terms of a type define the points of a space and identifications correspond to paths. In this homotopical context, indiscernibility of identicals is a consequence of the path lifting property of fibrations. Path induction is then justified by the fact that based path spaces are contractible.

This talk is part of the The LMS Hardy Lecture series.

This talk is included in these lists:

• All CMS events
• CMS Events
• CMS Seminars from business and industry
• DAMTP info aggregator
• DPMMS info aggregator
• Hanchen DaDaDash
• Interested Talks
• The Chapel Churchill College, Storey’s Way, Cambridge, CB3 0DS
• The LMS Hardy Lecture
• bld31

Note that ex-directory lists are not shown.