Seminar

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.

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

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

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

Created on April 19, 2018 at 17:16:58
by
Univalent foundations special year 2012