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

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

Paige North

HoTT

July 6

Martín Hötzel Escardó

Agda

July 8

Paige North

HoTT

July 11

Paige North

HoTT

July 13

Martín Hötzel Escardó

Agda

July 15

Ulrik Buchholtz

HoTT

July 18

Martín Hötzel Escardó

Agda

July 20

Ulrik Buchholtz

HoTT

July 22

Dan Licata

Agda

July 25

Ulrik Buchholtz

HoTT

July 27

Dan Licata

Agda

July 29

Emily Riehl

HoTT

August 1

Emily Riehl

HoTT

August 3

Dan Licata

Agda

August 5

Emily Riehl

HoTT

August 8

Anders Mörtberg

Agda

August 10

Egbert Rijke

HoTT

August 12

Anders Mörtberg

Agda

August 15

Egbert Rijke

HoTT

August 17

Anders Mörtberg

Agda

August 19

Egbert Rijke

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