Modal descent

DOI10.1017/S0960129520000201MaRDI QIDQ5022924zbMATH OpenFDO

Authors Felix Cherubini, Egbert Rijke

Publication date 20 January 2022

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

algebraic geometrycohesive homotopy type theoryfactorization systemshomotopy type theorymodal homotopy type theory

Mathematics Subject Classification ID

Classical first-order logic (03B10) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Abstract: Any modality in homotopy type theory gives rise to an orthogonal factorization system of which the left class is stable under pullbacks. We show that there is a second orthogonal factorization system associated to any modality, of which the left class is the class of $$-equivalences and the right class is the class of $$-'etale maps. This factorization system is called the reflective factorization system of a modality, and we give a precise characterization of the orthogonal factorization systems that arise as the reflective factorization system of a modality. In the special case of the $n$-truncation the reflective factorization system has a simple description: we show that the $n$-'etale maps are the maps that are right orthogonal to the map $mathbf1omathbf{S}^{n+1}$. We use the $$-'etale maps to prove a modal descent theorem: a map with modal fibers into $$ is the same thing as a $$-'etale map into a type $X$. We conclude with an application to real-cohesive homotopy type theory and remarks how $$-'etale maps relate to the formally etale maps from algebraic geometry.

Recommendations

• Characterizations of modalities and lex modalities
• Modalities in homotopy type theory
• Comprehensive factorisation systems
• On localization and stabilization for factorization systems
• A generalized Blakers–Massey theorem

Cites work

• A generalized Blakers–Massey theorem
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Higher groups in homotopy type theory
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3914531 (Why is no real title available?)
• scientific article; zbMATH DE number 3572315 (Why is no real title available?)
• Localization in Homotopy Type Theory
• Modalities in homotopy type theory
• Quantum gauge field theory in cohesive homotopy type theory
• Éléments de géométrie algébrique. I: Le langage des schémas. II: Étude globale élémentaire de quelques classe de morphismes. III: Étude cohomologique des faisceaux cohérents (première partie)
• Éléments de géométrie algébrique. IV: Étude locale des schémas et des morphismes de schémas (Quatrième partie). Rédigé avec la colloboration de J. Dieudonné

Cited in

(8)

• Characterizations of modalities and lex modalities
• scientific article; zbMATH DE number 6385415 (Why is no real title available?)
• Modal Ecthesis
• Good fibrations through the modal prism
• Topological quantum gates in homotopy type theory
• Modal fracture of higher groups
• The quantum monadology
• Synthetic G-jet-structures in modal homotopy type theory

This page was built for publication: Modal descent

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