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

Here is a list of recent seminars:

2020 (online after mid-March):

- Upcoming Seminars
- April 3: Reid Barton (Pitt), Model Categories for o-Minimal Homotopy Theory
- March 27: Mathieu Anel (CMU) Clans from Lurie’s Geometries
- March 4: Samuele Maschio (Padua) The Minimalist Foundation and Axiomatic Set Theories
- February 28: Milly Maietti (Padua) Compatibility of the Minimalist Foundation with Homotopy Type Theory
- February 21: Jonas Frey (CMU), Duality for Clans
- February 14: Colin Zwanziger (CMU), Generalizing the Topos of Coalgebras to the Natural Model of Coalgebras
- February 7: Reid Barton (Pitt), The Algebra of Combinatorial Premodel Categories
- January 31: Steve Awodey (CMU), A Cubical Universe of Fibrations
- 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 (partial):

- 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