| Title:
|
Synthetic fibered $(\infty,1)$-category theory (English) |
| Author:
|
Buchholtz, Ulrik |
| Author:
|
Weinberger, Jonathan |
| Language:
|
English |
| Journal:
|
Higher Structures |
| ISSN:
|
2209-0606 |
| Volume:
|
7 |
| Issue:
|
1 |
| Year:
|
2023 |
| Pages:
|
74-165 |
| Summary lang:
|
English |
| . |
| Category:
|
math |
| . |
| Summary:
|
We study cocartesian fibrations in the setting of the synthetic $(\infty,1)$-category theory developed in simplicial type theory introduced by Riehl and Shulman. Our development culminates in a Yoneda Lemma for cocartesian fibrations. (English) |
| Keyword:
|
homotopy type theory |
| Keyword:
|
simplicial type theory |
| Keyword:
|
$(\infty,1)$-categories |
| Keyword:
|
Segal spaces |
| Keyword:
|
Rezk spaces |
| Keyword:
|
cartesian fibrations |
| MSC:
|
03B38 |
| MSC:
|
18D30 |
| MSC:
|
18D40 |
| MSC:
|
18D70 |
| MSC:
|
18N45 |
| MSC:
|
18N50 |
| MSC:
|
18N55 |
| MSC:
|
18N60 |
| MSC:
|
55U35 |
| idZBL:
|
Zbl 1535.18039 |
| idMR:
|
MR4600458 |
| DOI:
|
10.21136/HS.2023.04 |
| . |
| Date available:
|
2026-03-13T10:10:46Z |
| Last updated:
|
2026-03-13 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/153459 |
| . |
| Reference:
|
[1] Altenkirch, Thorsten, Sestini, Filipo: Naturality for free! — the category interpretation of directed type theory.https://hott.github.io/HoTT-2019//conf-slides/Sestini.pdf, Presentation at Homotopy Type Theory 2019, CMU MR 4352338 |
| Reference:
|
[2] Annenkov, Danil, Capriotti, Paolo, Kraus, Nicolai, Sattler, Christian: Two-level type theory and applications.https://arxiv.org/abs/1705.03307 MR 4695500 |
| Reference:
|
[3] Ayala, David, Francis, John: Fibrations of \infty-categories.Higher Structures, Vol. 4, Iss. 1, https://higher-structures.math.cas.cz/api/files/issues/Vol4Iss1/AyalaFrancis MR 4074276 |
| Reference:
|
[4] Bakke, Fredrik: Segal spaces in homotopy type theory.Master’s thesis, NTNU |
| Reference:
|
[5] Barwick, Clark, Dotto, Emanuele, Glasman, Saul, Nardin, Denis, Shah, Jay: Parametrized higher category theory and higher algebra: Exposé I – Elements of parametrized higher category theory.https://arxiv.org/abs/1608.03657 MR 3781930 |
| Reference:
|
[6] Barwick, Clark, Shah, Jay: Fibrations in \infty-category theory.2016 MATRIX annals, pages 17-42, MR 3792514 |
| Reference:
|
[7] Bergner, Julia E.: Adding inverses to diagrams. II: Invertible homotopy theories are spaces.Homology Homotopy Appl., Vol. 10, Iss. 2, 175-193, DOI:10.4310/HHA.2008.v10.n2.a9 MR 2475608, 10.4310/HHA.2008.v10.n2.a9 |
| Reference:
|
[8] Bergner, Julia E.: The homotopy theory of (\infty,1)-categories.Cambridge University Press, Volume 90, DOI:10.1017/9781316181874 MR 3791455, 10.1017/9781316181874 |
| Reference:
|
[9] Bezem, Marc, Buchholtz, Ulrik, Cagne, Pierre, Dundas, Bjørn, Grayson, Dan: Symmetry.https://github.com/UniMath/SymmetryBook |
| Reference:
|
[10] Li-Bland, David: The stack of higher internal categories and stacks of iterated spans.https://arxiv.org/abs/1506.08870 |
| Reference:
|
[11] Borceux, Francis: Handbook of categorical algebra: Volume 2, categories and structures.Cambridge University Press, Volume 2 |
| Reference:
|
[12] Bousfield, Aldridge K.: The simplicial homotopy theory of iterated loop spaces.Typed notes by Julie Bergner |
| Reference:
|
[13] Buchholtz, Ulrik: Higher structures in homotopy type theory.Reflections on the foundations of mathematics: Univalent foundations, set theory and general thoughts, pages 151-172, MR 4352340 |
| Reference:
|
[14] Capriotti, Paolo: Models of type theory with strict equality.PhD thesis, The University of Nottingham |
| Reference:
|
[15] Cavallo, Evan, Riehl, Emily, Sattler, Christian: On the directed univalence axiom.http://www.math.jhu.edu/~eriehl/JMM2018-directed-univalence.pdf, Talk at AMS Special Session on Homotopy Type Theory, Joint Mathematics Meething, San Diego |
| Reference:
|
[16] Cisinski, Denis-Charles: Higher categories and homotopical algebra.Cambridge studies in advanced mathematics, Cambridge University Press, DOI:10.1017/9781108588737 MR 3931682, 10.1017/9781108588737 |
| Reference:
|
[17] Cisinski, Denis-Charles: Univalent universes for elegant models of homotopy types.https://arxiv.org/abs/1406.0058 |
| Reference:
|
[18] Clementino, Maria Manuel, Nunes, Fernando Lucatelli: Lax comma 2-categories and admissible 2-functors.https://arxiv.org/abs/2002.03132 MR 4732696 |
| Reference:
|
[19] Cohen, Cyril, Coquand, Thierry, Huber, Simon, Mörtberg, Anders: Cubical type theory: A constructive interpretation of the univalence axiom.21st International Conference on Types for Proofs and Programs (TYPES 2015), pages , LIPIcs. Leibniz int. Proc. inform. MR 4542234 |
| Reference:
|
[20] Columbus, Tobias: 2-Categorical aspects of quasi-categories.PhD thesis, Karlsruher Institut für Technologie (KIT); Karlsruher Institut für Technologie (KIT) |
| Reference:
|
[21] Brito, Pedro Boavida: Segal objects and the Grothendieck construction.https://arxiv.org/abs/1605.00706 MR 3807750 |
| Reference:
|
[22] Gepner, David, Haugseng, Rune, Nikolaus, Thomas: Lax colimits and free fibrations in \infty-categories.Doc. Math., Vol. 22, 1225-1266, DOI:10.25537/dm.2017v22.1225-1266 MR 3690268, 10.25537/dm.2017v22.1225-1266 |
| Reference:
|
[23] Gray, John W.: Fibred and cofibred categories.Proceedings of the conference on categorical algebra, pp 21-83, DOI:https://doi.org/10.1007/978-3-642-99902-4_2 10.1007/978-3-642-99902-4_2 |
| Reference:
|
[24] Hackney, Philip, Ozornova, Viktoriya, Riehl, Emily, Rovelli, Martina: An (\infty,2)-categorical pasting theorem.https://arxiv.org/abs/2106.03660 MR 4510118 |
| Reference:
|
[25] Hermida, Claudio: On fibred adjunctions and completeness for fibred categories.Recent trends in data type specification, pages 235-251, |
| Reference:
|
[26] Johnson, Niles, Yau, Donald: A bicategorical pasting theorem.https://arxiv.org/abs/1910.01220 |
| Reference:
|
[27] Johnstone, P. T.: On a topological topos.Proc. London Math. Soc. (3), Vol. 38, Iss. 2, 237-271, DOI:10.1112/plms/s3-38.2.237 10.1112/plms/s3-38.2.237 |
| Reference:
|
[28] Joyal, André: Notes on quasi-categories.http://www.math.uchicago.edu/~may/IMA/Joyal.pdf |
| Reference:
|
[29] Joyal, André: Quasi-categories and Kan complexes.J. Pure Appl. Algebra, pages 207-222, 175 MR 1935979 |
| Reference:
|
[30] Joyal, André, Tierney, Myles: Quasi-categories vs Segal spaces.Contemporary Mathematics, Vol. 431, Iss. 277-326, 10 MR 2342834, 10.1090/conm/431/08278 |
| Reference:
|
[31] Kavvos, Alex: A quantum of direction.https://www.lambdabetaeta.eu/papers/meio.pdf, preprint |
| Reference:
|
[32] Kazhdan, David, Varshavsky, Yakov: Yoneda lemma for complete Segal spaces.Funct. Anal. Its Appl., Vol. 48, 81-106, DOI:10.1007/s10688-014-0050-3 MR 3288174, 10.1007/s10688-014-0050-3 |
| Reference:
|
[33] Kock, Anders, Kock, Joachim: Local fibred right adjoints are polynomial.Math. Struct. Comput. Sci., Vol. 23, Iss. 1, 131-141, DOI:10.1017/S0960129512000217 MR 3008196, 10.1017/S0960129512000217 |
| Reference:
|
[34] Kudasov, Nikolai: Rzk.https://github.com/fizruk/rzk, Prototype interactive proof assistant based on a type theory for synthetic \infty-categories |
| Reference:
|
[35] Licata, Dan: More fibrations.https://github.com/dlicata335/cart-cube/blob/master/agda/directed/moreFibs.agda, Agda Formalization |
| Reference:
|
[36] Licata, Daniel R., Harper, Robert: 2-dimensional directed type theory.Twenty-Seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII), pages 263-289, Electron. Notes theor. Comput. sci. 276 MR 2917360 |
| Reference:
|
[37] Lietz, Peter: A fibrational theory of geometric morphisms.Diploma thesis, TU Darmstadt |
| Reference:
|
[38] Lurie, Jacob: (\infty, 2)-Categories and the Goodwillie Calculus I.https://arxiv.org/abs/0905.0462 |
| Reference:
|
[39] Lurie, Jacob: Higher topos theory.Annals of mathematics studies 170, Princeton University Press, https://arxiv.org/abs/math/0608040, DOI:10.1515/9781400830558 10.1515/9781400830558 |
| Reference:
|
[40] Martínez, César Bardomiano: Limits and colimits of synthetic \infty-categories.https://arxiv.org/abs/2202.12386 MR 4963152 |
| Reference:
|
[41] Martini, Louis: Cocartesian fibrations and straightening internal to an \infty-topos.https://arxiv.org/abs/2204.00295 |
| Reference:
|
[42] Martini, Louis: Yoneda’s lemma for internal higher categoriess.https://arxiv.org/abs/2103.17141 |
| Reference:
|
[43] Martini, Louis, Wolf, Sebastian: Limits and colimits in internal higher category theory.https://arxiv.org/abs/2111.14495 MR 4752519 |
| Reference:
|
[44] Mazel-Gee, Aaron: A user’s guide to co/cartesian fibrations.https://arxiv.org/abs/1510.02402 MR 3999274 |
| Reference:
|
[45] Moens, Jean-Luc: Caracterisation des topos de faisceaux sur un site interne à un topos.PhD thesis, UCL-Université Catholique de Louvain |
| Reference:
|
[46] Nguyen, Hoang Kim: Theorems in higher category theory and applications.PhD thesis, Universität Regensburg |
| Reference:
|
[47] North, Paige Randall: Towards a directed homotopy type theory.Electronic Notes in Theoretical Computer Science, Vol. 347, 223-239, DOI:https://doi.org/10.1016/j.entcs.2019.09.012 MR 4043275, 10.1016/j.entcs.2019.09.012 |
| Reference:
|
[48] Nuyts, Andreas: Contributions to multimode and presheaf type theory.PhD thesis, KU Leuven |
| Reference:
|
[49] Nuyts, Andreas: Towards a directed homotopy type theory based on 4 kinds of variance.Master’s thesis, KU Leuven |
| Reference:
|
[50] Paoli, Simona: Simplicial Methods for Higher Categories: Segal-type Models of Weak n-Categories.Springer, Volume 26, DOI:10.1007/978-3-030-05674-2 MR 3932125, 10.1007/978-3-030-05674-2 |
| Reference:
|
[51] Rasekh, Nima: A Model for the Higher Category of Higher Categories.https://arxiv.org/abs/1805.03816 MR 4695986 |
| Reference:
|
[52] Rasekh, Nima: Cartesian fibrations and representability.https://arxiv.org/abs/1711.03670 MR 4467022 |
| Reference:
|
[53] Rasekh, Nima: Cartesian fibrations of complete segal spaces.https://arxiv.org/abs/2102.05190 MR 4600457 |
| Reference:
|
[54] Rasekh, Nima: Quasi-categories vs. Segal spaces: Cartesian edition.J. Homotopy Relat. Struct., Vol. 16, Iss. 4, 563-604, DOI:10.1007/s40062-021-00288-2 MR 4343074, 10.1007/s40062-021-00288-2 |
| Reference:
|
[55] Rasekh, Nima: Univalence in higher category theory.https://arxiv.org/abs/2103.12762 |
| Reference:
|
[56] Rasekh, Nima: Yoneda lemma for \mathcal{D}-simplicial spaces.https://arxiv.org/abs/2108.06168 MR 4616631 |
| Reference:
|
[57] Rasekh, Nima: Yoneda lemma for simplicial spaces.https://arxiv.org/abs/1711.03160 MR 4616631 |
| Reference:
|
[58] Rezk, Charles: A model for the homotopy theory of homotopy theory.Trans. Amer. Math. Soc., Vol. 353, Iss. 3, 973-1007, DOI:10.1090/S0002-9947-00-02653-2 MR 1804411, 10.1090/S0002-9947-00-02653-2 |
| Reference:
|
[59] Rezk, Charles: Stuff about quasicategories.https://faculty.math.illinois.edu/~rezk/quasicats.pdf |
| Reference:
|
[60] Riehl, Emily: Could \infty-category theory be taught to undergraduates?.Notices of the American Mathematical Society, DOI:10.1090/noti2692 MR 4577816, 10.1090/noti2692 |
| Reference:
|
[61] Riehl, Emily, Cavallo, Evan, Sattler, Christian: On the directed univalence axiom.https://math.jhu.edu/~eriehl/JMM2018-directed-univalence.pdf, Talk at the AMS Special Session on Homotopy Type Theory, Joint Mathematics Meetings |
| Reference:
|
[62] Riehl, Emily, Shulman, Michael: A type theory for synthetic \infty-categories.Higher Structures, Vol. 1, Iss. 1, 147-224, https://higher-structures.math.cas.cz/api/files/issues/Vol1Iss1/RiehlShulman MR 3912054, 10.21136/HS.2017.06 |
| Reference:
|
[63] Riehl, Emily, Verity, Dominic: Cartesian exponentiation and monadicity.https://arxiv.org/abs/2101.09853 MR 4768929 |
| Reference:
|
[64] Riehl, Emily, Verity, Dominic: Elements of \infty-Category Theory.Cambridge studies in advanced mathematics, Cambridge University Press, https://emilyriehl.github.io/files/elements.pdf, DOI:10.1017/9781108936880 MR 4354541, 10.1017/9781108936880 |
| Reference:
|
[65] Riehl, Emily, Verity, Dominic: Fibrations and yoneda’s lemma in an \infty-cosmos.J. Pure Appl. Algebra, Vol. 221, Iss. 3, 499-564, DOI:10.1016/j.jpaa.2016.07.003 MR 3556697, 10.1016/j.jpaa.2016.07.003 |
| Reference:
|
[66] Riehl, Emily, Verity, Dominic: Infinity category theory from scratch.Higher Structures, Vol. 4, Iss. 1, https://higher-structures.math.cas.cz/api/files/issues/Vol4Iss1/RiehlVerity MR 4074275 |
| Reference:
|
[67] Riehl, Emily, Verity, Dominic: The 2-category theory of quasi-categories.Advances in Mathematics, Vol. 280, 549-642, DOI:10.1016/j.aim.2015.04.021 MR 3350229, 10.1016/j.aim.2015.04.021 |
| Reference:
|
[68] Rijke, Egbert: Classifying types: Topics in synthetic homotopy theory.PhD, CMU |
| Reference:
|
[69] Rijke, Egbert: Introduction to homotopy type theory.Forthcoming book with CUP. Version from 06/02/22 |
| Reference:
|
[70] Rijke, Egbert, Shulman, Michael, Spitters, Bas: Modalities in homotopy type theory.Log. Meth. Comput. Sci., Vol. Volume 16, Issue 1, DOI:10.23638/LMCS-16(1:2)2020 MR 4054355, 10.23638/LMCS-16(1:2)2020 |
| Reference:
|
[71] Shulman, Michael: All (\infty,1)-toposes have strict univalent universes.https://arxiv.org/abs/1904.07004 |
| Reference:
|
[72] Shulman, Michael: The univalence axiom for elegant reedy presheaves.Homology, Homotopy and Applications, Vol. 17, Iss. 2, 81-106, DOI:doi:10.4310/HHA.2015.v17.n2.a6 MR 3421464, 10.4310/HHA.2015.v17.n2.a6 |
| Reference:
|
[73] Simpson, Carlos: Homotopy Theory of Higher Categories: From Segal Categories to n-Categories and Beyond.New mathematical monographs, Cambridge University Press, DOI:10.1017/CBO9780511978111 MR 2883823, 10.1017/CBO9780511978111 |
| Reference:
|
[74] Stenzel, Raffael: Bousfield-Segal spaces.Homology Homotopy Appl., Vol. 24, Iss. 1, 217-243, DOI:10.4310/HHA.2022.v24.n1.a12 MR 4404965, 10.4310/HHA.2022.v24.n1.a12 |
| Reference:
|
[75] Stenzel, Raffael: Univalence and completeness of Segal objects.https://arxiv.org/abs/1911.06640 MR 4510804 |
| Reference:
|
[76] Sterling, Jonathan: Geometric universes and topoi.https://www.jonmsterling.com/math/lectures/topos.html, Draft version from 07/31/22 |
| Reference:
|
[77] Street, Ross: Correction to: “Fibrations in bicategories”.Cahiers Topologie Géom. Différentielle Catég., Vol. 28, Iss. 1, 53-56 |
| Reference:
|
[78] Street, Ross: Cosmoi of internal categories.Trans. Am. Math. Soc., Vol. 258, 271-318, DOI:10.2307/1998059 10.1090/S0002-9947-1980-0558176-3 |
| Reference:
|
[79] Street, Ross: Elementary cosmoi. I.Category Sem., Proc., Sydney 1972/1973, Lect. Notes Math. 420, 134-180 (1974). 10.1007/BFb0063103 |
| Reference:
|
[80] Street, Ross: Fibrations and Yoneda’s lemma in a 2-category.Category Seminar (Proc. Sem., Sydney, 1972/1973), pp 104-133. Lecture Notes in Math.,Vol. 420, DOI:10.1007/BFb0063102 10.1007/BFb0063102 |
| Reference:
|
[81] Street, Ross: Fibrations in bicategories.Cahiers Topologie Géom. Différentielle, Vol. 21, Iss. 2, 111-160, http://www.numdam.org/article/CTGDC_1980__21_2_111_0.pdf |
| Reference:
|
[82] Streicher, Thomas: Fibered Categories à la Jean Bénabou.https://arxiv.org/abs/1801.02927 |
| Reference:
|
[83] Univalent Foundations Program, The: Homotopy type theory: Univalent foundations of mathematics.https://homotopytypetheory.org/book MR 3204653 |
| Reference:
|
[84] Voevodsky, Vladimir: A simple type system with two identity types.Unpublished note. https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf |
| Reference:
|
[85] Warren, Michael: Directed type theory.https://www.youtube.com/watch?v=znn6xEZUKNE, Lecture at IAS, Princeton |
| Reference:
|
[86] Weaver, Matthew Z., Licata, Daniel R.: A constructive model of directed univalence in bicubical sets.Proceedings of the 35th annual ACM/IEEE symposium on logic in computer science, pp 915-928, DOI:10.1145/3373718.3394794 10.1145/3373718.3394794 |
| Reference:
|
[87] Weinberger, Jonathan: A Synthetic Perspective on (\infty,1)-Category Theory: Fibrational and Semantic Aspects.PhD thesis, TU Darmstadt |
| Reference:
|
[88] Weinberger, Jonathan: Internal sums for synthetic fibered (\infty,1)-categories.https://arxiv.org/abs/2205.00386 MR 4722334 |
| Reference:
|
[89] Weinberger, Jonathan: Strict stability of extension types.https://arxiv.org/abs/2203.07194, arXiv |
| Reference:
|
[90] Weinberger, Jonathan: Two-sided cartesian fibrations of synthetic (\infty,1)-categories.https://arxiv.org/abs/2204.00938 MR 4788003 |
| . |
