Research talks

• Directed univalence in simplicial homotopy type theory (Seminar of trimester program "Prospects of Formal Mathematics," Hausdorff Institute for Mathematics, Bonn, July 24)  

• Formalization of ∞-category theory (Logic and Semantics Seminar, Aarhus University, Aarhus, June 24) 

• The dependent Gödel fibration (ItaCa Fest 2024, June 24, video)

• Formalization of ∞-category theory (OCIE/MPP Seminar, Chapman University, Orange, CA, Mary 24, video)

• Synthetic Foundations & Formalization of ∞-Category Theory (Topology Seminar, University of Virginia, Charlottesville, VA)

• Formalizing the ∞-categorical Yoneda lemma (CPP 2024, IET, London, UK, Jan 24, video)

• Formalizing the ∞-categorical Yoneda lemma (BUGCAT, Binghamton University, NY, Nov 23)

• Formalizing the ∞-categorical Yoneda lemma (Slides, abstract) (Abstract Homotopy Theory Seminar, Max Planck Institute for Mathematics, Bonn, Germany, Aug 23)

• Formalizing the ∞-categorical Yoneda lemma (Topology Seminar, NTNU, Trondheim, Norway, Aug 23, invited)

• The dependent Gödel fibration (CT 23, UCLouvain, Louvain-la-Neuve, Jul 23)

• Internal sums for synthetic fibered (∞,1)-categories (Homotopy Type Theory 2023, Carnegie Mellon University, Pittsburgh, PA, May 23)

• Synthetic fibered (∞,1)-category theory (San Diego Category Theory and Type Theory Seminar, University of San Diego, San Diego, CA, Feb 23, video, invited)

• Generalized Dialectica constructions via Skolemization (HoTT Seminar, Carnegie Mellon University, Pittsburgh, PA, Nov 22)

• Dialectica constructions and lenses (Doktorandentreff AG Logik, TU Darmstadt, Germany, Oct 22)

• Dialectica constructions and lenses (Berkeley Seminar, Topos Institute, California, CA, Sep 22, video)

• A type theory for (∞,1)-categories (Berkeley Seminar, Topos Institute, California, CA, Sep 22, video)

• Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability (HoTT/UF 2022, Haifa/Internet, Jul 22, video)

• Synthetic (∞,1)-category theory in simplicial homotopy type theory (Uni Regensburg, SFB Higher Invariants Seminar, Jul 22, invited)

• Synthetic Tait Computability for Simplicial Type Theory (TYPES 2022, Nantes/Internet, June 22, video) 

• Simplicial homotopy type theory (MSRI HC Pt 2, Cuernavaca, Morelos, Mexico, June 22)

• Synthetic fibered (∞,1)-category theory (JMRA, March 22, video)

• Synthetic fibered (∞,1)-category theory (Logic and higher structures, CIRM, Marseille, Feb 22, video)

• Synthetic fibered (∞,1)-category theory (HoTTEST Event for Junior Researchers 2022, Western University, London, ON, online, Jan 22, video)

• Synthetic fibered (∞,1)-category theory (Topology Seminar, EPFL, Lausanne, Nov 21, invited)

• Synthetic fibered (∞,1)-category theory (Theoretical Computer Science Seminar, University of Birmingham, online, Nov 21)

• Internal sums for synthetic fibered (∞, 1)-categories (CaTCat: Open House on Category Theory 2021, celebrating F. Marmolejos 60th Birthday. Ciudad de México, online, Nov 21)

• Synthetic fibered (∞,1)-category theory (Novemberfest 2021, uOttawa, online, Nov 21) (video)

• A Yoneda Lemma for synthetic fibered ∞‑categories (CMU HoTT Graduate Student Workshop 2021, Carnegie Mellon University, online, Feb 21, invited) 

• A Yoneda Lemma for synthetic fibered ∞-categories  (Doktorandentreff AG Logik, TU Darmstadt, online, Dec 20) 

• A synthetic language for fibered higher categories (Doktorandentreff AG Logik, TU Darmstadt, online, Nov 20) 

• Cocartesian Fibrations in Simplicial Type Theory (correction Feb 19, 21) (Pittsburgh's HoTT Seminar, online, Sep 20)

• Modalities and Fibrations for Synthetic (∞,1)-Categories (New York City Category Theory Seminar, The Graduate Center of The City University of New York, New York, NY, Oct 19, invited) (video)

• Modalities and Fibrations for Synthetic (∞,1)-Categories (HoTT Seminar, Carnegie Mellon University, Pittsburgh, PA, Oct 19)

• Modalities and Fibrations for Synthetic (∞,1)-Categories (Category Theory Seminar, Johns Hopkins University, Baltimore, MD, Sep 19, invited)

• Type-theoretic Modalities for Synthetic (∞,1)-Categories (Homotopy Type Theory 2019, Pittsburgh, PA, Aug 19)

• Type-theoretic Modalities for Synthetic (∞,1)-Categories (TYPES 2019, Oslo, Jun 19)

• Fibrations, Modalities, and Universes for Synthetic (∞,1)-Categories (CAS, Oslo, Jun 19)

• Universes in a Type Theory for Synthetic ∞-Category Theory (CAS, Oslo, Dec 18)

• Universes in a Type Theory for Synthetic ∞-Category Theory (EUTYPES 2018, Aarhus, Oct 18)

• Simplicial Sets inside Cubical Sets (PSSL, Amsterdam, Oct 18)

• (Truncated) Simplicial Models of Type Theory (Workshop on HoTT/UF, FLoC, Oxford, Jul 18)

• Stable ∞-Categories in ∞-Cosmoses (PSSL, Brno, Apr 18)

• Fibrations in Type Theory with Shapes (PSSL, Santiago de Compostela, Jan 18)

• Interpreting Cubical Type Theory in Appropriate Presheaf Toposes (Working group "Logique de la Programmation", Aix-Marseille Université, Luminy, Sep 17)

• Interpreting Cubical Type Theory in Appropriate Presheaf Toposes (PSSL, Leeds, Sep 17)

• Interpreting Cubical Type Theory in Appropriate Presheaf Toposes (Workshop on HoTT/UF, FSCD, Oxford, Sep 17)

Expository talks

• Topological Hochschild Homology et al (Prismatic Cohomology Seminar, Johns Hopkins University, Baltimore, MD, Spring 23)

• Invertible TFTs and bordism spectra (TQFT Reading Group, Johns Hopkins University, Baltimore, MD, Spring 23)

• Goodwillie calculus and the n-excisive modality in an ∞-topos (Goodwillie Calculus Reading Group, Johns Hopkins University, Baltimore, MD, Fall 22)

• Homotopy type theory and synthetic homotopy theory (Intro to HoTT mini-series, Topology Seminar, MPIM Bonn, March 22)

• Lurie's Adjoint Functor Theorem for (∞,1)-Categories (Mini-workshop ∞-Categories, Darmstadt, Feb 19)

• What is...a Higher Category? (What is...? Seminar, Darmstadt, Nov 18) (expository)

• Proof of Model-Independence of ∞-Category Theory in an ∞-Cosmos (MIT Talbot 2018: Model-Independent Theory of ∞-Categories, Government Camp, OR, May 18)