Univalence for inverse diagrams and homotopy canonicity

DOI10.1017/S0960129514000565zbMath1362.03008arXiv1203.3253WikidataQ59757174 ScholiaQ59757174MaRDI QIDQ5740656

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)

Related Items (38)

Modalities in homotopy type theory ⋮ Adjoint Logic with a 2-Category of Modes ⋮ A characterisation of elementary fibrations ⋮ Homotopical patch theory ⋮ Univalent completion ⋮ Constructive sheaf models of type theory ⋮ Internal languages of finitely complete \((\infty , 1)\)-categories ⋮ Canonicity and normalization for dependent type theory ⋮ The Hurewicz theorem in homotopy type theory ⋮ On a model invariance problem in homotopy type theory ⋮ The Local Universes Model ⋮ Identity types and weak factorization systems in Cauchy complete categories ⋮ The Interpretation Lifting Theorem for C-Systems ⋮ 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 ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ Homotopical inverse diagrams in categories with attributes ⋮ Unnamed Item ⋮ A model of guarded recursion with clock synchronisation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Injective types in univalent mathematics ⋮ Exact completion of path categories and algebraic set theory. I: Exact completion of path categories ⋮ Univalence in locally Cartesian closed categories ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The homotopy theory of type theories ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ Semantics of higher inductive types ⋮ Model structures on categories of models of type theories ⋮ Pointers in Recursion: Exploring the Tropics ⋮ A homotopy-theoretic model of function extensionality in the effective topos ⋮ Unnamed Item ⋮ Univalence and completeness of Segal objects

Cites Work

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

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