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

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: Ssreflectand 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

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:

Ssreflectand 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: