Seminar

Friday, June 4th, 2021, 11:00, on Zoom.

Roberta Bonacina (Tübingen)
Two-level type theory

Abstract:

Homotopy type theory (HoTT) extends Martin-Löf type theory with the univalence axiom, which establishes a tight connection between types and homotopy spaces and allows to identify isomorphic objects. Univalence has very useful applications, but it has also drawbacks: properties that are not invariant under homotopy cannot be expressed internally. An important case is the concept of semisimplicial types, whose definition is so far elusive in HoTT. Two-level type theory (2LTT) is a formal theory which allows constructions that require access to non-homotopy-invariant notions. It is composed of two separate levels of types related by a conversion function that preserves context extensions; the outer level is Martin-Löf type theory plus the uniqueness of identity proofs, and the inner level is HoTT. In this talk we will discuss the consequences of univalence, and introduce 2LTT as a way to overcome some difficulties. Then, we will introduce the notion of model for this system, and define the syntactical category as a first step to prove an initiality result for the syntax of 2LTT. The last part of the talk is based on a joint work-in-progress with Benedikt Ahrens and Nicolai Kraus.

The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster or Giulio Fellin.