Normalization and coherence for $\infty$-type theories

TL;DR

This paper introduces a normalization technique for $ abla$-type theories, enabling the proof of a coherence theorem that connects $ abla$-type theories with $( abla, 1)$-categorical structures.

Contribution

It develops a normalization method for $ abla$-type theories and proves a coherence theorem linking initial models to $( abla, 1)$-categories.

Findings

Normalization technique for $ abla$-type theories

Proof that initial models are $0$-truncated

Supports interpretation of type theories in $( abla, 1)$-categories

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.