HigherCategoryTheory

A Formalization of Higher-Order Categories in Lean 4

A formal verification project based on the work by Enric Cosme Llópez on Higher-order categories.

Overview

In many works on (Higher) Category Theory, in addition to the usual many-sorted notions of n-categories and of ω-categories, the single-sorted versions of them are also commonly used.

The aim of this project is to provide a formalization of the latter notions and the proof of their equivalence in Lean 4.

[!NOTE] For the moment, this is an active research project for a Mathematics degree final project. The project is in early stages and the following documentation is intended for self-reference only.

Development

This section documents how to set up and work with the repository.

Code editor

It is recommended to work with Visual Studio Code. We have included a .vscode directory with recommended settings and extensions.

Running tasks

Development tasks (building, documentation, etc.) are managed using Just, a command runner similar to make. To see all available recipes, run:

just

This will display a list of available commands with their descriptions. You can inspect the justfile in the root of the repository to see the detailed implementation of each recipe.

Nix setup

The development environment is configured with Nix and devenv, which automatically installs all required tools and dependencies.

To enter the development shell, run:

devenv shell

[!TIP] If using direnv, you can automatically load the development environment by running direnv allow once in the root of the repository.

Once inside the shell, all tools will be available. Run devenv info to see what's included.

Manual setup

If not using Nix, you need to manually install the following tools:

Git: Version control system.
Lean 4: Theorem prover and toolchain (recommended: install via elan).
Just: Command runner for development tasks.

For building documentation, you'll also need:

Ruby with Bundler: For Jekyll static site generation.
TeX Live: For LaTeX/PDF generation (blueprint).
leanblueprint: Tool for generating Lean blueprints.
Python: For serving the documentation website locally.

After installing Lean, cache the upstream dependencies to avoid long compilation times:

just cache

Conventions

In this section, we document the workflow and conventions used in this repository.

Commit messages

This project follows the Conventional Commits specification for commit messages. The commit message format is as follows:

<type>[optional scope]: <description>

[optional body]

[optional footer(s)]

Where <type> is one of the following: feat, fix, docs, style, refactor, test, chore, build, ci, perf, revert.

[!TIP] If working with the development environment defined with devenv, a git hook is automatically installed to check the commit messages before committing.