Dr. Emily Riehl
Johns Hopkins University

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 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 traditional equality because 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.

Bio

Emily Riehl is a Professor of Mathematics at Johns Hopkins University in Baltimore. In addition to her research, in category theory and homotopy type theory, she has written several books and expository articles directed at various mathematical audiences, most of which are freely available online. She is also a co-founder of Spectra: the organization for LGBTQ mathematicians.

Math Colloquiums

Colloquium Seminars are held on select Fridays throughout the year. These broad audience presentations are intended to introduce the VCU community to the world of mathematics. Colloquium presentations explore topics in mathematics, applied mathematics, math history and education, and the exciting connections between math, science, art and humanities. 

Reception to follow.