Taichi Uemura: Higher dimensional normalization

Abstract

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. https://arxiv.org/abs/2106.01414
[3] R. Bocquet, A. Kaposi, and C. Sattler. Relative induction principles for type theories. https://arxiv.org/abs/2102.11649