Website

Contractibility as uniqueness: What does it mean for something to exist uniquely? Classically, to say that a set A has a unique element means that there is an element x of A and any other element y of A equals x. When this assertion is applied to a space A, instead of a mere set, and interpreted in a continuous fashion, it encodes the statement that the space is contractible, i.e., that A is continuously deformable to a point. This talk will explore this notion of contractibility as uniqueness and its role in generalizing from ordinary categories to infinite-dimensional categories.

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.

Arrow induction and the dependent Yoneda lemma: Arguably the least straightforward theorem of 1-category theory to extend to ∞-categories is the Yoneda lemma. The aim of this talk will be to present a few new perspectives on this result that can be used both to generalize its statement and provide a model-independent proof. Because we work at a level of abstraction in which an ∞-category is simply an object in a suitable “∞-cosmos,” no prior acquaintance with ∞-categories will be required. We show that Ross Street’s “Chevalley criterion” gives rise to two model-independent characterizations of “cartesian fibrations” of ∞-categories in terms of the presence of certain right adjoints. In fact, cartesian arrows can be characterized similarly in terms of the presence of certain “relative” right adjoints, from which the characterization of cartesian fibrations follows by considering the generic cartesian lift of the universal arrow. These notions can then be used to state and prove a fibrational form of the Yoneda lemma. By an analogy in which arrows in an ∞-category are thought of as directed paths, there is a principle of “arrow induction” that categorifies the principle of “path induction.” We explain how this unravels to a “dependent” generalization of the Yoneda lemma. This involves joint work with Dominic Verity and Mike Shulman.