Normalization and coherence for \infty-type theories

arXiv2212.11764MaRDI QIDQ6421391FDOQ6421391

Authors: Taichi Uemura 

Publication date: 22 December 2022

Abstract: We develop a technique for normalization for $infty$-type theories. The normalization property helps us to prove a coherence theorem: the initial model of a given $infty$-type theory is $0$-truncated. The coherence theorem justifies interpreting an ordinary type theory in $(infty,1)$-categorical structures.

Mathematics Subject Classification ID

Type theory (03B38) ((infty,1))-categories (quasi-categories, Segal spaces, etc.); (infty)-topoi, stable (infty)-categories (18N60)

This page was built for publication: Normalization and coherence for $\infty$-type theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6421391)