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!

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