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)

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

Feel free to add suggestions!