Print Email Facebook Twitter A Computer-Checked Library of Category Theory Title A Computer-Checked Library of Category Theory: Universal Properties of Category Theory in Functional Programming Author Orav, Markus (TU Delft Electrical Engineering, Mathematics and Computer Science) 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 Category theory is a branch of mathematics that is used to abstract and generalize other mathematical concepts. Its core idea is to take the emphasis off the details of the elements of these concepts and put it on the relationships between them instead. The elements can then be characterized in terms of their relationships using various universal properties. The goal of this project was to implement a pedagogical library of category theory in the computer proof assistant Lean, a software tool for formalizing mathematics, and provide a different perspective on various functional programming concepts by finding parallels between them and the universal properties of category theory. Subject category theoryuniversal propertiescomputer proof assistantsLeanfunctional programminginitial objectsterminal objectsbinary productsbinary coproducts To reference this document use: http://resolver.tudelft.nl/uuid:97c4e6b6-971c-4437-aa18-a3997f316a02 Part of collection Student theses Document type bachelor thesis Rights © 2023 Markus Orav Files PDF Research_Project_Markus_Orav.pdf 300.46 KB Close viewer /islandora/object/uuid:97c4e6b6-971c-4437-aa18-a3997f316a02/datastream/OBJ/view