A computer-checked library of category theory: Formally verifying currying via the product-exponential adjunction

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...

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

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...