A Computer-Checked Library of Category Theory

Universal Properties of Category Theory in Functional Programming

More Info


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.