The goal of this (personal) project is to establish the following goals with Lean 4:
- implementation of unbiased monoidal categories;
- proof of the coherence theorem that every (biased) monoidal category is an instance of an unbiased one;
- formalization of so-called "graphical calculus" on (unbiased) monoidal categories.
The project is released under Apache License (version 2.0); see LICENSE file.
The project heavily depends on Mathlib4 project. As it (and Lean 4 itself) are in Work-in-Progress state, keep in mind that the "validity" of the proofs in the proejct are unstable.