[HoTT] HoTTEST summer school colloquia

["'EMILY RIEHL' via Homotopy Type Theory" <HomotopyTypeTheory@googlegroups.com>]

This week and next, we are looking forward to five colloquium talks that will conclude this summer's HoTTEST Summer School. The talks will take place on Mondays, Wednesdays, and Fridays, starting tomorrow and concluding at the end of the month, from 2:30-4 PM UTC, at the following link:

https://zoom.us/j/99263826765

All are welcome.

Our speakers are Jon Sterling, Pierre Cagne, Jonas Frey, Favonia, and Chaitanya Leena Subramaniam. Titles and abstracts appear below. Hope to see you there!

Monday 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.

Wednesday 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 knowledgeable 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).

Friday 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.

Monday 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.

Wednesday August 31: Chaitanya Leena Subramaniam, TBD

---
Professor of Mathematics (she/her)
Johns Hopkins University
emilyriehl.github.io

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/DS7PR01MB7758EDA9277BB98584EBF5EFC8719%40DS7PR01MB7758.prod.exchangelabs.com.