@book{MacLane,
  author    = {Mac Lane, Saunders},
  title     = {Categories for the working mathematician},
  series    = {Graduate Texts in Mathematics},
  volume    = {5},
  edition   = {Second},
  publisher = {Springer-Verlag, New York},
  year      = {1998},
  pages     = {xii+314},
  isbn      = {0-387-98403-8},
  mrclass   = {18-02},
  mrnumber  = {1712872}
}

@misc{CT4P,
  author = {Benedikt Ahrens and Kobe Wullaert},
  title  = {Category Theory for Programming},
  year   = {2023},
  eprint = {arXiv:2209.01259}
}

@book{Kashiwara,
  author     = {Kashiwara, Masaki and Schapira, Pierre},
  title      = {Categories and sheaves},
  series     = {Grundlehren der mathematischen Wissenschaften [Fundamental
                Principles of Mathematical Sciences]},
  volume     = {332},
  publisher  = {Springer-Verlag, Berlin},
  year       = {2006},
  pages      = {x+497},
  isbn       = {978-3-540-27949-5; 3-540-27949-0},
  mrclass    = {18-02 (14F05 18F20)},
  mrnumber   = {2182076},
  mrreviewer = {Corrado\ Marastoni},
  doi        = {10.1007/3-540-27950-4},
  url        = {https://doi.org/10.1007/3-540-27950-4}
}

@article{Hyland,
  title     = {Classical lambda calculus in modern dress},
  volume    = {27},
  doi       = {10.1017/S0960129515000377},
  number    = {5},
  journal   = {Mathematical Structures in Computer Science},
  publisher = {Cambridge University Press},
  author    = {Hyland, J.M.E.},
  year      = {2017},
  pages     = {762–781}
}

@book{algebraic-theories-2010,
  place      = {Cambridge},
  series     = {Cambridge Tracts in Mathematics},
  title      = {Algebraic Theories: A Categorical Introduction to General Algebra},
  doi        = {10.1017/CBO9780511760754},
  publisher  = {Cambridge University Press},
  author     = {Adámek, J. and Rosický, J. and Vitale, E. M.},
  year       = {2010},
  collection = {Cambridge Tracts in Mathematics}
}

@book{higher-operads,
  place      = {Cambridge},
  series     = {London Mathematical Society Lecture Note Series},
  title      = {Higher Operads, Higher Categories},
  doi        = {10.1017/CBO9780511525896},
  publisher  = {Cambridge University Press},
  author     = {Leinster, Tom},
  year       = {2004},
  collection = {London Mathematical Society Lecture Note Series}
}

@book{curry,
  title     = {To H.B. Curry: Essays on Combinatory Logic and Formalism},
  editor    = {Seldin, J. P. and Hindley, J. R.},
  publisher = {Academic Press},
  month     = sep,
  year      = 1980,
  address   = {San Diego, CA},
  language  = {en}
}

@article{monads-endofunctors,
  author       = {Thosten Altenkirch and James Chapman and Tarmo Uustalu},
  title        = {Monads need not be endofunctors},
  year         = {2014},
  eprint       = {arXiv:1412.7148},
  howpublished = {Logical Methods in Computer Science, Volume 11, Issue 1 (March 6,
                  2015) lmcs:928},
  doi          = {10.2168/LMCS-11(1:3)2015}
}

@article{lambda-monoid,
  title    = {Towards a Notion of Lambda Monoid},
  journal  = {Electronic Notes in Theoretical Computer Science},
  volume   = {303},
  pages    = {59-77},
  year     = {2014},
  note     = {Proceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013)},
  issn     = {1571-0661},
  doi      = {https://doi.org/10.1016/j.entcs.2014.02.004},
  url      = {https://www.sciencedirect.com/science/article/pii/S1571066114000309},
  author   = {Martin Hyland},
  keywords = {Algebraic theories, Abstract clones, -calculus, Reflexive objects, Λ-monoids},
  abstract = {Any interpretation of the lambda calculus determines a composition monoid and this monoid can be equipped with structure from which the interpretation can be recovered. That is the essence of Dana Scott's account of the lambda calculus in terms of its category of retracts. This paper presents a new approach to the needed structure on the monoid deriving from a recent analysis of the lambda calculus in terms of algebraic theory.}
}

@misc{nlab:grothendieck_fibration,
  author       = {{nLab authors}},
  title        = {{{G}}rothendieck fibration},
  howpublished = {\url{https://ncatlab.org/nlab/show/Grothendieck+fibration}},
  note         = {\href{https://ncatlab.org/nlab/revision/Grothendieck+fibration/113}{Revision 113}},
  month        = feb,
  year         = 2024
}

 @misc{nlab:adjoint_equivalence,
  author       = {{nLab authors}},
  title        = {adjoint equivalence},
  howpublished = {\url{https://ncatlab.org/nlab/show/adjoint+equivalence}},
  note         = {\href{https://ncatlab.org/nlab/revision/adjoint+equivalence/17}{Revision 17}},
  month        = may,
  year         = 2024
}

@misc{stackexchange:yoneda-exponentials,
  title        = {Show that the Yoneda embedding preserves exponential objects},
  author       = {Mark Kamsma},
  howpublished = {Mathematics Stack Exchange},
  note         = {URL:https://math.stackexchange.com/q/3511278 (version: 2022-12-20)},
  eprint       = {https://math.stackexchange.com/q/3511278},
  url          = {https://math.stackexchange.com/q/3511278}
}

@phdthesis{taylor,
  author = {Paul Taylor},
  title  = {Recursive Domains, Indexed Category Theory and Polymorphism},
  school = {University of Cambridge},
  year   = {1986}
}

@misc{strachey,
  author       = {Dana S. Scott},
  title        = {Greetings to the Participants at “Strachey 100”},
  year         = {2016},
  note         = {A talk read out at the Strachey 100 centenary conference},
  howpublished = {\url{https://www.cs.ox.ac.uk/strachey100/Strachey_booklet.pdf}}
}

@inproceedings{scott-continuous,
  author    = {Scott, Dana},
  editor    = {Lawvere, F. W.},
  title     = {Continuous lattices},
  booktitle = {Toposes, Algebraic Geometry and Logic},
  year      = {1972},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  pages     = {97--136},
  url       = {http://dx.doi.org/10.1007/BFb0073967},
  abstract  = {Starting from the topological point of view a certain wide class of To-spaces is introduced having a very strong extension property for continuous functions with values in these spaces. It is then shown that all such spaces are complete lattices whose lattice structure determines the topology --- these are the continuous lattices --- and every such lattice has the extension property. With this foundation the lattices are studied in detail with respect to projections, subspaces, embeddings, and constructions such as products, sums, function spaces, and inverse limits. The main result of the paper is a proof that every topological space can be embedded in a continuous lattice which is homeomorphic (and isomorphic) to its own function space. The function algebra of such spaces provides mathematical models for the Church-Curry $\lambda$-calculus.},
  isbn      = {978-3-540-37609-5}
}

@article{freyd,
  title     = {Aspects of topoi},
  volume    = {7},
  doi       = {10.1017/S0004972700044828},
  url       = {http://dx.doi.org/10.1017/S0004972700044828},
  number    = {1},
  journal   = {Bulletin of the Australian Mathematical Society},
  author    = {Freyd, Peter},
  year      = {1972},
  month     = aug,
  pages     = {1–76},
  issn      = {1755-1633},
  publisher = {Cambridge University Press (CUP)}
}

@article{theory-of-constructions,
  title     = {The theory of constructions: Categorical semantics and topos-theoretic models},
  author    = {Hyland,  J. Martin E. and Pitts,  Andrew M.},
  journal   = {Contemporary Mathematics},
  volume    = {92},
  pages     = {137–199},
  year      = {1989},
  isbn      = {0821851004},
  doi       = {10.1090/conm/092/1003199},
  url       = {http://dx.doi.org/10.1090/conm/092/1003199},
  publisher = {American Mathematical Society}
}

@unpublished{martin-lof-type-theory,
  author = {Martin-Löf, Per},
  note   = {Preprint, Stockholm University},
  title  = {A theory of types},
  year   = {1971}
}

@book{hottbook,
  author    = {The {Univalent Foundations Program}},
  title     = {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {\url{https://homotopytypetheory.org/book}},
  address   = {Institute for Advanced Study},
  year      = 2013
}

@article{univalent-categories,
  title     = {Univalent categories and the Rezk completion},
  volume    = {25},
  issn      = {1469-8072},
  url       = {http://dx.doi.org/10.1017/S0960129514000486},
  doi       = {10.1017/s0960129514000486},
  number    = {5},
  journal   = {Mathematical Structures in Computer Science},
  publisher = {Cambridge University Press (CUP)},
  author    = {Ahrens, Benedikt and Kapulkin, Krzysztof and Shulman, Michael},
  year      = {2015},
  month     = jan,
  pages     = {1010–1039}
}

@misc{circle-fundamental-group,
  title         = {Construction of the Circle in UniMath},
  author        = {Marc Bezem and Ulrik Buchholtz and Daniel R. Grayson and Michael Shulman},
  year          = {2020},
  eprint        = {1910.01856},
  archiveprefix = {arXiv},
  primaryclass  = {math.LO}
}

@inproceedings{girard,
  author    = {Hurkens, Antonius J. C.},
  editor    = {Dezani-Ciancaglini, Mariangiola
               and Plotkin, Gordon},
  title     = {A simplification of Girard's paradox},
  booktitle = {Typed Lambda Calculi and Applications},
  year      = {1995},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  pages     = {266--278},
  abstract  = {In 1972 J.-Y. Girard showed that the Burali-Forti paradox can be formalised in the type system U. In 1991 Th. Coquand formalised another paradox in U−. The corresponding proof terms (that have no normal form) are large. We present a shorter term of type ⊥ in the Pure Type System $\lambda$U− and analyse its reduction behaviour. The idea is to construct a universe U and two functions such that a certain equality holds. Using this equality, we prove and disprove that a certain object in U is well-founded.},
  isbn      = {978-3-540-49178-1}
}

@inproceedings{lawvere-fixpoints,
  author    = {Lawvere, F. William},
  title     = {Diagonal arguments and cartesian closed categories},
  booktitle = {Category Theory, Homology Theory and their Applications II},
  year      = {1969},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  pages     = {134--145},
  isbn      = {978-3-540-36101-5},
  doi       = {https://doi.org/10.1007/BFb0080769}
}

@book{borceux,
  place      = {Cambridge},
  series     = {Encyclopedia of Mathematics and its Applications},
  title      = {Handbook of Categorical Algebra},
  publisher  = {Cambridge University Press},
  author     = {Borceux, Francis},
  year       = {1994},
  collection = {Encyclopedia of Mathematics and its Applications}
}

@book{riehl,
  place      = {Cambridge},
  series     = {New Mathematical Monographs},
  title      = {Categorical Homotopy Theory},
  publisher  = {Cambridge University Press},
  author     = {Riehl, Emily},
  year       = {2014},
  collection = {New Mathematical Monographs}
}

@article{hayashi-1985-semifunctors,
  title    = {Adjunction of semifunctors: Categorical structures in nonextensional lambda calculus},
  journal  = {Theoretical Computer Science},
  volume   = {41},
  pages    = {95-104},
  year     = {1985},
  issn     = {0304-3975},
  doi      = {https://doi.org/10.1016/0304-3975(85)90062-3},
  url      = {https://www.sciencedirect.com/science/article/pii/0304397585900623},
  author   = {Susumu Hayashi},
  abstract = {Some connections between λ-calculus and category theory have been known. Among them, it has been shown by Lambek that cartesian closed categories (ccc for short) can be identified with extensional typed λ-calculus (cf. Lambek (1980), and Lambek and Scott (1986)). In this paper we introduce the notion of adjunction of semifunctors (for simplicity, we refer to this as ‘semiadjunction’) and, by the aid of this notion, we define the notion of semi cartesian closed category (semi-ccc for short). Some categorical or algebraic systems aimed to represent λ-calculus will turn out to be special cases of semi-ccc. Another intersting connection between ccc and λ-calculus is Scott's embedding of λ-theory into a ccc (cf. Scott (1980)). (This will be referred to as Scott embedding.) We will show that any semiadjunction is embeddable in an adjunction (of functors) and Scott embedding is a special case.}
}

@misc{hoofman-1993-semi-cartesian-closed,
  author       = {Hoofman, Raymond and Harold Schellinx},
  title        = {Models of the untyped lambda-calculus in semi cartesian closed categories},
  year         = {1993},
  month        = {2},
  howpublished = {ILLC Prepublication Series for Mathematical Logic and Foundations, ML-93-05},
  institution  = {Institute for Logic, Language and Computation},
  eprint       = {https://eprints.illc.uva.nl/id/eprint/1329/1/ML-1993-05.text.pdf}
}

@article{selinger-lambda-calculus-algebraic,
  title   = {The lambda calculus is algebraic},
  volume  = {12},
  doi     = {10.1017/S0956796801004294},
  number  = {6},
  journal = {Journal of Functional Programming},
  author  = {Selinger, Peter},
  year    = {2002},
  pages   = {549–566}
}

@inbook{MacLane-Moerdijk,
  author    = {Mac Lane, Saunders
               and Moerdijk, Ieke},
  title     = {Categories of Functors},
  booktitle = {Sheaves in Geometry and Logic: A First Introduction to Topos Theory},
  year      = {1994},
  publisher = {Springer New York},
  address   = {New York, NY},
  pages     = {24--63},
  abstract  = {Many constructions on various mathematical objects depend not just on the elements of those objects but also on the morphisms between them. Such constructions can thus be effectively formulated in the corresponding category of objects. A ``topos'' is a category in which a number of the most basic such constructions (product, pullback, exponential, characteristic function,{\ldots}) are always possible. With these constructions available, many other properties can be efficiently developed. Superficially quite different categories, arising in geometry, topology, algebraic geometry, group representations, and set theory, all turn out to satisfy the axioms defining such a topos.},
  isbn      = {978-1-4612-0927-0},
  doi       = {10.1007/978-1-4612-0927-0_3},
  url       = {https://doi.org/10.1007/978-1-4612-0927-0_3}
}

@article{displayed-categories,
  title    = {{Displayed Categories}},
  author   = {Benedikt Ahrens and Peter LeFanu Lumsdaine},
  url      = {https://lmcs.episciences.org/5252},
  doi      = {10.23638/LMCS-15(1:20)2019},
  journal  = {{Logical Methods in Computer Science}},
  volume   = {{Volume 15, Issue 1}},
  year     = {2019},
  month    = Mar,
  keywords = {Mathematics - Category Theory ; Mathematics - Logic ; 18A15, 03B15, 03B70 ; F.4.1},
  eprint       = {arXiv:1705.04296},
}

@misc{simplicial-set-model,
  title         = {The Simplicial Model of Univalent Foundations (after Voevodsky)},
  author        = {Chris Kapulkin and Peter LeFanu Lumsdaine},
  year          = {2018},
  eprint        = {1211.2851},
  archiveprefix = {arXiv},
  primaryclass  = {math.LO},
  url           = {https://arxiv.org/abs/1211.2851}
}

@inproceedings{proof-irrelevant-model,
  author    = {Miquel, Alexandre
               and Werner, Benjamin},
  editor    = {Geuvers, Herman
               and Wiedijk, Freek},
  title     = {The Not So Simple Proof-Irrelevant Model of CC},
  booktitle = {Types for Proofs and Programs},
  year      = {2003},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  pages     = {240--258},
  abstract  = {It is well-known that the Calculus of Constructions (CC) bears a simple set-theoretical model in which proof-terms are mapped onto a single object---a property which is known as proof-irrelevance. In this paper, we show that when going into the (generally omitted) technical details, this naive model raises several unexpected difficulties related to the interpretation of the impredicative level, especially for the soundness property which is surprisingly difficult to be given a correct proof in this simple framework. We propose a way to tackle these difficulties, thus giving a (more) detailed elementary consistency proof of CC without going back to a translation to F$\omega$. We also discuss some possible alternatives and possible extensions of our construction.},
  isbn      = {978-3-540-39185-2}
}

@article{church-lambda-calculus,
  issn      = {0003486X, 19398980},
  url       = {http://www.jstor.org/stable/1968337},
  author    = {Alonzo Church},
  journal   = {Annals of Mathematics},
  number    = {2},
  pages     = {346--366},
  publisher = {[Annals of Mathematics, Trustees of Princeton University on Behalf of the Annals of Mathematics, Mathematics Department, Princeton University]},
  title     = {A Set of Postulates for the Foundation of Logic},
  urldate   = {2024-09-25},
  volume    = {33},
  year      = {1932}
}

@article{church-number-theory,
  issn      = {00029327, 10806377},
  url       = {http://www.jstor.org/stable/2371045},
  author    = {Alonzo Church},
  journal   = {American Journal of Mathematics},
  number    = {2},
  pages     = {345--363},
  publisher = {The Johns Hopkins University Press},
  title     = {An Unsolvable Problem of Elementary Number Theory},
  urldate   = {2024-09-25},
  volume    = {58},
  year      = {1936}
}

@article{kleene-lambda,
  title     = {λ-definability and recursiveness},
  volume    = {2},
  issn      = {0012-7094},
  url       = {http://dx.doi.org/10.1215/s0012-7094-36-00227-2},
  doi       = {10.1215/s0012-7094-36-00227-2},
  number    = {2},
  journal   = {Duke Mathematical Journal},
  publisher = {Duke University Press},
  author    = {Kleene,  S. C.},
  year      = {1936},
  month     = jun
}

@article{turing-lambda,
  issn      = {00224812},
  url       = {http://www.jstor.org/stable/2268280},
  author    = {A. M. Turing},
  journal   = {The Journal of Symbolic Logic},
  number    = {4},
  pages     = {153--163},
  publisher = {[Association for Symbolic Logic, Cambridge University Press]},
  title     = {Computability and λ-Definability},
  urldate   = {2024-09-25},
  volume    = {2},
  year      = {1937}
}

@misc{python-expressions,
  url     = {https://docs.python.org/3/reference/expressions.html#lambda},
  journal = {The Python Language Reference},
  author  = {Python Software Foundation, The},
  year    = {2024},
  month   = {10}
}

@misc{java-lambdas,
  url     = {https://docs.oracle.com/javase/tutorial/java/javaOO/lambdaexpressions.html},
  journal = {The JavaTM Tutorials},
  author  = {Oracle},
  year    = {2022}
}

@misc{voevodsky-univalent-foundations,
  title         = {Experimental library of univalent formalization of mathematics},
  author        = {Vladimir Voevodsky},
  year          = {2014},
  eprint        = {1401.0053},
  archiveprefix = {arXiv},
  primaryclass  = {math.HO},
  url           = {https://arxiv.org/abs/1401.0053}
}

@incollection{Lawvere-Karoubi,
  author     = {Lawvere, F. William},
  title      = {Qualitative distinctions between some toposes of generalized
                graphs},
  booktitle  = {Categories in computer science and logic ({B}oulder, {CO},
                1987)},
  series     = {Contemp. Math.},
  volume     = {92},
  pages      = {261--299},
  publisher  = {Amer. Math. Soc., Providence, RI},
  year       = {1989},
  isbn       = {0-8218-5100-4},
  mrclass    = {18B25 (54C40)},
  mrnumber   = {1003203},
  mrreviewer = {Kimmo\ I.\ Rosenthal},
  doi        = {10.1090/conm/092/1003203},
  url        = {https://doi.org/10.1090/conm/092/1003203}
}

@article{four-color-theorem,
  author    = {K. Appel and W. Haken},
  title     = {{Every planar map is four colorable}},
  volume    = {82},
  journal   = {Bulletin of the American Mathematical Society},
  number    = {5},
  publisher = {American Mathematical Society},
  pages     = {711 -- 712},
  year      = {1976}
}

@misc{Kepler-conjecture,
  title         = {The Kepler conjecture},
  author        = {Thomas C. Hales},
  year          = {2002},
  eprint        = {math/9811078},
  archiveprefix = {arXiv},
  primaryclass  = {math.MG},
  url           = {https://arxiv.org/abs/math/9811078}
}

@inproceedings{formalized-four-color-theorem,
  author    = {Gonthier, Georges},
  editor    = {Kapur, Deepak},
  title     = {The Four Colour Theorem: Engineering of a Formal Proof},
  booktitle = {Computer Mathematics},
  year      = {2008},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  pages     = {333--333},
  abstract  = {The 150 year old Four Colour Theorem is the first famous result with a proof that requires large computer calculations. Such proofs are still controversial: It is thought that computer programs cannot be reviewed with mathematical rigor.},
  isbn      = {978-3-540-87827-8}
}


@article{formalized-Kepler-conjecture,
  title   = {A Formal Proof of the Kepler Conjecture},
  volume  = {5},
  doi     = {10.1017/fmp.2017.1},
  journal = {Forum of Mathematics, Pi},
  author  = {Hales, Thomas and Adams, Mark and Bauer, Gertrud and Dang, Tat Dat and Harrison, John and Hoang, Le Truong and Kaliszyk, Cezary and Magron, Victor and McLaughlin, Sean and Nguyen, Tat Thang and et al.},
  year    = {2017},
  pages   = {e2}
}

@article{Zermelo-set-theory,
  title     = {Untersuchungen über die Grundlagen der Mengenlehre. I},
  volume    = {65},
  issn      = {1432-1807},
  url       = {http://dx.doi.org/10.1007/BF01449999},
  doi       = {10.1007/bf01449999},
  number    = {2},
  journal   = {Mathematische Annalen},
  publisher = {Springer Science and Business Media LLC},
  author    = {Zermelo,  E.},
  year      = {1908},
  month     = jun,
  pages     = {261–281}
}

@book{Russell-type-theory,
  author    = {Bertrand Russell},
  publisher = {University Press},
  address   = {Cambridge},
  title     = {The Principles of Mathematics},
  year      = {1903},
  language  = {English}
}