@book{bloch_real_2010,
	address = {Heidelberg},
	title = {The {Real} {Numbers} and {Real} {Analysis}},
	isbn = {978-0-387-72176-7},
	publisher = {Springer Science + Business Media},
	author = {Bloch, Ethan D.},
	year = {2010},
}
@book{takeuti_introduction_1971,
	address = {Heidelberg},
	title = {Introduction to {Axiomatic} {Set} {Theory}},
	isbn = {0-387-05302-6},
	publisher = {Springer-Verlag},
	author = {Takeuti, Gaisi and Zaring, Wilson M.},
	year = {1971},
}
@book{bourbaki_elements_1970,
	title = {Elements of {Mathematics}, {Theory} of {Sets}},
	isbn = {978-3-540-22525-6},
	publisher = {Originally published as {\'E}l{\'e}ments de Math{\'e}matique Th{\'e}orie des Ensembles; Paris: N. Bourbaki. Reprint, Heidelberg: Springer-Verlag, 2004.},
	author = {Bourbaki, Nicolas},
	year = {1970},
}
@book{hungerford_algebra_2003,
	address = {New York},
	title = {Algebra},
	isbn = {978-0-387-90518-1},
	publisher = {Springer},
	author = {Hungerford, Thomas W.},
	year = {2003},
}
@book{kelley_general_1955,
	title = {General {Topology}},
	isbn = {978-0-486-81544-2},
	publisher = {Originally published as General Topology; New York, NY, USA: Van Nostrand Reinhold Company. Reprint, Mineola, NY, USA: Dover Publications, 2017},
	author = {Kelley, John L.},
	year = {1955},
}
@incollection{berardi_locales_2004,
	address = {Heidelberg},
	title = {Locales and {Locale} {Expressions} in {Isabelle}/{Isar}},
	volume = {3085},
	isbn = {978-3-540-22164-7},
	booktitle = {Types for {Proofs} and {Programs}},
	publisher = {Springer},
	author = {Ballarin, Clemens},
	editor = {Berardi, Stefano and Coppo, Mario and Damiani, Ferruccio},
	year = {2004},
	pages = {34--50},
}
@book{adamek_abstract_2006,
	title = {Abstract and {Concrete} {Categories} - {The} {Joy} of {Cats}},
	author = {Adamek, Jiri and Herrlich, Horst and Strecker, George},
	year = {2006},
}
@misc{noauthor_wikipedia_2001,
	title = {Wikipedia},
	url = {https://www.wikipedia.org/},
	year = {2001},
}
@misc{noauthor_encyclopedia_nodate,
	title = {Encyclopedia of {Mathematics}},
	url = {https://www.encyclopediaofmath.org/index.php/Main_Page},
}
@misc{noauthor_proofwiki_nodate,
	title = {{ProofWiki}},
	url = {https://proofwiki.org/wiki/Main_Page},
}
@article{paulson_hereditarily_2013,
	title = {The {Hereditarily} {Finite} {Sets}},
	journal = {Archive of Formal Proofs},
	author = {Paulson, Lawrence C.},
	year = {2013},
}
@book{mac_lane_categories_2010,
	address = {New York},
	edition = {2},
	series = {Graduate {Texts} in {Mathematics}},
	title = {Categories for the {Working} {Mathematician}},
	isbn = {978-1-4419-3123-8},
	number = {5},
	publisher = {Springer},
	author = {Mac Lane, Saunders},
	year = {2010},
}
@article{stark_category_2016,
	title = {Category {Theory} with {Adjunctions} and {Limits}},
	journal = {Archive of Formal Proofs},
	author = {Stark, Eugene W.},
	year = {2016},
}
@article{paulson_zermelo_2019,
	title = {Zermelo {Fraenkel} {Set} {Theory} in {Higher}-{Order} {Logic}},
	journal = {Archive of Formal Proofs},
	author = {Paulson, Lawrence C.},
	year = {2019},
}
@article{katovsky_category_2010,
	title = {Category {Theory}},
	journal = {Archive of Formal Proofs},
	author = {Katovsky, Alexander},
	year = {2010},
}
@article{okeefe_category_2005,
	title = {Category {Theory} to {Yoneda}'s {Lemma}},
	journal = {Archive of Formal Proofs},
	author = {O'Keefe, Greg},
	year = {2005},
}
@misc{noauthor_nlab_nodate,
	title = {{nLab}},
	url = {https://ncatlab.org/nlab/show/HomePage},
}
@book{bodo_categories_1970,
	address = {New York},
	title = {Categories and {Functors}},
	publisher = {Academic Press},
	author = {Bodo, Pareigis},
	year = {1970},
}
@article{mitchell_dominion_1972,
	title = {The {Dominion} of {Isbell}},
	volume = {167},
	journal = {Transactions of the American Mathematical Society},
	author = {Mitchell, Barry},
	year = {1972},
}
@inproceedings{brown_higher-order_2019,
	address = {Portland, USA},
	title = {Higher-{Order} {Tarski} {Grothendieck} as a {Foundation} for {Formal} {Proof}},
	booktitle = {10th {International} {Conference} on {Interactive} {Theorem} {Proving} ({ITP} 2019)},
	author = {Brown, Chad E. and Kaliszyk, Cezary and Pak, Karol},
	editor = {Harrison, John and O'Leary, John and Tolmach, Andrew},
	year = {2019},
	keywords = {000 Computer science, knowledge, general works, Computer Science},
	pages = {9:1--9:16},
}
@inproceedings{feferman_set-theoretical_1969,
	address = {Heidelberg},
	series = {Lecture {Notes} in {Mathematics}},
	title = {Set-{Theoretical} {Foundations} of {Category} {Theory}},
	booktitle = {Reports of the {Midwest} {Category} {Seminar} {III}},
	publisher = {Springer},
	author = {Feferman, Solomon and Kreisel, Georg},
	editor = {Barr, M. and Berthiaume, P. and Day, B. J. and Duskin, J. and Feferman, S. and Kelly, G. M. and Mac Lane, S. and Tierney, M. and Walters, R. F. C.},
	year = {1969},
	keywords = {Abelian Group, Category Theory, Closure Condition, Free Variable, Mathematical Practice},
	pages = {201--247},
}
@article{shulman_set_2008,
	title = {Set {Theory} for {Category} {Theory}},
	url = {http://arxiv.org/abs/0810.1279},
	journal = {arXiv:0810.1279 [math]},
	author = {Shulman, Michael A.},
	year = {2008},
	keywords = {Mathematics - Category Theory, Mathematics - Logic},
}
@incollection{barkaoui_partizan_2006,
	address = {Berlin},
	title = {Partizan {Games} in {Isabelle}/{HOLZF}},
	volume = {4281},
	isbn = {978-3-540-48815-6},
	booktitle = {{ICTAC} 2006},
	publisher = {Springer},
	author = {Obua, Steven},
	editor = {Barkaoui, Kamel and Cavalcanti, Ana and Cerone, Antonio},
	year = {2006},
	pages = {272--286},
}
@book{jech_set_2006,
	address = {Heidelberg},
	edition = {3},
	series = {Pure and applied mathematics},
	title = {Set {Theory}},
	isbn = {3-540-44085-2},
	number = {79},
	publisher = {Springer},
	author = {Jech, Thomas},
	year = {2006},
	keywords = {Set theory},
}
@incollection{sica_doing_2006,
	title = {On {Doing} {Category} {Theory} within {Set} {Theoretic} {Foundations}},
	isbn = {978-88-7699-031-1},
	booktitle = {What is {Category} {Theory}?},
	publisher = {Polimetrica s.a.s.},
	author = {Rao, Vidhyanath K.},
	editor = {Sica, Giandomenico},
	year = {2006},
	keywords = {Mathematics / General},
}
@unpublished{ballarin_tutorial_2020,
	title = {Tutorial to {Locales} and {Locale} {Interpretation}},
	url = {https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020/doc/locales.pdf},
	author = {Ballarin, Clemens},
	year = {2020},
}
@inproceedings{kuncar_types_2014,
	title = {From {Types} to {Sets} in {Isabelle}/{HOL}},
	booktitle = {Isabelle {Workshop}, {Vienna}, {Austria}, {July} 13, 2014, {Revised} {Selected} {Papers}},
	author = {Kun{\v c}ar, Ond{\v r}ej and Popescu, Andrei},
	year = {2014},
}
@misc{noauthor_isabellehol_2020,
	title = {Isabelle/{HOL} {Standard} {Library}},
	url = {https://isabelle.in.tum.de/website-Isabelle2020/dist/library/HOL/HOL/index.html},
	journal = {Isabelle/HOL},
	year = {2020},
}
@misc{eberl_syntax_2021,
	title = {Syntax proposal: multiway if},
	url = {https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-February/msg00034.html},
	journal = {The Cl-isabelle-users Archives},
	author = {Eberl, Manuel},
	year = {2021},
}
@misc{noauthor_association_nodate,
	title = {Association of {Mizar} {Users}. {Mizar} home page.},
	url = {http://mizar.org/},
}
@article{bylinski_introduction_1990,
	title = {Introduction to {Categories} and {Functors}},
	volume = {1},
	number = {2},
	journal = {Formalized Mathematics},
	author = {Byli{\'n}ski, Czes{\l }aw},
	year = {1990},
	pages = {409--420},
}
@article{bylinski_subcategories_1990,
	title = {Subcategories and {Products} of {Categories}},
	volume = {1},
	number = {4},
	journal = {Formalized Mathematics},
	author = {Byli{\'n}ski, Czes{\l }aw},
	year = {1990},
	pages = {725--732},
}
@article{bylinski_opposite_1991,
	title = {Opposite {Categories} and {Contravariant} {Functors}},
	volume = {2},
	number = {3},
	journal = {Formalized Mathematics},
	author = {Byli{\'n}ski, Czes{\l }aw},
	year = {1991},
	pages = {419--424},
}
@article{trybulec_natural_1991,
	title = {Natural {Transformations}. {Discrete} {Categories}},
	volume = {2},
	number = {4},
	journal = {Formalized Mathematics},
	author = {Trybulec, Andrzej},
	year = {1991},
	pages = {467--474},
}
@article{bylinski_category_1991,
	title = {Category {Ens}},
	volume = {2},
	number = {4},
	journal = {Formalized Mathematics},
	author = {Byli{\'n}ski, Czes{\l }aw},
	year = {1991},
	pages = {527--533},
}
@article{muzalewski_categories_1991,
	title = {Categories of {Groups}},
	volume = {2},
	number = {4},
	journal = {Formalized Mathematics},
	author = {Muzalewski, Micha{\l }},
	year = {1991},
	pages = {563--571},
}
@article{trybulec_isomorphisms_1991,
	title = {Isomorphisms of {Categories}},
	volume = {2},
	number = {5},
	journal = {Formalized Mathematics},
	author = {Trybulec, Andrzej},
	year = {1991},
	pages = {629--634},
}
@article{muzalewski_category_1991,
	title = {Category of {Rings}},
	volume = {2},
	number = {5},
	journal = {Formalized Mathematics},
	author = {Muzalewski, Micha{\l }},
	year = {1991},
	pages = {643--648},
}
@article{muzalewski_category_1991-1,
	title = {Category of {Left} {Modules}},
	volume = {2},
	number = {5},
	journal = {Formalized Mathematics},
	author = {Muzalewski, Micha{\l }},
	year = {1991},
	pages = {649--652},
}
@article{bancerek_comma_1991,
	title = {Comma {Category}},
	volume = {2},
	number = {5},
	journal = {Formalized Mathematics},
	author = {Bancerek, Grzegorz and Darmochwa{\l }, Agata},
	year = {1991},
	pages = {679--681},
}
@article{bylinski_products_1991,
	title = {Products and {Coproducts} in {Categories}},
	volume = {2},
	number = {5},
	journal = {Formalized Mathematics},
	author = {Byli{\'n}ski, Czes{\l }aw},
	year = {1991},
	pages = {701--709},
}
@article{trybulec_isomorphisms_1992,
	title = {Some {Isomorphisms} {Between} {Functor} {Categories}},
	volume = {3},
	number = {1},
	journal = {Formalized Mathematics},
	author = {Trybulec, Andrzej},
	year = {1992},
	pages = {33--40},
}
@article{bylinski_cartesian_1992,
	title = {Cartesian {Categories}},
	volume = {3},
	number = {2},
	journal = {Formalized Mathematics},
	author = {Byli{\'n}ski, Czes{\l }aw},
	year = {1992},
	pages = {161--169},
}
@article{bancerek_categorial_1996,
	title = {Categorial {Categories} and {Slice} {Categories}},
	volume = {5},
	number = {2},
	journal = {Formalized Mathematics},
	author = {Bancerek, Grzegorz},
	year = {1996},
	pages = {157--165},
}
@article{trybulec_categories_1996,
	title = {Categories without {Uniqueness} of cod and dom},
	volume = {5},
	number = {2},
	journal = {Formalized Mathematics},
	author = {Trybulec, Andrzej},
	year = {1996},
	pages = {259--267},
}
@article{bancerek_indexed_1996,
	title = {Indexed {Category}},
	volume = {5},
	number = {3},
	journal = {Formalized Mathematics},
	author = {Bancerek, Grzegorz},
	year = {1996},
	pages = {329--337},
}
@article{trybulec_functors_1996,
	title = {Functors for {Alternative} {Categories}},
	volume = {5},
	number = {4},
	journal = {Formalized Mathematics},
	author = {Trybulec, Andrzej},
	year = {1996},
	pages = {595--608},
}
@article{nieszczerzewski_category_1997,
	title = {Category of {Functors} {Between} {Alternative} {Categories}},
	volume = {6},
	number = {3},
	journal = {Formalized Mathematics},
	author = {Nieszczerzewski, Robert},
	year = {1997},
	pages = {371--375},
}
@article{kornilowicz_categories_1997,
	title = {On the {Categories} {Without} {Uniqueness} of cod and dom. {Some} {Properties} of the {Morphisms} and the {Functors}},
	volume = {6},
	number = {4},
	journal = {Formalized Mathematics},
	author = {Korni{\l }owicz, Artur},
	year = {1997},
	pages = {475--481},
}
@article{kornilowicz_composition_1998,
	title = {The {Composition} of {Functors} and {Transformations} in {Alternative} {Categories}},
	volume = {7},
	number = {1},
	journal = {Formalized Mathematics},
	author = {Korni{\l }owicz, Artur},
	year = {1998},
	pages = {1--7},
}
@article{bancerek_concrete_2001,
	title = {Concrete {Categories}},
	volume = {9},
	number = {3},
	journal = {Formalized Mathematics},
	author = {Bancerek, Grzegorz},
	year = {2001},
	pages = {605--621},
}
@article{kornilowicz_products_2012,
	title = {Products in {Categories} without {Uniqueness} of cod and dom},
	volume = {20},
	number = {4},
	journal = {Formalized Mathematics},
	author = {Korni{\l }owicz, Artur},
	year = {2012},
	pages = {303--307},
}
@article{riccardi_object-free_2013,
	title = {Object-{Free} {Definition} of {Categories}},
	volume = {21},
	number = {3},
	journal = {Formalized Mathematics},
	author = {Riccardi, Marco},
	year = {2013},
	keywords = {correspondence between different approaches to category, object-free category},
	pages = {193--205},
}
@article{golinski_coproducts_2013,
	title = {Coproducts in {Categories} without {Uniqueness} of cod and dom},
	volume = {21},
	number = {4},
	journal = {Formalized Mathematics},
	author = {Goli{\'n}ski, Maciej and Korni{\l }owicz, Artur},
	year = {2013},
	keywords = {coproducts, disjoined union},
	pages = {235--239},
}
@book{grabowski_preface_2014,
	title = {Preface},
	volume = {22},
	number = {2},
	author = {Grabowski, Adam and Shidama, Yasunari},
	year = {2014},
	keywords = {Mizar, Mizar Mathematical Library},
}
@article{riccardi_categorical_2015,
	title = {Categorical {Pullbacks}},
	volume = {23},
	doi = {10.2478/forma-2015-0001},
	number = {1},
	journal = {Formalized Mathematics},
	author = {Riccardi, Marco},
	year = {2015},
	keywords = {category pullback, pullback lemma},
	pages = {1--14},
}
@article{riccardi_exponential_2015,
	title = {Exponential {Objects}},
	volume = {23},
	number = {4},
	journal = {Formalized Mathematics},
	author = {Riccardi, Marco},
	year = {2015},
	keywords = {exponential objects, functor category, natural transformation},
	pages = {351--369},
}
@article{paulson_natural_1986,
	title = {Natural {Deduction} as {Higher}-{Order} {Resolution}},
	volume = {3},
	doi = {10.1016/0743-1066(86)90015-4},
	number = {3},
	journal = {The Journal of Logic Programming},
	author = {Paulson, Lawrence C.},
	year = {1986},
	pages = {237--258},
}
@book{riehl_category_2016,
	title = {Category {Theory} in {Context}},
	publisher = {Emily Riehl},
	author = {Riehl, Emily},
	year = {2016},
	keywords = {Mathematics / Logic},
}
@misc{chen_hotg_2021,
	title = {{HOTG}},
	url = {https://bitbucket.org/cezaryka/tyset/src},
	journal = {HOTG},
	author = {Chen, Joshua and Kappelmann, Kevin and Krauss, Alexander},
	year = {2021},
}
@misc{haftmann_sketch-and-explore_2021,
	title = {Sketch-and-{Explore}},
	url = {https://isabelle.in.tum.de/library/HOL/HOL-ex/Sketch_and_Explore.html},
	author = {Haftmann, Florian},
	year = {2021},
}
@book{megill_metamath_2019,
	address = {Morrisville, North Carolina},
	title = {Metamath: {A} {Computer} {Language} for {Mathematical} {Proofs}},
	isbn = {978-0-359-70223-7},
	publisher = {Lulu Press},
	author = {Megill, Norman and Wheeler, David A.},
	year = {2019},
}
@inproceedings{kammuller_locales_1999,
	address = {Heidelberg, Germany},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Locales {A} {Sectioning} {Concept} for {Isabelle}},
	isbn = {978-3-540-48256-7},
	doi = {10.1007/3-540-48256-3_11},
	booktitle = {Proceedings of the 12th {International} {Conference} on {Theorem} {Proving} in {Higher} {Order} {Logics}, {TPHOLs}'99, {Nice}, {France}, {September}, 1999},
	publisher = {Springer},
	author = {Kamm{\"u}ller, Florian and Wenzel, Markus and Paulson, Lawrence C.},
	editor = {Bertot, Yves and Dowek, Gilles and Th{\'e}ry, Laurent and Hirschowitz, Andr{\'e} and Paulin-Mohring, Christine},
	year = {1999},
	pages = {149--165},
}
@article{milehins_category_2021,
	title = {Category {Theory} for {ZFC} in {HOL} {II}: {Elementary} {Theory} of 1-{Categories}},
	journal = {Archive of Formal Proofs},
	author = {Milehins, Mihails},
	year = {2021},
}
@inproceedings{caccamo_higher-order_2001,
	address = {Berlin, Heidelberg},
	title = {A {Higher}-{Order} {Calculus} for {Categories}},
	isbn = {978-3-540-44755-9},
	doi = {10.1007/3-540-44755-5_11},
	booktitle = {Theorem {Proving} in {Higher} {Order} {Logics}},
	publisher = {Springer},
	author = {C{\'a}ccamo, Mario and Winskel, Glynn},
	editor = {Boulton, Richard J. and Jackson, Paul B.},
	year = {2001},
	pages = {136--153},
}
@techreport{caccamo_higher-order_2001-1,
	address = {Aarhus, Denmark},
	title = {A {Higher}-{Order} {Calculus} for {Categories}},
	institution = {University of Aarhus},
	author = {C{\'a}ccamo, Mario Jose and Winskel, Glynn},
	year = {2001},
}
