[
[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.
]Search in Google Scholar
[
[2] Grzegorz Bancerek. Increasing and continuous ordinal sequences. Formalized Mathematics, 1(4):711–714, 1990.
]Search in Google Scholar
[
[3] Grzegorz Bancerek. Veblen hierarchy. Formalized Mathematics, 19(2):83–92, 2011. doi:10.2478/v10037-011-0014-5.
]Open DOISearch in Google Scholar
[
[4] Grzegorz Bancerek. Consequences of the reflection theorem. Formalized Mathematics, 1 (5):989–993, 1990.
]Search in Google Scholar
[
[5] Grzegorz Bancerek. The reflection theorem. Formalized Mathematics, 1(5):973–977, 1990.
]Search in Google Scholar
[
[6] Grzegorz Bancerek and Noboru Endou. Compactness of lim-inf topology. Formalized Mathematics, 9(4):739–743, 2001.
]Search in Google Scholar
[
[7] Grzegorz Bancerek and Andrzej Kondracki. Mostowski’s fundamental operations – Part II. Formalized Mathematics, 2(3):425–427, 1991.
]Search in Google Scholar
[
[8] Grzegorz Bancerek, Noboru Endou, and Yuji Sakai. On the characterizations of compactness. Formalized Mathematics, 9(4):733–738, 2001.
]Search in Google Scholar
[
[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.
]Open DOISearch in Google Scholar
[
[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
]Open DOISearch in Google Scholar
[
[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.
]Open DOISearch in Google Scholar
[
[12] Czesław Byliński. Category Ens. Formalized Mathematics, 2(4):527–533, 1991.
]Search in Google Scholar
[
[13] Olivia Caramello and Riccardo Zanfa. Relative topos theory via stacks. arXiv preprint arXiv:2107.04417, 2021.
]Search in Google Scholar
[
[14] Daniel Gratzer, Michael Shulman, and Jonathan Sterling. Strict universes for Grothendieck topoi. arXiv preprint arXiv:2202.12012, 2022.
]Search in Google Scholar
[
[15] Ewa Grądzka. On the order-consistent topology of complete and uncomplete lattices. Formalized Mathematics, 9(2):377–382, 2001.
]Search in Google Scholar
[
[16] Andrzej Kondracki. Mostowski’s fundamental operations – Part I. Formalized Mathematics, 2(3):371–375, 1991.
]Search in Google Scholar
[
[17] Jacob Lurie. Higher Topos Theory. Princeton University Press, 2009.10.1515/9781400830558
]Search in Google Scholar
[
[18] Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, Heidelberg, Berlin, 1971.
]Search in Google Scholar
[
[19] Beata Madras. Irreducible and prime elements. Formalized Mathematics, 6(2):233–239, 1997.
]Search in Google Scholar
[
[20] Michał Muzalewski. Categories of groups. Formalized Mathematics, 2(4):563–571, 1991.
]Search in Google Scholar
[
[21] Michał Muzalewski. Category of left modules. Formalized Mathematics, 2(5):649–652, 1991.
]Search in Google Scholar
[
[22] Michał Muzalewski. Rings and modules – part II. Formalized Mathematics, 2(4):579–585, 1991.
]Search in Google Scholar
[
[23] Michał Muzalewski. Category of rings. Formalized Mathematics, 2(5):643–648, 1991.
]Search in Google Scholar
[
[24] nLab Authors. Grothendieck universe, 2022.
]Search in Google Scholar
[
[25] Bogdan Nowak and Grzegorz Bancerek. Universal classes. Formalized Mathematics, 1(3): 595–600, 1990.
]Search in Google Scholar
[
[26] Karol Pąk. Grothendieck universes. Formalized Mathematics, 28(2):211–215, 2020. doi:10.2478/forma-2020-0018.
]Open DOISearch in Google Scholar
[
[27] Krzysztof Retel. The class of series-parallel graphs. Part II. Formalized Mathematics, 11 (3):289–291, 2003.
]Search in Google Scholar
[
[28] Marco Riccardi. Free magmas. Formalized Mathematics, 18(1):17–26, 2010. doi:10.2478/v10037-010-0003-0.
]Open DOISearch in Google Scholar
[
[29] Emily Riehl. Category theory in context. Courier Dover Publications, 2017.
]Search in Google Scholar
[
[30] Michael A. Shulman. Set theory for category theory. arXiv preprint arXiv:0810.1279, 2008.
]Search in Google Scholar
[
[31] Bartłomiej Skorulski. Lim-inf convergence. Formalized Mathematics, 9(2):237–240, 2001.
]Search in Google Scholar
[
[32] Andrzej Trybulec. Scott topology. Formalized Mathematics, 6(2):311–319, 1997.
]Search in Google Scholar
[
[33] Andrzej Trybulec. Moore-Smith convergence. Formalized Mathematics, 6(2):213–225, 1997.
]Search in Google Scholar
[
[34] Josef Urban. Mahlo and inaccessible cardinals. Formalized Mathematics, 9(3):485–489, 2001.
]Search in Google Scholar
[
[35] Mariusz łynel. The equational characterization of continuous lattices. Formalized Mathematics, 6(2):199–205, 1997.
]Search in Google Scholar
