Normalization and coherence for $\infty$-type theories
Logic
2022-12-23 v1 Logic in Computer Science
Category Theory
Abstract
We develop a technique for normalization for -type theories. The normalization property helps us to prove a coherence theorem: the initial model of a given -type theory is -truncated. The coherence theorem justifies interpreting an ordinary type theory in -categorical structures.
Cite
@article{arxiv.2212.11764,
title = {Normalization and coherence for $\infty$-type theories},
author = {Taichi Uemura},
journal= {arXiv preprint arXiv:2212.11764},
year = {2022}
}