A Formalization of Higher-Order Categories in Lean 4

Introduction

What is a formalization project?

A formalization project is an effort to translate mathematical definitions, theorems, and proofs into a formal language that can be verified by a computer proof assistant. In this project, we use Lean 4, a theorem prover and programming language developed at Microsoft Research with Leonardo de Moura as the lead developer. Lean is particularly well-suited for formalizing modern mathematics.

What is this docuemnt?

This document is a blueprint for a formalization project in Lean 4. A blueprint serves as a roadmap for mathematical formalization, providing a human-readable mathematical exposition alongside references to the corresponding formal code. It acts as a bridge between traditional mathematical writing and computer-verified proofs, allowing us to understand the mathematical content while tracking the progress of its formalization. Refer to the official https://github.com/PatrickMassot/leanblueprintLean Blueprint GitHub repository for more information on blueprints.

What is this project about?

This project formalizes the theory of higher-order categories and their different presentations. Specifically, we formalize:

  1. Single-sorted categories: Where objects, morphisms, 2-morphisms, and higher morphisms all live in a single type.

  2. Many-sorted categories: The traditional presentation where objects, morphisms, and higher morphisms live in separate types.

  3. The equivalence between these presentations: Proving that these two approaches of higher-order categories are equivalent.

This project is based on the work by Enric Cosme Llópez and Raul Ruiz Mora in [ 1 ] .