| Title:
|
Good Fibrations through the Modal Prism (English) |
| Author:
|
Myers, David Jaz |
| Language:
|
English |
| Journal:
|
Higher Structures |
| ISSN:
|
2209-0606 |
| Volume:
|
6 |
| Issue:
|
1 |
| Year:
|
2022 |
| Pages:
|
212-255 |
| Summary lang:
|
English |
| . |
| Category:
|
math |
| . |
| Summary:
|
Homotopy type theory is a formal language for doing abstract homotopy theory — the study of identifications. But in unmodified homotopy type theory, there is no way to say that these identifications come from identifying the path-connected points of a space. In other words, we can do abstract homotopy theory, but not algebraic topology. Shulman’s {\it Real Cohesive HoTT} remedies this issue by introducing a system of modalities that relate the spatial structure of types to their homotopical structure. In this paper, we develop a theory of {\it modal fibrations} for a general modality, and apply it in particular to the shape modality of real cohesion. We then give examples of modal fibrations in Real Cohesive HoTT, and develop the theory of covering spaces. (English) |
| Keyword:
|
Homotopy Type Theory |
| Keyword:
|
Modality |
| Keyword:
|
Fibration |
| Keyword:
|
Axiomatic Cohesion |
| MSC:
|
55U35 |
| idZBL:
|
Zbl 1502.18047 |
| idMR:
|
MR4456595 |
| DOI:
|
10.21136/HS.2022.04 |
| . |
| Date available:
|
2026-03-13T09:57:18Z |
| Last updated:
|
2026-03-13 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/153448 |
| . |
| Reference:
|
[1] Anel, M., Biedermann, G., Finster, E., Joyal, A.: Goodwillie’s calculus of functors and higher topos theory.Journal of Topology, Vol. 11, Iss. 4, 1100-1132, http://dx.doi.org/10.1112/topo.12082, DOI:10.1112/topo.12082 MR 3989439, 10.1112/topo.12082 |
| Reference:
|
[2] Anel, Mathieu, Biedermann, Georg, Finster, Eric, Joyal, André: A generalized blakers-massey theorem. |
| Reference:
|
[3] Buchholtz, Ulrik, Doorn, Floris, Rijke, Egbert: Higher groups in homotopy type theory. |
| Reference:
|
[4] Cherubini, Felix, Rijke, Egbert: Modal descent.Mathematical Structures in Computer Science, 1-29, http://dx.doi.org/10.1017/S0960129520000201, DOI:10.1017/s0960129520000201 MR 4368346, 10.1017/s0960129520000201 |
| Reference:
|
[5] Christensen, J. Daniel, Opie, Morgan, Rijke, Egbert, Scoccola, Luis: Localization in Homotopy Type Theory.arXiv e-prints MR 4074272 |
| Reference:
|
[6] Dold, Albrecht, Thom, Rene: Quasifaserungen und unendliche symmetrische produkte.Annals of Mathematics, Vol. 67, Iss. 2, 239-281, http://www.jstor.org/stable/1970005 10.2307/1970005 |
| Reference:
|
[7] Goodwillie, Tom: Quasifibrations.Email to ALGTOP mailing list |
| Reference:
|
[8] Rijke, Egbert: Classifying types: Topics in synthetic homotopy theory.PhD thesis, Carnegie Mellon University |
| Reference:
|
[9] Rijke, Egbert, Shulman, Michael, Spitters, Bas: Modalities in homotopy type theory.arXiv e-prints MR 4054355 |
| Reference:
|
[10] Schreiber, Urs: Differential cohomology in a cohesive infinity-topos. |
| Reference:
|
[11] Shulman, Michael: All (\infty,1)-toposes have strict univalent universes. |
| Reference:
|
[12] Shulman, Michael: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory.Mathematical Structures in Computer Science, Vol. 28, Iss. 6, 856-941, DOI:10.1017/S0960129517000147 MR 3798599, 10.1017/S0960129517000147 |
| Reference:
|
[13] Univalent Foundations Program, The: Homotopy type theory: Univalent foundations of mathematics.https://homotopytypetheory.org/book MR 3204653 |
| Reference:
|
[14] Wellen, Felix: Cohesive covering theory.Proceedings of HoTT/UF 2018 |
| Reference:
|
[15] Wellen, Felix: Formalizing cartan geometry in modal homotopy type theory.PhD thesis, Karlsruher Institut für Technologie |
| . |
