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

Taichi Uemura: Homotopy type theory as an internal language of a diagram of infinity logoses

Time: Wed 2022-10-05 10.00 - 12.00

Location: Albano house 1, floor 3, Room U (Kovalevsky)

Participating: Taichi Uemura (Stockholm University)

Export to calendar


*Homotopy type theory* is an internal language of an *∞-logos* (aka ∞-topos). But ∞-logoses are often connected by functors and natural transformations. Homotopy type theory is, at first sight, not sufficiently rich to reason about such a *diagram* of ∞-logoses, because the actions of functors and natural transformations are not internalized. Extending homotopy type theory with non-internal modalities could be one solution, but it would cause coherence problems for not only ∞-logoses but also functors and natural transformations.

In this talk, we consider using *plain* homotopy type theory in some way to reason about a diagram of ∞-logoses. We show that some kind of diagram of ∞-logoses is reconstructed internally to its *oplax limit* via *internal modalities*. Then plain homotopy type theory as internal language of the oplax limit can be used for reasoning about the original diagram.

The first half of the talk will be an introduction to modalities in type theory (Rijke, Shulman, and Spitters 2020 <>). In the second half, I will explain what kind of diagrams of ∞-logoses can be internally expressed using modalities.

A short note is at <>.