Modalities in homotopy type theory

zbMATH Open1489.03005arXiv1706.07526MaRDI QIDQ5208873FDOQ5208873

Authors: Egbert Rijke, Michael Shulman, Bas Spitters 

Publication date: 22 January 2020

Abstract: Univalent homotopy type theory (HoTT) may be seen as a language for the category of $infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a "localization" higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.

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

Recommendations

• Homotopy-theoretic models of type theory
• The homotopy theory of type theories
• Homotopy type theory
• Homotopy Type Theory
• Type theory and homotopy
• Natural models of homotopy type theory
• Fibrational modal type theory
• Higher Structures in Homotopy Type Theory
• Homotopy type theory and the formalization of mathematics
• Homotopy Type Theory in Isabelle

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)

Cites Work

• On localization and stabilization for factorization systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Higher Topos Theory (AM-170)
• Notions of computation and monads
• More concise algebraic topology. Localization, completion, and model categories
• Univalence in locally Cartesian closed categories
• Contextual modal type theory
• Introduction to extensive and distributive categories
• Homotopy type theory. Univalent foundations of mathematics
• Implications of large-cardinal principles in homotopical localization
• Cover semantics for quantified lax logic
• The simplicial model of univalent foundations (after Voevodsky)
• The local universes model: an overlooked coherence construction for dependent type theories
• Univalence for inverse diagrams and homotopy canonicity
• The univalence axiom for elegant Reedy presheaves
• Semantics of higher inductive types
• Univalence for inverse EI diagrams
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Fibrational modal type theory
• Propositions as [Types]
• Locally Cartesian closed quasi-categories from type theory
• Higher homotopies in a hierarchy of univalent universes
• Eilenberg-MacLane spaces in homotopy type theory
• Sets in homotopy type theory
• The real projective spaces in homotopy type theory
• Partiality, Revisited
• Bousfield localization and the Hasse square
• Iterated algebraic injectivity and the faithfulness conjecture
• A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory
• The independence of Markov's principle in type theory

Cited In (35)

• $L'$-localization in an $\infty$-topos
• Non-accessible localizations
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• Title not available (Why is that?)
• The long exact sequence of homotopy n-groups
• Characterizations of modalities and lex modalities
• Topological quantum gates in homotopy type theory
• Nilpotent types and fracture squares in homotopy type theory
• Homotopy type theory: the logic of space
• Semantics of higher inductive types
• Left-exact localizations of \(\infty\)-topoi. II: Grothendieck topologies
• Adjoint logic with a 2-category of modes
• Good fibrations through the modal prism
• Modal fracture of higher groups
• Homotopy type theory as internal languages of diagrams of \(\infty\)-logoses
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Sets in homotopy type theory
• Homotopy type theory. Univalent foundations of mathematics
• Higher Structures in Homotopy Type Theory
• On Church’s thesis in cubical assemblies
• Indexed type theories
• Precovers, Modalities and Universal Closure Operators in a Topos
• Curry-Howard-Lambek correspondence for intuitionistic belief
• Modal descent
• Normalization for multimodal type theory
• Modal Homotopy Type Theory
• Localization in Homotopy Type Theory
• Synthetic fibered \((\infty,1)\)-category theory
• Modal dependent type theory and dependent right adjoints
• Constructive sheaf models of type theory
• Left-exact localizations of \(\infty\)-topoi. I: Higher sheaves
• Internal universes in models of homotopy type theory
• Multimodal dependent type theory
• Modular types in some supersimple theories
• The compatibility of the minimalist foundation with homotopy type theory

This page was built for publication: Modalities in homotopy type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5208873)