References
- [1] M. Artin, A. Grothendieck, and J.L. Verdier. Théorie des topos et cohomologie étale des schémas. Tome 1: Théorie des topos (exposés i à iv). Séminaire de Géométrie Algébrique du Bois Marie, Vol.1964.
- [2] Grzegorz Bancerek. Increasing and continuous ordinal sequences. Formalized Mathematics, 1(4):711–714, 1990.
- [3] Grzegorz Bancerek. Veblen hierarchy. Formalized Mathematics, 19(2):83–92, 2011. doi:10.2478/v10037-011-0014-5.
- [4] Grzegorz Bancerek. Consequences of the reflection theorem. Formalized Mathematics, 1 (5):989–993, 1990.
- [5] Grzegorz Bancerek. The reflection theorem. Formalized Mathematics, 1(5):973–977, 1990.
- [6] Grzegorz Bancerek and Noboru Endou. Compactness of lim-inf topology. Formalized Mathematics, 9(4):739–743, 2001.
- [7] Grzegorz Bancerek and Andrzej Kondracki. Mostowski’s fundamental operations – Part II. Formalized Mathematics, 2(3):425–427, 1991.
- [8] Grzegorz Bancerek, Noboru Endou, and Yuji Sakai. On the characterizations of compactness. Formalized Mathematics, 9(4):733–738, 2001.
- [9] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-817.
- [10] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.604425130069070
- [11] Chad E. Brown and Karol Pąk. A tale of two set theories. In Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics – 12th International Conference, CICM 2019, CIIRC, Prague, Czech Republic, July 8-12, 2019, Proceedings, volume 11617 of Lecture Notes in Computer Science, pages 44–60. Springer, 2019. doi:10.1007/978-3-030-23250-44.
- [12] Czesław Byliński. Category Ens. Formalized Mathematics, 2(4):527–533, 1991.
- [13] Olivia Caramello and Riccardo Zanfa. Relative topos theory via stacks. arXiv preprint arXiv:2107.04417, 2021.
- [14] Daniel Gratzer, Michael Shulman, and Jonathan Sterling. Strict universes for Grothendieck topoi. arXiv preprint arXiv:2202.12012, 2022.
- [15] Ewa Grądzka. On the order-consistent topology of complete and uncomplete lattices. Formalized Mathematics, 9(2):377–382, 2001.
- [16] Andrzej Kondracki. Mostowski’s fundamental operations – Part I. Formalized Mathematics, 2(3):371–375, 1991.
- [17] Jacob Lurie. Higher Topos Theory. Princeton University Press, 2009.10.1515/9781400830558
- [18] Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, Heidelberg, Berlin, 1971.
- [19] Beata Madras. Irreducible and prime elements. Formalized Mathematics, 6(2):233–239, 1997.
- [20] Michał Muzalewski. Categories of groups. Formalized Mathematics, 2(4):563–571, 1991.
- [21] Michał Muzalewski. Category of left modules. Formalized Mathematics, 2(5):649–652, 1991.
- [22] Michał Muzalewski. Rings and modules – part II. Formalized Mathematics, 2(4):579–585, 1991.
- [23] Michał Muzalewski. Category of rings. Formalized Mathematics, 2(5):643–648, 1991.
- [24] nLab Authors. Grothendieck universe, 2022.
- [25] Bogdan Nowak and Grzegorz Bancerek. Universal classes. Formalized Mathematics, 1(3): 595–600, 1990.
- [26] Karol Pąk. Grothendieck universes. Formalized Mathematics, 28(2):211–215, 2020. doi:10.2478/forma-2020-0018.
- [27] Krzysztof Retel. The class of series-parallel graphs. Part II. Formalized Mathematics, 11 (3):289–291, 2003.
- [28] Marco Riccardi. Free magmas. Formalized Mathematics, 18(1):17–26, 2010. doi:10.2478/v10037-010-0003-0.
- [29] Emily Riehl. Category theory in context. Courier Dover Publications, 2017.
- [30] Michael A. Shulman. Set theory for category theory. arXiv preprint arXiv:0810.1279, 2008.
- [31] Bartłomiej Skorulski. Lim-inf convergence. Formalized Mathematics, 9(2):237–240, 2001.
- [32] Andrzej Trybulec. Scott topology. Formalized Mathematics, 6(2):311–319, 1997.
- [33] Andrzej Trybulec. Moore-Smith convergence. Formalized Mathematics, 6(2):213–225, 1997.
- [34] Josef Urban. Mahlo and inaccessible cardinals. Formalized Mathematics, 9(3):485–489, 2001.
- [35] Mariusz łynel. The equational characterization of continuous lattices. Formalized Mathematics, 6(2):199–205, 1997.