Talks

Mini-courses

UCLA Distinguished Lecture Series, also part of the Distinguished Women in Math Lecture Series organized by the Women in Math group; Contractibility as uniqueness, Path induction and the indiscernibility of identicals, Arrow induction and the dependent Yoneda lemma.
On the ∞-topos semantics of homotopy type theory delivered at CIRM-Luminy as part of the workshop Logic and Higher Structures; lecture notes.
The model-independent theory of (∞,1)-categories delivered at the Isaac Newton Institute for Mathematical Sciences at the University of Cambridge as part of the workshop Higher structures in homotopy theory to open the semester program Homotopy Harnessing Higher Structures: lecture 1, lecture 2, lecture 3, lecture 4.
A mini course ∞-category theory from scratch given at the 2015 Young Topologists’ Meeting: lecture 1, lecture 2, lecture 3, lecture 4.

Technical lectures

The ∞-cosmos project: formalizing 1-, 2-, V-, and ∞-category theory in Lean, slides and video from a talk given at Lean Together 2025.
Formalizing post-rigorous mathematics, slides from a talk given at the Hausdorff Institute Trimester Program: Prospects of Formal Mathematics.
Formalizing ∞-category theory in the Rzk proof assistant, slides from a talk given at the Interactions of Proof Assistants and Mathematics summer school describing ongoing formalization project; video from another version given at the Hausdorff Institute a year later.
Homotopy types as homotopy types, lecture notes from A panorama of homotopy theory: a conference in honour of Mike Hopkins; video.
The equivariant uniform Kan fibration model of cubical homotopy type theory, a talk given in the cubical sets seminar at MSRI; slides.
A macrocosm principle for cartesian fibrations given at the Workshop on Higher Structures in Geometry and Physics at the Fields Institute.
A formal theory for ∞-categories, slides from the 2019 International Category Theory Conference in Edinburgh.
The synthetic approach to ∞-category theory from the Summer School on Higher Topos Theory and Univalent Foundations at Leeds.
The synthetic theory of ∞-categories vs the synthetic theory of ∞-categories given at the Vladimir Voevodsky Memorial Conference at IAS; slides.
A proof of the model-independence of ∞-category theory delivered at the workshop ∞-Categories, ∞-Operads, and their Applications at the Casa Matématica Oaxaca.
A proof of the model-independence of (∞,1)-category theory, slides from a talk given at the 2018 International Category Theory Conference.
The synthetic theory of ∞-categories vs the synthetic theory of ∞-categories, from the Homotopy Type Theory Electronic Seminar Talks; slides.
Foundations of (∞,2)-category theory, a talk at the Women in Topology workshop at MSRI outlining a research program.
On the directed univalence axiom, slides from the 2018 Joint Mathematics Meetings.
A synthetic theory of ∞-categories in homotopy type theory, slides from Octoberfest at Carnegie Mellon University.
A synthetic theory of ∞-categories in homotopy type theory, slides from CT2017 at the University of British Columbia.
Towards a synthetic theory of (∞,1)-categories given at the 2016 Workshop on Homotopy Type Theory and Univalent Foundations of Mathematics at the Fields Institute.
The formal theory of adjunctions, monads, algebras, and descent, from the workshop Reimagining the Foundations of Algebraic Topology at MSRI; slides.
Limits of quasi-categories with (co)limits, from the Connections for Women workshop at MSRI.
Homotopy coherent adjunctions, slides from the AMS Special Session on Homotopy Theory at the 2014 Joint Mathematics Meetings.
The formal theory of homotopy coherent monads, slides from the Samuel Eilenberg Centenary Conference.
Algebraic model structures, slides from the AWM Anniversary Conference at ICERM.
Cellularity, composition, and morphisms of weak factorization systems, slides from the CT2011 at the University of British Columbia.
Algebraic model structures slides from the 2011 CMS Summer Meeting at the University of Alberta.
Algebraic model structures, slides from CT2010 at the University of Genova.

Colloquia

Prospects for computer formalization of infinite-dimensional category theory and Collaborative formalizations of ∞-category theory, a pair of colloquia delivered at the end of a mini course at UCLouvain; also a condensed and updated version delivered at CPP 2025.
Do we need a new foundation for higher structures?, a colloquium given at Rutgers.
A reintroduction to proofs, a Logic @ Texas State undergraduate colloquium.
A reintroduction to proofs, given as the PIMS Distinguished Lecture at the University of Regina.
Path induction and the indiscernibility of identicals, a colloquium given at UCLouvain.
Introduction to Homotopy Type Theory and Univalent Foundations, a Tech Talk given at Google X.
Elements of ∞-Category Theory, a colloquium given at the General Meeting of the London Mathematical Society.
Elements of ∞-Category Theory, a colloquium hosted by the Matrix Institute; slides.
Elements of ∞-Category Theory, a virtual talk for the Mathematical Picture Language seminar at Harvard; slides.
Contractibility as Uniqueness, a Topos Institute colloquium talk; slides.
Contractibility as Uniqueness, a talk for LGBTQ+Math Day held virtually at the Fields Institute.
∞-category theory for undergraduates, a talk in the Berkeley Logic Colloquium; slides.
The complicial sets model of higher ∞-categories, slides from Structures supérieures at CIRM.
The complicial sets model of higher ∞-categories slides from Between Topology and Quantum Field Theory: A conference in celebration of Dan Freed’s 60th birthday.
The complicial sets model of higher ∞-categories, slides from a colloquium given at the Perimeter Institute.
A universal approach to universal algebra, a colloquium given at the Center for Geometry and Physics in Pohang, Korea.
A synthetic theory of ∞-categories in homotopy type theory, slides from a colloquium given to the Association of Symbolic Logic at the 2018 Joint Mathematics Meetings.
Quasi-category theory you can use, slides from the Graduate Student Topology and Geometry Conference at UT Austin.

Applied category theory

The Yoneda Lemma in the category of Matrices, a tutorial given as part of Applied Category Theory 2020; slides.
Categorifying cardinal arithmetic, slides originally prepared for the Category Theory for All session at MAA MathFest; condensed version that gives away the answers to the questions posed.
A categorical view of computational effects given at Lambda World Cádiz.
A categorical view of computational effects, a keynote lecture delivered at the Compose Conference; slides.
Functoriality in algebra and topology, slides from a colloquium talk given to pure and applied mathematicians at Macquarie University.

General audience

The mathematical multiverse: the case against a unified mathematical reality, for Investigating Reality: A Philosophical, Mathematical, and Scientific Exploration at the Santa Fe Institute.
On the art of giving the same name to different things, an expanded version for the Calgary Mathematics and Philosophy Lectures and the SUMS 2023: Math and Language conference.
Mathematician explains infinity in 5 levels of difficulty, episode 22 of the WIRED 5 levels series.
On the art of giving the same name to different things, slides prepared for a joint talk with Stephanie Burt for The Multiplicity Turn: Theories of Identity from Poetry to Mathematics.
Transition to Research, slides prepared for a panel discussion for the paraDIGMS 2021 Spring Conference.
A brief introduction to ∞-cosmoi and higher category theory, filmed by Quanta Magazine.
A formal language for ∞-category theory, the 2020 President’s Frontier Award lecture.
The mathematics of social choice, slides prepared for the 2019 National Math Festival and video for a talk given in the Thursday Think Speaker Series for Math for America.
A promotional video for Fat Chance: Probability from 0 to 1 also available as a course on edX.

the Stable Marriage Problem

A solution to the stable marriage problem, a public lecture given virtually at the Perimeter Institute for Theoretical Physics.
The stable marriage problem and the math behind the scenes, produced by Numberphile.
The stable marriage problem, filmed by Girls’ Angle.
A solution to the stable marriage problem, a Pecha Kucha presentation geared toward members of the Harvard math department.