Univalence for inverse diagrams and homotopy canonicity

DOI10.1017/S0960129514000565MaRDI QIDQ5740656zbMATHWikidataFDO

Authors Michael Shulman

Publication date 27 July 2016

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

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

Mathematics Subject Classification ID

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

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.

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

Cites work

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

Cited in

(51)

• An electrical engineering perspective on naturality in computational physics
• Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
• Normalization for multimodal type theory
• Adjoint logic with a 2-category of modes
• On notions of compactness, object classifiers, and weak Tarski universes
• Univalent categories of modules
• Two-level type theory and applications
• Univalence in locally Cartesian closed categories
• Fibred fibration categories
• Univalent completion
• The homotopy theory of type theories
• Model structures on categories of models of type theories
• Internal languages of finitely complete \((\infty , 1)\)-categories
• Modalities in homotopy type theory
• Univalence and completeness of Segal objects
• Univalence for inverse EI diagrams
• Partial univalence in \(n\)-truncated type theory
• Topological quantum gates in homotopy type theory
• Homotopical inverse diagrams in categories with attributes
• scientific article; zbMATH DE number 7559277 (Why is no real title available?)
• Canonicity and normalization for dependent type theory
• On a model invariance problem in homotopy type theory
• A characterisation of elementary fibrations
• Internal parametricity for cubical type theory
• Homotopical patch theory
• Canonicity and homotopy canonicity for cubical type theory
• A homotopy-theoretic model of function extensionality in the effective topos
• The local universes model: an overlooked coherence construction for dependent type theories
• Pointers in Recursion: Exploring the Tropics
• The Hurewicz theorem in homotopy type theory
• Multimodal dependent type theory
• Univalent polymorphism
• Simplicial sets inside cubical sets
• On Small Types in Univalent Foundations
• scientific article; zbMATH DE number 5002267 (Why is no real title available?)
• scientific article; zbMATH DE number 7559297 (Why is no real title available?)
• Constructive sheaf models of type theory
• The Interpretation Lifting Theorem for C-Systems
• Natural models of homotopy type theory
• The univalence axiom for elegant Reedy presheaves
• The simplicial model of univalent foundations (after Voevodsky)
• A model of guarded recursion with clock synchronisation
• A model for the higher category of higher categories
• Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)
• From cubes to twisted cubes via graph morphisms in type theory
• Towards a constructive simplicial model of Univalent Foundations
• Injective types in univalent mathematics
• Internal universes in models of homotopy type theory
• Semantics of higher inductive types
• Identity types and weak factorization systems in Cauchy complete categories

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)