Print Email Facebook Twitter A computer-checked library of category theory Title A computer-checked library of category theory: Formally verifying currying via the product-exponential adjunction Author Stanciu, Ciprian (TU Delft Electrical Engineering, Mathematics and Computer Science; TU Delft Programming Languages) Contributor Ahrens, B.P. (mentor) Escot, L.F.B. (mentor) Liang, K. (graduation committee) Degree granting institution Delft University of Technology Programme Computer Science and Engineering Project CSE3000 Research Project Date 2023-06-27 Abstract Existing implementations of category theory for proof assistants aim to be as generic as possible in order to be reusable and extensible, often at the expense of readability and clarity. We present a (partial) formalisation of category theory in the proof assistant Lean limited in purpose to explaining currying, intended to be faithful to the language and definitions used in mathematics literature. We also present some design features of our library and contrast the extent and educational merit with other implementations. Subject Category theoryProof assistantFunctional Programming To reference this document use: http://resolver.tudelft.nl/uuid:1f6d6c5e-54e3-4c26-a1be-79de08653f9c Part of collection Student theses Document type bachelor thesis Rights © 2023 Ciprian Stanciu Files PDF Final_paper.pdf 181.43 KB Close viewer /islandora/object/uuid:1f6d6c5e-54e3-4c26-a1be-79de08653f9c/datastream/OBJ/view