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


  • 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


  • 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