A computer-checked library of category theory

A computer-checked library of category theory: Defining functors and their algebras

Todorov, Rado (TU Delft Electrical Engineering, Mathematics and Computer Science)

Ahrens, B.P. (mentor)
Escot, L.F.B. (mentor)
Liang, K. (graduation committee)

Delft University of Technology

Computer Science and Engineering

CSE3000 Research Project

2023-06-27

Category theory is a branch of abstract mathematics that aims to give a high-level overview of relations between objects. Proof assistants are tools that aid in verifying the correctness of mathematical proofs. To reason about category theory using such assistants, fundamental notions have to be defined. Computer-checked libraries contain all relevant structures and theorems in an accessible way for end users. However, current libraries of category theory are not welcoming to people without in-depth domain knowledge. This paper introduces a library of category theory tailored towards newcomers to the field as well as the learning journey of the authors. We describe the project’s structure, design choices and provide examples of the main features. Moreover, a detailed overview is provided of F-algebras and their relation with inductive data types found in functional programming languages. Construction and evaluation of types like lists and binary trees can be defined in terms of algebras. They provide a general framework for recursion over these types which allow us to reason about them with simple functions.

Category theory
Functional Programming
Proof assistant

http://resolver.tudelft.nl/uuid:526ed078-f8be-4a3e-a711-e5729082a589

Student theses

bachelor thesis

© 2023 Rado Todorov