Modalities in homotopy type theory

zbMath1489.03005arXiv1706.07526MaRDI QIDQ5208873

Michael Shulman, Bas Spitters, Egbert Rijke

Publication date: 22 January 2020

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

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Related Items

Left-exact localizations of \(\infty\)-topoi. I: Higher sheaves ⋮ Localization in Homotopy Type Theory ⋮ $L'$-localization in an $\infty$-topos ⋮ On Church’s thesis in cubical assemblies ⋮ Constructive sheaf models of type theory ⋮ Left-exact localizations of \(\infty\)-topoi. II: Grothendieck topologies ⋮ The long exact sequence of homotopy n-groups ⋮ Unnamed Item ⋮ Nilpotent types and fracture squares in homotopy type theory ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Characterizations of modalities and lex modalities ⋮ Indexed type theories ⋮ Good Fibrations through the Modal Prism ⋮ Semantics of higher inductive types ⋮ Unnamed Item ⋮ Modal dependent type theory and dependent right adjoints ⋮ Curry-Howard-Lambek correspondence for intuitionistic belief ⋮ Unnamed Item ⋮ Modal descent

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Univalence in locally Cartesian closed categories
• Notions of computation and monads
• Introduction to extensive and distributive categories
• On localization and stabilization for factorization systems
• Univalence for inverse EI diagrams
• Fibrational modal type theory
• The simplicial model of univalent foundations (after Voevodsky)
• Implications of large-cardinal principles in homotopical localization
• Higher Homotopies in a Hierarchy of Univalent Universes
• The Local Universes Model
• Partiality, Revisited
• Cover semantics for quantified lax logic
• Locally cartesian closed quasi‐categories from type theory
• Bousfield localization and the Hasse square
• Eilenberg-MacLane spaces in homotopy type theory
• A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Propositions as [Types]
• Semantics of higher inductive types
• The real projective spaces in homotopy type theory
• Iterated algebraic injectivity and the faithfulness conjecture
• Contextual modal type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Higher Topos Theory (AM-170)
• Sets in homotopy type theory
• Univalence for inverse diagrams and homotopy canonicity
• The univalence axiom for elegant Reedy presheaves