Path induction and the indiscernibility of identicals
Hosted by the Faculty of Mathematics, Cambridge University 2025 LMS Hardy Lecturer. Emily Riehl, Johns Hopkins University, Baltimore MD, U.S.A. Date & Time. Monday, 30 June 2025, 4pm. Location. The Chapel at Churchill College, Churchill Road. Coordinators. Enrico Pajer, Benedikt Löwe.

Abstract. 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.

The LMS Hardy Lectureship is named after G.H. Hardy, former President of the London Mathematical Society. The LMS Hardy Lecturer visits the UK and gives a number of lectures at many UK universities. The 2025 Hardy Lecturer is Emily Riehl who the Kelly Miller Professor of Mathematics at Johns Hopkins University, a leading expert in higher category theory, and a well-known and enthusiastic expositor of mathematics. In 2007, she did Part III at Churchill College, Cambridge.

Venue. The Chapel at Churchill College is located at the west end of the grounds of Churchill College. Due to the secular nature of the College, it is independent from the College and managed by the Chapel Trust. The Chapel was designed by the architect Richard Sheppard (who also designed the College itself) and built in 1967 as a modern interpretation of a Byzantine basilica. It was the building of the month October 2007 of the Twentieth Century Society.

How to get there. The Chapel is located at the end of Churchill Road, a private road off Storey's Way that passes through the grounds of Churchill College. It is close to the main car park at the top end of the College. See  map of Churchill College. According to google maps it is an 16 minute walk from the CMS to the Chapel (but google maps does not know about the entrance to the Churchill College grounds on Madingley Road).