2012/03/31 by Michael Shulman, MICHAEL SHULMAN · 48 citations
Computer Science · Mathematics · #Advanced Topology and Set Theory #Cofibration #Diagram #Functor #Homotopy #Homotopy and Cohomology in Algebraic Topology #Inverse #Logic, programming, and type systems #Type (biology) #Type theory #math.CT #msc:18C50
paper · pdf · doi:10.1017/s0960129514000565
published in Mathematical Structures in Computer Science 25(5), 1203-1277 (Cambridge University Press (CUP)) · 70 pages. v2: greatly expanded and largely rewritten, with more detailed proofs, and new applications to gluing and a partial solution to Voevodsky's homotopy canonicity conjecture. v3: small changes and fixes, final version to appear in MSCS
arxiv created 2013/11/18 · crossref issued 2014/11/24 · crossref published 2014/11/24 · crossref published-online 2014/11/24 · openalex publication_date 2014/11/24 · crossref created 2014/11/26 · crossref published-print 2015/06/01 · openalex created_date 2016/06/24 · arxiv updated 2019/02/20 · crossref deposited 2019/08/17 · crossref indexed 2026/08/06 · openalex updated_date 2026/08/06
We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (∞, 1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.