category-theory: an axiom-free formalization of category theory in Coq

What the formalization is actually for

The stated aim of this development is to allow representation and manipulation of categorical terms, as well as the realization of those terms in various target categories. That third word is the interesting one. The library is not only a dictionary of definitions, it is a place where a categorical construction can be moved into a category you care about and then manipulated there.

The description calls it an axiom-free formalization, and that phrase is load bearing in a proof assistant context. Everything is derived rather than assumed, which is why the coverage list can run long: comonads with their co-resolutions, Beck's monadicity theorems, orthogonal factorization systems and regular categories, coends and the profunctor calculus with Day convolution, displayed categories and the Grothendieck construction, additive and abelian structure, bicategories with the mates correspondence, pseudo double categories with companions and conjoints, enriched category theory with Sets-weighted limits, the general and special adjoint functor theorems with reflective subcategories and orthogonal localization, Lawvere theories, symmetric multicategories and operads, and elementary topos theory with a fully computable witness on skeletal finite sets.

The supported toolchain is narrow and specific. Coq 8.19 through 8.20 and Rocq 9.0 through 9.1 are supported, and some parts depend on Coq-Equations 1.2.4 through 1.3.1. The project describes itself as being for personal study and practical work, which sets the expectation: this is a working notebook that happens to be a library, not a product with a support commitment.

The directory layout encodes an argument about concepts

The library is broken into several major areas, and the way they are arranged is itself part of the design.

The core sits in Theory, covering categories, functors, natural transformations, adjunctions and kan extensions. Categorical Structure reveals the internal structure of a category by way of morphisms related to some universal property. Construction introduces external structure by building new categories out of existing ones. Alongside those, the library develops species of different kinds of functor, natural transformation, adjunction and kan extension, with the monoidal example given in the README as the model: categories with monoidal structure give rise to monoidal functors preserving that structure, which in turn leads to monoidal transformations that transform functors while preserving their monoidal mapping property.

The Instance directory defines various categories. Some are fairly general, such as the category of preorders, which applies to any PreOrder relation, while others are either not defined in terms of other categories or are sufficiently specific to stand alone.

The convention worth understanding is duplication. When a concept such as limits can be defined using more fundamental terms, that version lives in a subdirectory of the derived concept, so there is both Category.Structure.Limit and Category.Limit.Kan.Extension. The README says this is done to demonstrate the relationship of ideas, with Category.Construction.Comma.Natural.Transformation as the example. The consequence for a user is that files with the same name occur often, and the parent directory establishes intent. That is a cost you pay in search and in reading, in exchange for being able to see both the primitive and the derived version of an idea side by side.

The programming sub-library and how lawfulness is established

Inside Theory.Coq there is a sub-library aimed at applied category theory for programmers working in the category of Coq types and functions. It continues work started in the coq-haskell library, and its aim is to mimic the utility of Haskell's monad hierarchy for Coq users, in the way ext-lib does for Haskell, with a few notations adjusted to match ext-lib more closely.

What makes it interesting is a deliberate difference of approach. In this sub-library, laws are not defined for the structures. Instead the programmer establishes that her Monad is lawful by proving that a mapping exists from that definition into the general definition of monads in Theory.Monad, specialized to the category of Coq types. The rest of the category theory library is then used to discharge those proof obligations, while the programmatic side stays as simple as possible.

The README demonstrates the payoff with two proofs. The first is Compose_ApplicativeLaws, which composes two applicatives and proves the laws for the result using rewriting tactics, and the text is candid that the proof is confined to the specific case of Coq applicative endo-functors. The second, Compose_IsApplicative, takes the better route, appealing to general results: that every Coq functor has strength, that any two strong functors compose to a strong functor, and that any two lax monoidal functors compose to a lax monoidal functor.

That is the alternative approach worth naming. The obvious method is to state the laws directly for the programmatic structures and discharge them by hand, which is what the first proof does with a fair amount of tactic work. The approach this library takes instead is to make the general library do the work and prove a bridge, which costs a bridge theorem but reuses everything already proved.

Building with Nix and the Makefile targets

The easiest way to build is with Nix, and the default builds against Rocq 9.1:

    nix build
    nix build .#category-theory_8_20
    nix build .#category-theory_9_0

Those two extra outputs exist because the supported version range spans several Coq and Rocq releases, and a development that has to build against more than one of them cannot rely on a single pin.

For interactive work, nix develop opens a development shell with all the dependencies, and from there the standard Makefile is used. The main targets are make to build everything, make clean to clean build artifacts and make install to install the library. The additional development targets are make lint to check for admitted proofs and TODOs, make format-check to check for trailing whitespace, make format to fix trailing whitespace, make timing to build with per-file timing, make timing-report to show the slowest files from the last timing build, and make check to run all checks.

The per-file timing targets are a reasonable answer to a problem specific to large proof developments. Compiling a formalization of this size is slow, and knowing which files dominate is what makes the build tolerable.

Pre-commit hooks are set up with lefthook install, which requires Lefthook. The repository ships the flake, a flake.lock, a default.nix and a coq-category-theory.opam file, so the same project can be built through Nix or through the opam ecosystem.

The lint gates are the interesting engineering

In a proof assistant library, the interesting engineering is often about what is forbidden rather than what is present, and the Makefile makes the rules explicit.

The todo target greps every .v file for Fail, abort, admit, undefined and jww, excluding the definition named undefined and excluding paths under old, new and research directories. That exclusion of the research directories is a deliberate signal about how the project treats exploratory work: it is kept in the tree, but it is not part of the checked surface.

The lint target chains several checks together, namely todo, bench-config-check and claude-md-counts-check, and prints that the lint checks are complete when they pass. The format-check target greps for trailing whitespace in .v files and exits with an error when it finds any, and the format target fixes it with a perl one-liner across the tree.

The most interesting number in the repository is the aborted-sketch budget, and the Makefile explains how it is computed: the count uses the same criterion as the lefthook admitted hook and the flake admitted-check, case insensitive, with no word boundary and Admitted included, so that the three gates cannot disagree about the number. The comment records that this was a maintainer decision taken on 2026-09-06, and that before it the target used a narrower criterion.

That is a project that treats unfinished proof obligations as a budget to be managed rather than a matter of taste. There is an .admitted-baseline file in the repository root and a check/ directory, which is what makes such a budget enforceable.

Using the library from another development

Consuming this library takes two steps. You add the mapping to your _CoqProject file:

    -R <path to this library> Category

and then you import the primary elements of the library in your own development:

    Require Import Category.Theory.

The Category prefix is the load path, so the module names in the documentation translate directly into import paths, and the directory convention described earlier carries over into your file names.

The repository structure supports the same kind of exploration. There are top level directories for Adjunction, Comonad, Construction, Functor, Monad, Natural, Structure, Solver and Tools, plus a Lib directory, a Theory.v file that is presumably the umbrella import, and a Test directory for the test suite. The Tools directory and the Solver directory are the parts worth a look if you want to see the library used rather than defined.

Two other things in the tree describe how the project is worked on. There is a CLAUDE.md file, which in this ecosystem usually holds the conventions and instructions for automated coding assistants, and the Makefile has a claude-md-counts-check target that keeps that file consistent. There is also a doc/ and a docs/ directory, and a check/ directory for the lint gates.

Where this library is the wrong tool

Three situations point elsewhere.

The first is a team that wants to use categorical ideas rather than prove them. This library is a formalization: the value is that the results are checked, and the cost is that the results are large, that reading them takes time, and that the toolchain is constrained to a narrow range of Coq and Rocq versions with a dependency on Coq-Equations for some parts. A general purpose library of monads and adjunctions in your language of choice will be easier to adopt and will not give you the proofs.

The second is a project that has to move quickly across Coq versions. The supported range is Coq 8.19 to 8.20 and Rocq 9.0 to 9.1, and the Nix outputs exist per version, which tells you the maintenance cost is real rather than theoretical.

The third is anyone expecting a stable, versioned API. The repository has exactly one tagged release, 1.0.0, dated 2022-08-19, while the last push was on 2026-10-08. The code moves and the release line does not, so a consumer pinning to a released version gets a snapshot that is several years behind the working tree.

That last point is the one to weigh. The library is described as being for personal study and practical work, and the dense directory structure with duplicated concepts is well suited to reading and learning. For a production dependency, the absence of releases and the wide coverage make it a research base rather than a stable package.

Editorial conclusion

Adopt this library if you are working in Coq or Rocq on categorical constructions, if you want monads, adjunctions, kan extensions and related machinery with proofs rather than documentation, or if you want a practitioner friendly programming sub-library for Coq types and functions. Do not adopt it if you want a compact, quickly learned API, because the breadth of the formalization is the point and the cost is size, or if your toolchain cannot take Coq 8.19 to 8.20 and Rocq 9.0 to 9.1 with Coq-Equations 1.2.4 to 1.3.1. Verify three things first: that the version you build against matches the one your development uses, since the Nix outputs differ per Coq and Rocq release; that the lint targets pass, because make lint checks for admitted proofs and TODOs and the repository carries an admitted baseline and an aborted sketch budget; and whether the piece you need is defined in the general library or in the derived subdirectory, since the library deliberately keeps both versions to show the relationship between them. The licence is BSD-3-Clause, the only tagged release is 1.0.0 dated 2022-08-19, and the last push was on 2026-10-08.

Frequently asked questions

Official sources

1. Issues
2. jwiegley/category-theory on GitHub
3. License: BSD-3-Clause
4. README
5. Releases