There are various tutorials by UF participants.
Tutorials are usually on Mondays, 4 – 5:30 pm, in S-101.

Future tutorials



Past tutorials


Monday March 25: Isomorphism of Types: a Simple(-Typed) Viewpoint (Sergei Soloviev)

Monday March 11: Homotopy colimits (Egbert Rijke)

Monday February 18: Infinity categories (Joachim Kock)

Monday February 11: Homotopy in Quillen model categories (Eric Finster) [following Dwyer-Spalinski]

Monday February 4: n-Types and h-Levels (Mike Shulman)

Monday January 28: Quillen Model Categories (André Joyal)

Friday January 25: H-Levels (Mike Shulman)

Friday January 18: HoTT tutorial (Egbert Rijke)

Monday December 17: State of the HoTT library (Andrej Bauer)

Monday December 10: Type Classes in Coq (Matthieu Sozeau)

Monday November 26: Logical Frameworks (Bob Harper) [notes]

Monday November 19: Homotopy initial algebras (Kristina Sojakova)

Tuesday November 13: Computational content of UA (Thierry Coquand)
Monday November 12: Computational content of UA (Thierry Coquand)

Monday November 5: How to implement type theory in 500 lines (Andrej Bauer) [code]

Monday October 22: Simplicial sets I (Mike Shulman) [notes]

Monday October 15: Higher inductive types (Guillaume Brunerie)

Monday October 8: The groupoid model of type theory (Thierry Coquand)

Tuesday October 2: Introduction to homotopy type theory (Mike Shulman)

Friday September 28: Type theories as (various) categories (Peter Lumsdaine) [wiki page]
Wednesday September 26: Type theory for mathematicians (Peter Aczel)

Other possible topics

  • Doing homotopy type theory in Coq: Bauer
  • Higher topos theory for type theorists: Shulman
  • Introduction to the Coq source code
  • Doing homotopy type theory in Agda
  • How not to annoy a type theorist: Licata

Feel free to add suggestions!