Skip to main content

Taichi Uemura: Cubical assemblies models of type theory

Time: Wed 2023-02-15 10.00 - 12.00

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

Participating: Taichi Uemura, Stockholm University

Export to calendar

Abstract

The assemblies model of type theory has an impredicative universe and satisfies principles of constructive recursive mathematics. The cubical assemblies, cubical objects in the assemblies model, form a model of type theory which is naturally expected to have an impredicative and univalent universe and satisfy principles of constructive recursive mathematics.

In this talk, we will study the cubical assemblies model and related models. The cubical assemblies model DOES have an impredicative and univalent universe. This universe does NOT admit propositional resizing. The cubical assemblies model does NOT satisfy Church's thesis, one of the most important principles of constructive recursive mathematics. A localization of the cubical assemblies model DOES satisfy Church's thesis. Another localization of the cubical assemblies model DOES satisfy a version of extended Church's thesis.

Most part of this talk is about earlier work of Andrew Swan and myself. The result on extended Church's thesis has recently been shown by Swan (arXiv:2209.15035).