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

Taichi Uemura: Higher dimensional normalization

Time: Wed 2022-02-23 10.00 - 12.00

Location: Kräftriket, House 5, Room 31

Participating: Taichi Uemura (Stockholm University)

Export to calendar


We develop a normalization technique for the initial space-valued model of a type theory. A consequence is that the initial space-valued model coincides with the initial set-valued model of the type theory, which allows us to interpret the type theory in higher dimensional structures.

In the talk, we first review recent development of synthetic normalization proof such as [1–3] and then discuss how to generalize it to the higher dimensional setting.

[1] J. Sterling and C. Angiuli. Normalization for cubical type theory. LICS 2021. doi:10.1109/LICS52264.2021.9470719
[2] D. Gratzer. Normalization for multimodal type theory.
[3] R. Bocquet, A. Kaposi, and C. Sattler. Relative induction principles for type theories.