Article
MSC:
03B38,
18D30,
18D40,
18D70,
18N45,
18N50,
18N55,
18N60,
55U35 | MR 4600458 | Zbl 1535.18039 | DOI: 10.21136/HS.2023.04
Full entry |
PDF
(1.3 MB)
Feedback
PDF
(1.3 MB)
Feedback
Keywords:
homotopy type theory; simplicial type theory; $(\infty,1)$-categories; Segal spaces; Rezk spaces; cartesian fibrations
homotopy type theory; simplicial type theory; $(\infty,1)$-categories; Segal spaces; Rezk spaces; cartesian fibrations
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.
References:
[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
[2] Annenkov, Danil, Capriotti, Paolo, Kraus, Nicolai, Sattler, Christian: Two-level type theory and applications. https://arxiv.org/abs/1705.03307 MR 4695500
[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
[4] Bakke, Fredrik: Segal spaces in homotopy type theory. Master’s thesis, NTNU
[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
[6] Barwick, Clark, Shah, Jay: Fibrations in \infty-category theory. 2016 MATRIX annals, pages 17-42, MR 3792514
[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 DOI 10.4310/HHA.2008.v10.n2.a9 | MR 2475608
[8] Bergner, Julia E.: The homotopy theory of (\infty,1)-categories. Cambridge University Press, Volume 90, DOI:10.1017/9781316181874 DOI 10.1017/9781316181874 | MR 3791455
[9] Bezem, Marc, Buchholtz, Ulrik, Cagne, Pierre, Dundas, Bjørn, Grayson, Dan: Symmetry. https://github.com/UniMath/SymmetryBook
[10] Li-Bland, David: The stack of higher internal categories and stacks of iterated spans. https://arxiv.org/abs/1506.08870
[11] Borceux, Francis: Handbook of categorical algebra: Volume 2, categories and structures. Cambridge University Press, Volume 2
[12] Bousfield, Aldridge K.: The simplicial homotopy theory of iterated loop spaces. Typed notes by Julie Bergner
[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
[14] Capriotti, Paolo: Models of type theory with strict equality. PhD thesis, The University of Nottingham
[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
[16] Cisinski, Denis-Charles: Higher categories and homotopical algebra. Cambridge studies in advanced mathematics, Cambridge University Press, DOI:10.1017/9781108588737 DOI 10.1017/9781108588737 | MR 3931682
[17] Cisinski, Denis-Charles: Univalent universes for elegant models of homotopy types. https://arxiv.org/abs/1406.0058
[18] Clementino, Maria Manuel, Nunes, Fernando Lucatelli: Lax comma 2-categories and admissible 2-functors. https://arxiv.org/abs/2002.03132 MR 4732696
[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
[20] Columbus, Tobias: 2-Categorical aspects of quasi-categories. PhD thesis, Karlsruher Institut für Technologie (KIT); Karlsruher Institut für Technologie (KIT)
[21] Brito, Pedro Boavida: Segal objects and the Grothendieck construction. https://arxiv.org/abs/1605.00706 MR 3807750
[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 DOI 10.25537/dm.2017v22.1225-1266 | MR 3690268
[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 DOI 10.1007/978-3-642-99902-4_2
[24] Hackney, Philip, Ozornova, Viktoriya, Riehl, Emily, Rovelli, Martina: An (\infty,2)-categorical pasting theorem. https://arxiv.org/abs/2106.03660 MR 4510118
[25] Hermida, Claudio: On fibred adjunctions and completeness for fibred categories. Recent trends in data type specification, pages 235-251,
[26] Johnson, Niles, Yau, Donald: A bicategorical pasting theorem. https://arxiv.org/abs/1910.01220
[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 DOI 10.1112/plms/s3-38.2.237
[28] Joyal, André: Notes on quasi-categories. http://www.math.uchicago.edu/~may/IMA/Joyal.pdf
[29] Joyal, André: Quasi-categories and Kan complexes. J. Pure Appl. Algebra, pages 207-222, 175 MR 1935979
[30] Joyal, André, Tierney, Myles: Quasi-categories vs Segal spaces. Contemporary Mathematics, Vol. 431, Iss. 277-326, 10 DOI 10.1090/conm/431/08278 | MR 2342834
[31] Kavvos, Alex: A quantum of direction. https://www.lambdabetaeta.eu/papers/meio.pdf, preprint
[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 DOI 10.1007/s10688-014-0050-3 | MR 3288174
[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 DOI 10.1017/S0960129512000217 | MR 3008196
[34] Kudasov, Nikolai: Rzk. https://github.com/fizruk/rzk, Prototype interactive proof assistant based on a type theory for synthetic \infty-categories
[35] Licata, Dan: More fibrations. https://github.com/dlicata335/cart-cube/blob/master/agda/directed/moreFibs.agda, Agda Formalization
[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
[37] Lietz, Peter: A fibrational theory of geometric morphisms. Diploma thesis, TU Darmstadt
[38] Lurie, Jacob: (\infty, 2)-Categories and the Goodwillie Calculus I. https://arxiv.org/abs/0905.0462
[39] Lurie, Jacob: Higher topos theory. Annals of mathematics studies 170, Princeton University Press, https://arxiv.org/abs/math/0608040, DOI:10.1515/9781400830558 DOI 10.1515/9781400830558
[40] Martínez, César Bardomiano: Limits and colimits of synthetic \infty-categories. https://arxiv.org/abs/2202.12386 MR 4963152
[41] Martini, Louis: Cocartesian fibrations and straightening internal to an \infty-topos. https://arxiv.org/abs/2204.00295
[42] Martini, Louis: Yoneda’s lemma for internal higher categoriess. https://arxiv.org/abs/2103.17141
[43] Martini, Louis, Wolf, Sebastian: Limits and colimits in internal higher category theory. https://arxiv.org/abs/2111.14495 MR 4752519
[44] Mazel-Gee, Aaron: A user’s guide to co/cartesian fibrations. https://arxiv.org/abs/1510.02402 MR 3999274
[45] Moens, Jean-Luc: Caracterisation des topos de faisceaux sur un site interne à un topos. PhD thesis, UCL-Université Catholique de Louvain
[46] Nguyen, Hoang Kim: Theorems in higher category theory and applications. PhD thesis, Universität Regensburg
[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 DOI 10.1016/j.entcs.2019.09.012 | MR 4043275
[48] Nuyts, Andreas: Contributions to multimode and presheaf type theory. PhD thesis, KU Leuven
[49] Nuyts, Andreas: Towards a directed homotopy type theory based on 4 kinds of variance. Master’s thesis, KU Leuven
[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 DOI 10.1007/978-3-030-05674-2 | MR 3932125
[51] Rasekh, Nima: A Model for the Higher Category of Higher Categories. https://arxiv.org/abs/1805.03816 MR 4695986
[52] Rasekh, Nima: Cartesian fibrations and representability. https://arxiv.org/abs/1711.03670 MR 4467022
[53] Rasekh, Nima: Cartesian fibrations of complete segal spaces. https://arxiv.org/abs/2102.05190 MR 4600457
[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 DOI 10.1007/s40062-021-00288-2 | MR 4343074
[55] Rasekh, Nima: Univalence in higher category theory. https://arxiv.org/abs/2103.12762
[56] Rasekh, Nima: Yoneda lemma for \mathcal{D}-simplicial spaces. https://arxiv.org/abs/2108.06168 MR 4616631
[57] Rasekh, Nima: Yoneda lemma for simplicial spaces. https://arxiv.org/abs/1711.03160 MR 4616631
[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 DOI 10.1090/S0002-9947-00-02653-2 | MR 1804411
[59] Rezk, Charles: Stuff about quasicategories. https://faculty.math.illinois.edu/~rezk/quasicats.pdf
[60] Riehl, Emily: Could \infty-category theory be taught to undergraduates?. Notices of the American Mathematical Society, DOI:10.1090/noti2692 DOI 10.1090/noti2692 | MR 4577816
[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
[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 DOI 10.21136/HS.2017.06 | MR 3912054
[63] Riehl, Emily, Verity, Dominic: Cartesian exponentiation and monadicity. https://arxiv.org/abs/2101.09853 MR 4768929
[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 DOI 10.1017/9781108936880 | MR 4354541
[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 DOI 10.1016/j.jpaa.2016.07.003 | MR 3556697
[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
[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 DOI 10.1016/j.aim.2015.04.021 | MR 3350229
[68] Rijke, Egbert: Classifying types: Topics in synthetic homotopy theory. PhD, CMU
[69] Rijke, Egbert: Introduction to homotopy type theory. Forthcoming book with CUP. Version from 06/02/22
[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 DOI 10.23638/LMCS-16(1:2)2020 | MR 4054355
[71] Shulman, Michael: All (\infty,1)-toposes have strict univalent universes. https://arxiv.org/abs/1904.07004
[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 DOI 10.4310/HHA.2015.v17.n2.a6 | MR 3421464
[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 DOI 10.1017/CBO9780511978111 | MR 2883823
[74] Stenzel, Raffael: Bousfield-Segal spaces. Homology Homotopy Appl., Vol. 24, Iss. 1, 217-243, DOI:10.4310/HHA.2022.v24.n1.a12 DOI 10.4310/HHA.2022.v24.n1.a12 | MR 4404965
[75] Stenzel, Raffael: Univalence and completeness of Segal objects. https://arxiv.org/abs/1911.06640 MR 4510804
[76] Sterling, Jonathan: Geometric universes and topoi. https://www.jonmsterling.com/math/lectures/topos.html, Draft version from 07/31/22
[77] Street, Ross: Correction to: “Fibrations in bicategories” . Cahiers Topologie Géom. Différentielle Catég., Vol. 28, Iss. 1, 53-56
[78] Street, Ross: Cosmoi of internal categories. Trans. Am. Math. Soc., Vol. 258, 271-318, DOI:10.2307/1998059 DOI 10.1090/S0002-9947-1980-0558176-3
[79] Street, Ross: Elementary cosmoi. I. Category Sem., Proc., Sydney 1972/1973, Lect. Notes Math. 420, 134-180 (1974). DOI 10.1007/BFb0063103
[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 DOI 10.1007/BFb0063102
[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
[82] Streicher, Thomas: Fibered Categories à la Jean Bénabou. https://arxiv.org/abs/1801.02927
[83] Univalent Foundations Program, The: Homotopy type theory: Univalent foundations of mathematics. https://homotopytypetheory.org/book MR 3204653
[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
[85] Warren, Michael: Directed type theory. https://www.youtube.com/watch?v=znn6xEZUKNE, Lecture at IAS, Princeton
[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 DOI 10.1145/3373718.3394794
[87] Weinberger, Jonathan: A Synthetic Perspective on (\infty,1)-Category Theory: Fibrational and Semantic Aspects. PhD thesis, TU Darmstadt
[88] Weinberger, Jonathan: Internal sums for synthetic fibered (\infty,1)-categories. https://arxiv.org/abs/2205.00386 MR 4722334
[89] Weinberger, Jonathan: Strict stability of extension types. https://arxiv.org/abs/2203.07194, arXiv
[90] Weinberger, Jonathan: Two-sided cartesian fibrations of synthetic (\infty,1)-categories. https://arxiv.org/abs/2204.00938 MR 4788003
Search
Partner of
