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