The Calgary Math & Philosophy Lectures: Emily Riehl

Mathematics has developed an increasingly “higher dimensional” point of view of when different things deserve the same name, categorifying the traditional logical notion of equality to isomorphism (from Greek isos “equal” and morphe “form” or “shape”) and equivalence (from Latin aequus “equal” and valere “be well, be worth”). In practice, mathematicians tend to become more flexible in determining when different things deserve the same name as those things become more complicated, as measured by the dimensions of the categories to which they belong. Unfortunately, these pervasive notions of sameness no longer satisfy Leibniz’s identity of indiscernibles — the assertion that two objects are identical just when they share the same properties — essentially because the traditional set theoretical foundations of mathematics make it too easy to formulate “evil” statements. However, in a new proposed foundation system there are common rules that govern the meaning of identity for mathematical objects of any type that allow one to “transport” information along any identification. Moreover, as a consequence of Voevodsky’s univalence axiom, these identity types are faithful to the meanings of sameness that have emerged from centuries of mathematical practice.