Univalence for inverse diagrams and homotopy canonicity

DOI10.1017/S0960129514000565zbMATH Open1362.03008arXiv1203.3253WikidataQ59757174 ScholiaQ59757174MaRDI QIDQ5740656FDOQ5740656

Michael Shulman

Publication date: 27 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Abstract: 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 (infinity,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.

Full work available at URL: https://arxiv.org/abs/1203.3253

Recommendations

• Path categories and propositional identity types
• The univalence axiom for elegant Reedy presheaves
• The simplicial model of univalent foundations (after Voevodsky)
• On a model invariance problem in homotopy type theory
• Axioms for modelling cubical type theory in a topos
• Homotopy type theory
• scientific article; zbMATH DE number 7003193
• Natural models of homotopy type theory
• Topological and simplicial models of identity types

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Categorical logic and type theory
• Homotopical algebra
• The homotopy category is a homotopy category
• Higher Topos Theory (AM-170)
• Generalized algebraic theories and contextual categories
• Types are weak ω -groupoids
• Homotopy theoretic models of identity types
• The identity type weak factorisation system
• On an extension of the notion of Reedy category
• Reedy categories and the \(\varTheta\)-construction
• Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview
• Combinatorial realizability models of type theory
• Théories homotopiques dans les topos. (Homotopy theories in topoi)
• Finitely generated free Heyting algebras
• A coherence theorem for Martin-Löf's type theory
• On the construction of functorial factorizations for model categories
• Uncomplemented C(X)-Subalgebras of C(X)

Cited In (45)

• The homotopy theory of type theories
• A characterisation of elementary fibrations
• On Small Types in Univalent Foundations
• Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
• Adjoint Logic with a 2-Category of Modes
• Canonicity and homotopy canonicity for cubical type theory
• On notions of compactness, object classifiers, and weak Tarski universes
• Univalent categories of modules
• Two-level type theory and applications
• Title not available (Why is that?)
• Univalence in locally Cartesian closed categories
• Topological quantum gates in homotopy type theory
• A homotopy-theoretic model of function extensionality in the effective topos
• The simplicial model of univalent foundations (after Voevodsky)
• Identity types and weak factorization systems in Cauchy complete categories
• Semantics of higher inductive types
• Univalence and completeness of Segal objects
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
• Homotopical patch theory
• An electrical engineering perspective on naturality in computational physics
• Univalent completion
• The Local Universes Model
• The Interpretation Lifting Theorem for C-Systems
• Title not available (Why is that?)
• The Hurewicz theorem in homotopy type theory
• A model of guarded recursion with clock synchronisation
• Simplicial sets inside cubical sets
• Title not available (Why is that?)
• Towards a constructive simplicial model of Univalent Foundations
• Injective types in univalent mathematics
• Model structures on categories of models of type theories
• Normalization for multimodal type theory
• Univalence for inverse EI diagrams
• Title not available (Why is that?)
• Modalities in homotopy type theory
• Constructive sheaf models of type theory
• Title not available (Why is that?)
• Canonicity and normalization for dependent type theory
• On a model invariance problem in homotopy type theory
• Internal languages of finitely complete \((\infty , 1)\)-categories
• Homotopical inverse diagrams in categories with attributes
• Pointers in Recursion: Exploring the Tropics

This page was built for publication: Univalence for inverse diagrams and homotopy canonicity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740656)