A Computer-Checked Library of Category Theory

Universal Properties of Category Theory in Functional Programming

Bachelor thesis (2023)

Authors

M. Orav Electrical Engineering, Mathematics and Computer Science

Contributors

B.P. Ahrens Programming Languages - EEMCS (mentor)
L.F.B. Escot Programming Languages - EEMCS (mentor)
K. Liang Cyber Security - EEMCS (graduation committee member)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
Copyright: © 2023 Markus Orav
More Info
expand_more

Published Date

27-06-2023

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

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.

Files

Research_Project_Markus_Orav.p... (pdf)
(pdf | 0.293 Mb)
Unknown license