Modalities in homotopy type theory

MaRDI QIDQ5208873zbMATH OpenFDO

Authors Egbert Rijke, Michael Shulman, Bas Spitters

Publication date 22 January 2020

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

Mathematics Subject Classification ID

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

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.

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

Cites work

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

Cited in

(49)

• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• Curry-Howard-Lambek correspondence for intuitionistic belief
• Left-exact localizations of \(\infty\)-topoi. I: Higher sheaves
• Characterizations of modalities and lex modalities
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Modular types in some supersimple theories
• Precovers, Modalities and Universal Closure Operators in a Topos
• Semantics of higher inductive types
• Internal universes in models of homotopy type theory
• Modal descent
• On Church’s thesis in cubical assemblies
• Constructive sheaf models of type theory
• Good fibrations through the modal prism
• Dual-context calculi for modal logic
• Nilpotent types and fracture squares in homotopy type theory
• Multimodal dependent type theory
• Indexed type theories
• Homotopy type theory: the logic of space
• Modal Homotopy Type Theory
• Localization in Homotopy Type Theory
• $L'$-localization in an $\infty$-topos
• Modal dependent type theory and dependent right adjoints
• Adjoint logic with a 2-category of modes
• Homotopy type theory. Univalent foundations of mathematics
• Sets in homotopy type theory
• Left-exact localizations of -topoi. II: Grothendieck topologies
• Higher Structures in Homotopy Type Theory
• The compatibility of the minimalist foundation with homotopy type theory
• The long exact sequence of homotopy n-groups
• Synthetic fibered (,1)-category theory
• Non-accessible localizations
• Topological quantum gates in homotopy type theory
• Modal fracture of higher groups
• Homotopy type theory as internal languages of diagrams of -logoses
• Normalization for multimodal type theory
• Normalization for multimodal type theory
• Homotopy type theory as a language for diagrams of -logoses
• Towards univalent reference types: the impact of univalence on denotational semantics
• Exponentiable functors between synthetic -categories
• Toward a geometry for syntax
• The quantum monadology
• ``Upon this quote I will build my Church thesis
• (, 1)-categorical comprehension schemes
• Smooth and proper maps with respect to a fibration
• Synthetic G-jet-structures in modal homotopy type theory
• Strict universes for Grothendieck topoi
• Coslice colimits in homotopy type theory
• A foundation for synthetic Stone duality
• Left-exact localizations of -topoi. III: The acyclic product

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)