The HoTT Seminar meets Fridays 1-3 pm in BH 150.

Here is a partial list of recent seminars:

2020:

- January 17: Jon Sterling (CMU), Gluing Models of Type Theory Along Flat Functors

2019:

- December 6: Jonas Frey (CMU), Categories of Partial Equivalence Relations as Localizations
- November 22: Mathieu Anel (CMU), A Small Object Argument for Unique Factorization Systems
- November 15: Evan Cavallo (CMU), Modelling Identity Types with a Fibred Factorization System
- October 11: Andrew Swan (CMU), Lifting Problems and Algebraic Weak Factorisation Systems over a Grothendieck Fibration
- October 4: Jonathan Weinberger (Darmstadt), Modalities and Fibrations for Synthetic (∞,1)-Categories
- May 3: Greg Langmead (CMU), Categories and Modalities for Smoothness: Part 2
- April 26: Adam Millar (CMU), The Groupoid Model; Zesen Qian (CMU) Induction and Coinduction
- April 19: Anders Mortberg (CMU), UniMath – Univalent Foundations of Mathematics
- March 29: Jonathan Sterling (CMU), Algebraic Type Theory and the Gluing Construction
- March 22: Mathieu Anel (CMU), Small Objects and Their Arguments
- March 11-15: Geometry in Modal Homotopy Type Theory (workshop)
- February 28: Loïc Pujet (Nantes), Synthetic Homotopy Theory in Cubical Type Theory and the Hopf Fibration
- February 22: Iosif Petrakis (LMU Munich), Dependent Sums and Products in Bishop Set Theory
- February 15: David Spivak (MIT), A Higher-Order Temporal Logic for Dynamical Systems
- February 8: Bruno Bentzen (CMU), Informal Cartesian Cubical Type Theory
- February 1: Steve Awodey (CMU), A Quillen Model Structure on the Cartesian Cubical Sets
- January 25: Colin Zwanziger (CMU), Modal Categories with Attributes: Part 2
- January 18: Felix Wellen (CMU), Covering Spaces in Modal HoTT

2018:

- December 14: Colin Zwanziger (CMU), Modal Categories with Attributes: Part 1
- December 7: Siva Somayyajula (CMU), Perspectives on Sessions
- November 30: Koundinya Vajjha (Pittsburgh), Voevodsky’s Simplicial Modal of HoTT
- November 21: Egbert Rijke (UIUC), The Small Object Argument in Terms of the Pushout-Product.
- November 20: David Jaz Myers (Johns Hopkins)
- November 16: Adam Millar (CMU), The Groupoid Model as a Category with Families
- November 9: Greg Langmead (CMU), Categories and Modalities for Smoothness
- November 2: Steve Awodey (CMU), Lax and Strict Models of Dependent Type Theory
- October 25: Marcelo Fiore (Cambridge), 2-Dimensional Lambda Calculus
- October 5, 12, 19: Jonas Frey (CMU), Semantics of Type Theory
- September 21, 28: Mathieu Anel (CMU), Type Theory v. Higher Category Theory
- September 7: Max Doré (LMU Munich) and Colin Zwanziger (CMU), Intension and Extension in Type Theory
- April 27: Dan Christensen (Western Ontario), Vector Fields on Spheres
- April 13: Colin Zwanziger (CMU), Intensional Predicates in Comonadic Intensional Type Theory
- April 6: Marcelo Fiore (Cambridge), An Algebraic Combinatorial Approach to the Abstract Syntax of Opetopic Structures
- March 8: Andrew Pitts, Pursuing Univalence with Categorical Logic
- February 16: Mathieu Anel (Paris), What’s New in oo-Topoi?
- February 8: Eric Finster (Paris), Lex Modalities in Type Theory
- February 6, 13: André Joyal (Montreal), Theory of Tribes.
- February 2: Felix Wellen (CMU), Algebraic Geometry and Modal Type Theory
- January 26: Joseph Helfer (Stanford), First-Order Homotopical Logic
- January 19: Felix Wellen (CMU), Fiber Bundles in HoTT
- January 15: Ian Orton (Cambridge), An internal presentation of cubical models

2017:

- December 8: Marco Larrea (Leeds), Models of Martin-Löf Type Theory from Algebraic Weak Factorisation Systems
- November 3, 10, 17: Anders Mörtberg (CMU), Introduction to Cubical Type Theory.
- October 20: Simon Boulier (Nantes), Model Structure on the Universe in a Two Level Type Theory
- October 13: Felix Wellen (CMU), Differential Homotopy Type Theor
- September 22: Clive Newstead (CMU), Polynomials, Representability and Dependent Type Theory
- September 1: Pino Rosolini (Genova), Dominance