Normalization and coherence for $\mathrm{\infty }$-type theories

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