- 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.
- 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.
- 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.
- 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 Stable Marriage Problem