Skip to main content
To KTH's start page To KTH's start page

Felix Cherubini: Formalization of synthetic geometry

Time: Wed 2022-05-04 10.00 - 12.00

Location: Kräftriket, House 5, Room 31

Participating: Felix Cherubini (Chalmers University of Technology)

Export to calendar


With this talk, I would like to provide an overview of past and ongoing efforts to formalize parts of modern pure mathematics in (modal) homotopy type theory. The general idea is to use type theories as internal languages of toposes, which sometimes requires modalities to introduce relations of toposes into type theory. While it is not known, if there is a cubical type theory that admits interpretation in arbitrary toposes, those type theories are still interesting, since they provide at least some means of checking arguments involving more complicated higher inductive types. I will focus on more recent efforts to make a formalization of synthetic algebraic geometry possible with the cubical agda library.