Univalence for inverse diagrams and homotopy canonicity

DOI10.1017/S0960129514000565MaRDI QIDQ5740656zbMATH OpenWikidataFDO

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

• 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
• scientific article; zbMATH DE number 1226952 (Why is no real title available?)
• scientific article; zbMATH DE number 1860105 (Why is no real title available?)
• 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 -groupoids
• Uncomplemented C(X)-Subalgebras of C(X)

Cited in

(58)

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

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)