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 — given by Per Martin-Löf's intensional identity types — encodes 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 and path induction is justified by the fact that based path spaces are contractible.
Abstract: Queer theory challenges essentialist or normative conceptions of identity, often using personal stories to show the limits of conventional categories. In this talk, I will share my journey as a queer mathematician, tracing the formation of a pair of identities that were more often developed in parallel rather than fully integrated. I will also describe a recent "queering" of the concept of "identity" in mathematics, which enables a more expansive notion of mathematical equality than appears in traditional mathematical foundations.
PDF version of this announcement (suitable for posting).