2022/12/22 by Taichi Uemura, Uemura, Taichi · 1 citation
Mathematics · #03B38 (Primary) 18N60 (Secondary) #Advanced Topology and Set Theory #Algebraic structures and combinatorial models #Category Theory (math.CT) #F.3.2 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · pdf · doi:10.48550/arxiv.2212.11764
openalex publication_date 2022/12/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 0-truncated. The coherence theorem justifies interpreting an ordinary type theory in (∞, 1)-categorical structures.