Path Induction and the Indiscernibility of Identicals

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 x and y 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.

About the Speaker

Emily Riehl is a professor of mathematics at Johns Hopkins University. She received her Ph.D. at the University of Chicago working with Peter May and then was a postdoctoral fellow at Harvard University. She was Lead Organizer of the Higher Categories and Categorification Program at MSRI in 2020 and has held visiting positions at the Centre of Australian Category Theory, Institut Mittag-Leffler, Center for Advanced Study at the Norwegian Academy of Science and Letters, and the Max Planck and Hausdorff Research Institutes for Mathematics.

In addition to her many journal publications, Riehl is the author of the books Categories in Context and Categorical homotopy theory. She is a co-host of the n-Category Café. 

Riehl was the recipient of the fourth AWM Joan & Joseph Birman Research Prize in Topology and Geometry and the sixth recipient of the $250,000 President's Frontier Award, which supports Johns Hopkins researchers poised to become leaders in their field. She is a co-founder of Spectra, an association for LGBT mathematicians.