Errol Yuksel: Classical sets for simplicial type theorists
Time: Tue 2021-08-24 13.30 - 14.30
Respondent: Errol Yuksel
Abstract: In recent years, Homotopy Type Theory (HoTT) has emerged as an alternative formal system for mathematics, capable of expressing highly classical concepts such as homotopy theory in a type-theoretical syntax close to those found in computer science. This formal system was based in part on what is now its most archetypal model, the simplicial model; built in the category of simplicial sets, this model is topologically flavoured: its basic objects can be seen as spaces for instance.
Accordingly, elements of the universe of discourse of HoTT can be understood as abstract spaces, thus the notion of set can be encoded in the theory as an “abstract discrete space”. The present work aims to show that properties of classical sets are preserved when those sets are interpreted as discrete spaces in the simplicial model. While the approach taken is specific to the model at hand, it lays the foundations for a more general framework which could be used in the future to answer similar questions for different models.
A notable obstruction lies with a notion needed to interpret classical existence in HoTT, propositional truncation, as it is not part of the original construction of the simplicial model. As a result, this work comprises an account of the method one can employ to truncate types down to strict propositions in the simplicial model using image factorisations.