Eric Finster: Left Exact Modalities in Type Theory
Time: Wed 2019-04-24 10.00 - 11.45
Lecturer: Eric Finster
Location: Room 16, building 5, Kräftriket, Department of Mathematics, Stockholm University
Abstract: In ordinary topos theory, one can encode the notion of a subtopos as a Lawvere-Tierney topology on the sub-object classifier. Viewing homotopy type theory as an internal language, this time for higher toposes, the natural replacement for such a topology is a modality on the universe of types. But whereas the localization associated to a Lawvere-Tierney topology always preserves finite limits and thus determines a subtopos, this fails to be the case in general in type theory (the n-trucation modalities provide a simple class of counterexamples). Those modalities which do in fact preserve finite limits, and thus determine a subtopos, are called left exact.
In this talk, I will discuss the problem of lex modalities in type theory and exhibit a criterion which allows us to detect when modalities do indeed generate sub-toposes, as well provides us with tools to generate such modalities. Time permitting, I will explain how every left exact modality generates and infinite tower of associated modalities and describe some properties of this tower.