The Univalent Foundations Seminar will meet Wednesdays and Thursdays 11 – 12:30 in S-101 beginning 9.26.2012.
See http://www.math.ias.edu/seminars for all currently scheduled IAS talks, and the calendar page here for the UF talks.

There are sometimes some additional seminars on Friday 11 – 12:30 in S-101

Notes for Vladimir seminars are available here: expressions_current.pdf and Universe polymorphic type sytem.pdf.

Past seminars



Monday April 15: TBA (Sergei Mehlikov)

Wednesday April 17: Linear type theory (Michael Warren)

Thursday April 18: Survey of results (The homotopy group)

Monday April 8: The semi-simplicial universe (Thierry Coquand)
Wednesday April 10: The category of hSets (Bas Spitters)
Thursday April 11: HoTT is a polyvalent foundation of mathematics (André Joyal)

Friday March 29: Revisiting the categorical interpretation of dependent type theory (Pierre-Louis Curien)
Thursday March 28: Natural models of type theory (Steve Awodey)
Wednesday March 27: The James construction and pi_4(S^3) (Guillaume Brunerie)

Thursday March 21: Substructural type theory (Noam Zeilberger)
Wednesday March 20: A proof assistant prototype based on algebraic effects and handlers (Andrej Bauer)

Friday March 15: W-types in SSets (Benno van den Berg)
Thursday March 14: Homotopy colimits and a descent theorem (Egbert Rijke)
Wednesday March 13: Eilenberg–MacLane spaces in HoTT (Dan Licata)

Thursday March 7: Setoids, e-categories and exact completions (Richard Garner)
Wednesday March 6: Cohomology in HoTT (Eric Finster)

Friday March 1: Cartesian closed bicategories of bimodules (Nicola Gambino)
Thursday February 28: Formal Abstract Homotopy Theory (Jeremy Avigad)
Wednesday February 27: Semantics of higher inductive types (Mike Shulman)

Friday February 22: The Universe is Indiscrete (Martin Escardo)
Thursday February 21: Locally Cartesian Closed Infinity Categories (Joachim Kock)
Wednesday February 20: pi_2(S^2) in HoTT (Guillaume Brunerie)

Thursday February 14: On finite types that are not h-sets (Sergey Mehlikov) [video]
Wednesday February 13: The Hopf fibration in HoTT (Peter Lumsdaine) [video]

Thursday February 7: The structure identity principle (Peter Aczel) [video]
Wednesday February 6: A Quillen model structure in HoTT (Peter Lumsdaine) [video]

Friday February 1: Weak infinity groupoids II (Guillaume Brunerie)
Thursday January 31: Calculus of opetopes (Eric Finster) [video]
Wednesday January 30: Weak infinity groupoids (Guillaume Brunerie) [video]

Thursday January 24: Orthogonal factorization systems in HoTT (Egbert Rijke) [notes] [video]
Wednesday January 23: Homotopy and Univalence (Thorsten Altenkirch) [video]

Thursday January 17: State of the new proof assistant (Dan Grayson) [video]
Wednesday January 16: Semi-simplicial types: what and why? (Peter Lumsdaine) [video]

Thursday December 20: Building HITs in realizability models (Andrej Bauer)

Friday December 14: A formalisation of semi-simplicial types, and some general issues about definitional equality (Hugo Herbelin)

Thursday December 13: Invariance under isomorphism and definability (Per Martin–Löf) [video]
Wednesday December 12: The univalence axiom for simplicial diagrams (Mike Shulman) [video]

Friday December 7: TS + OCAML + LF (Dan Grayson)
Thursday December 6: The simplicial set model (Peter Lumsdaine)
Wednesday December 5: Type Systems VII (Vladimir Voevodsky)

Friday November 30: The game model (Peter Dybjer) [slides] [video]
Thursday November 29: The simplicial set model (Chris Kapulkin) [video]
Wednesday November 28: Type Systems VI (Vladimir Voevodsky) [Description of LF in TS style] [video]

Wednesday November 21: Type Systems V (Vladimir Voevodsky) [video]

Friday November 16: pi_k(S^n) for k < n (Guillaume Brunerie)
Thursday November 15: The simplicial set model (Peter Lumsdaine) [video]
Wednesday November 14 (1:30 – 3): Type Systems IV (Vladimir Voevodsky)
Wednesday November 14: Towards implementing Higher Inductive Types (Mike Shulman) [notes] [video]

Friday November 9: Ssreflect and methodology for large-scale formalization (Assia Mahboubi)
Thursday November 8: The simplicial set model (Peter Lumsdaine)
Wednesday November 7: Informal HoTT (collective) [wiki page] and semi-simplicial types (Peter Lumsdaine) [wiki page]

Friday October 26: Universes in Type Theory (Zhaohui Luo) [slides]
Thursday October 25: The simplicial set model (Peter Lumsdaine)

Thursday October 18: Toward a computational interpretation of Univalence (Dan Licata) [video]

Thursday October 11: On the setoid model of type theory (Erik Palmgren) [slides] [video]
Wednesday October 10: Type Systems III (Vladimir Voevodsky) [video]

Friday October 5: Type Theories as representable maps of presheaves (Steve Awodey) [notes]
Thursday October 4: Univalent Foundations in Coq (Michael Warren) [video]
Wednesday October 3: Type Systems II (Vladimir Voevodsky) [video]

Wednesday September 26: Type Systems I (Vladimir Voevodsky) [video]

Other possible topics


Here are some proposed topics for future seminars, perhaps with speakers:

  • Higher inductive types: Lumsdaine
  • Reflective subcategories and higher modalities: Shulman