Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time

Build Status License: AGPL v3

Idris category theory

This repository contains several definitions from category theory.

The project is written in Idris, which allows us to state properties (logical propositions) of the code, along with their formal proofs, in the code itself. These provide guarantees that the code is correct by construction.

Moreover, we are using literate Idris, so that we can seamlessly integrate code and documentation, and produce prose documentation alongside the compiled artifacts.

If you want a more detailed and slow introduction to the library, please have a look at the series of blog posts we are writing:

Nix build

If you have Nix installed, you can build the project just by doing


For additional targets, have a look at the instructions in default.nix.

If you get an error message like error: cloning builder process: Operation not permitted, run

sysctl kernel.unprivileged_userns_clone=1

as suggested in NixOS/nix#2633

Manual build


You'll need lhs2tex, latexmk and Idris.

Generate documentation

Use make to generate the PDF documentation. You will find it in the docs directory. Look directly in the Makefile for additional options.

You can also consult the documentation directly here.

Generate comparaison data with Idris2

Use make compare to output which files have not been converted to Idris2.

If the executable has already been generated, simply execute ./compare src/ idris2/ to rerun the comparaison between the two file trees.

Build code

You can build manually all the code using

idris --checkpkg idris-ct.ipkg

Build with Elba

Alternatively you can build the library with elba using

elba build

Use as a dependency

The preferred way to use this library as a dependency for another project is using elba.

It should be enough to add the following section

"statebox/idris-ct" = { git = "" }

to the elba.toml file of your project.


Unless explicitly stated otherwise all files in this repository are licensed under the GNU Affero General Public License.

Copyright © 2019 Stichting Statebox.


formally verified category theory library








No releases published


No packages published