# HoTTEST Summer School 2022

The **HoTTEST Summer School 2022** will take place online everywhere in the world during the months of July and August 2022. It will start with parallel introductions to homotopy type theory and formalization, and end with a series of colloquia introducing more advanced topics and exciting areas for further study.

The school will run both synchronously and asynchronously. The lectures will be delivered live (between 2:30-4pm UTC) and paired with various tutorial sessions run by teaching assistants. The course will also feature a discord-based all-hours Q&A and an online archive of all course materials so that participants can follow along on their own schedule.

A central aim of the summer school is to build community among all of the participants, irrespective of geography. To further this, we will hold some online social events (e.g. game nights) for the summer school staff and participants.

Details will be announced here in due course.

# Essential information

**Dates:**July-August 2022.**Live lectures:**2:30-4 PM UTC.**Discord:**https://discord.gg/tkhJ9zCGs9**GitHub:**repository.**Youtube:**HoTTEST-
**Google Calendar:**link

# Audience

This school is for everyone and anyone with some familiarity with abstract mathematics or theoretical computer science and an itching to learn about homotopy type theory. Our goal is to make homotopy type theory accessible to, and inclusive of, everyone who is interested, regardless of cultural background, age, ability, formal education, ethnicity, gender identity, or expression. We believe HoTT is for everyone, and are committed to fostering a kind, inclusive environment.

Attendance is free of charge.

# Schedule

The lectures take place MWF 2:30-4 PM UTC, starting July 4 and ending August 19. There are two parallel tracks: Homotopy Type Theory (HoTT) and Formalization in Agda (Agda).

July 4
HoTT |
July 6
Agda |
July 8
HoTT |

July 11
HoTT |
July 13
Agda |
July 15
HoTT |

July 18
Agda |
July 20
HoTT |
July 22
Agda |

July 25
HoTT |
July 27
Agda |
July 29
HoTT |

August 1
HoTT |
August 3
Agda |
August 5
HoTT |

August 8
Agda |
August 10
HoTT |
August 12
Agda |

August 15
HoTT |
August 17
Agda |
August 19
HoTT |

The end-of-summer colloquia follow the same schedule on the following dates:

- August 22:
**Jon Sterling**,*How to code your own type theory*

There is a considerable distance between the formal rules of type theory and the code that you must write in order to animate them as a running program. In this colloquium, you will learn the basic techniques of type theoretic implementation in the OCaml programming language, including the representation of syntax as well as type-directed conversion. - August 24:
**Pierre Cagne**,*Group theory without groups*During the summer school, two key aspects of HoTT (and their cubical derivatives) have been put on display: identity types and univalent universes. In this colloquium, we will take advantage of both these features of HoTT to introduce what I like to call synthetic symmetry theory, which is essentially a univalent type-theoretic take on group theory. The usual presentation of groups as sets structured by multiplication, inverse and neutral operations is cast aside to the benefit of what are, in my opinion, the intended stars of the show: the mathematical objects on which groups act. This is a shift in perspective, that many group theorists probably implement at an informal level of reasoning, which is here taken seriously at a formal level.

I will introduce basic notions of group theory through this lens. People in the audience with no background whatsoever in classical group theory are invited to consider this as an introduction to a new fun area of mathematics, while those knowlegdeable about group theory in its classical form are welcome to contrast what will be presented here with the classical theory. At the end of the colloquium, both the former and the latter should be able, and hopefully enticed, to read further about the subject in the work-in-progress book Symmetry (https://unimath.github.io/SymmetryBook/book.pdf). - August 26:
**Jonas Frey**,*Modalities and Cohesive HoTT*

Motivated by the example of truncation levels, this talk will start out by systematically introducing and discussing the notion of*modality*in HoTT, mostly following [1]. In particular we will see characterizations of modalities and ways to construct them. The second part of the talk will give a brief introduction to the ideas of*cohesive*homotopy type theory, which is an extension of homotopy type theory in which modalities play a central role [2].

[1] Egbert Rijke, Michael Shulman, Bas Spitters.*Modalities in homotopy type theory.*Logical Methods in Computer Science 16 (2020).

[2] Michael Shulman,*Brouwer's fixed-point theorem in real-cohesive homotopy type theory.*Mathematical Structures in Computer Science 28.6 (2018): 856-941. - August 29:
**Favonia**,*Cartesian cubical type theory*

We have multiple variants of cubical type theory different from what we have seen in Cubical Agda. In the colloquium, I will introduce another main variant---Cartesian cubical type theory. - August 31:
**Chaitanya Leena Subramaniam**,*Semantics of HoTT*

The goal of this talk is to explain the homotopical semantics of HoTT, i.e. why the constructions of HoTT are meaningful in ordinary homotopy theory. We will see how the categorical semantics of dependent types and identity types allows them to be interpreted as, respectively, fibrations and path objects of a model category, following [1]. Following [2], this can be extended to an interpretation of univalence in the model category of simplicial sets. The model category of simplicial sets presents the Grothendieck (∞,1)-topos of ∞-groupoids, and we will see that every Grothendieck (∞,1)-topos has a canonical model of univalence, following [3].

[1] Homotopy theoretic models of identity types. S. Awodey and M. Warren

[2] The simplicial model of univalent foundations (after Voevodsky). K. Kapulkin and P. LeFanu Lumsdaine

[3] All (∞,1)-toposes have strict univalent universes. M. Shulman

# Staff

## Instructors

- Ulrik Buchholtz
- Martín Hötzel Escardó
- Dan Licata
- Anders Mörtberg
- Paige North
- Emily Riehl
- Egbert Rijke

## Colloquium speakers

- Pierre Cagne
- Favonia
- Jonas Frey
- Jon Sterling
- Chaitanya Leena Subramaniam

## Teaching assistants

- Elisabeth Bonnevier
- Tom de Jong
- Jarl G. Taxerås Flaten
- Chris Grossack
- Artem Gureev
- Perry Hart
- Astra Kolomatskaia
- Amélia Liao
- Axel Ljungström
- Matheus Magalhães de Alcantara
- Jacob Neumann
- Johannes Schipp von Branitz
- Christopher Stough-Brown
- Max Zeuner

## Organizers

- Carlo Angiuli
- Dan Christensen
- Martín Hötzel Escardó
- Chris Kapulkin
- Dan Licata
- Emily Riehl
- Egbert Rijke