Skip to content
An experimental framework for applied category theory
Branch: master
Clone or download
epatters Merge pull request #47 from epatters/literate-jl
Use Literate.jl to generate Jupyter notebooks and HTML documentation
Latest commit 9074de8 Sep 28, 2019
Type Name Latest commit message Commit time
Failed to load latest commit information.
docs DOC: Link to Jupyter notebooks via nbviewer in generated Markdown. Sep 27, 2019
src BUG: Handle boxes with zero inputs and zero outputs. Sep 24, 2019
test BUG: Handle boxes with zero inputs and zero outputs. Sep 24, 2019
.gitignore ENH: Allow Graphviz wire labels to be headlabels or taillabels. Apr 21, 2018
.travis.yml BUILD: Install Graphviz and LaTeX when building docs on Travis. Sep 27, 2019
Manifest.toml BUILD: Upgrade to LightGraphs v1.3. Aug 18, 2019
Project.toml BUILD: Release v0.3.0. Sep 24, 2019
REQUIRE BUILD: Record TikzPictures as an optional dependency. Aug 17, 2019


Build Status Latest Docs

Catlab is an experimental library for computational category theory, written in Julia. It aims to provide a programming library and interactive interface for applications of category theory to the mathematical sciences. It emphasizes monoidal categories due to their wide applicability but can support any categorical doctrine that is formalizable as a generalized algebraic theory. An early inspiration for Catlab is the Julia library Cateno.

Warning: This is experimental software. Important features are missing, the API is unstable, and the documentation and examples are sparse. However, it is already useable for some purposes. Contributions are welcome!

What is it?

Catlab is (or will eventually be!) the following things.

Programming library: First and foremost, Catlab provides data structures, algorithms, and serialization for applied category theory. Macros offer a convenient syntax for specifying categorical doctrines and type-safe symbolic manipulation systems. Wiring diagrams (aka string diagrams) are supported through specialized data structures and can be serialized to and from GraphML (an XML-based graph format).

Interactive computing environment: Catlab can also be used interactively in Jupyter notebooks. Symbolic expressions are displayed using LaTeX and wiring diagrams are visualized using Graphviz or TikZ. The TikZ wiring diagrams are suitable for publication.

Computer algebra system: Catlab will serve as a computer algebra system for category theory. Unlike most computer algebra systems, all expressions are typed using fragment of dependent type theory called generalized algebraic theories. We will implement core algorithms for solving word problems and reducing expressions in normal form, with respect to several important doctrines, such as the doctrine of categories and the doctrine of symmetric monoidal categories.

What is it not?

Catlab is not any of the following things. (We do not rule out that Catlab could eventually evolve in these directions but they are not our current focus.)

Automated theorem prover: Catlab is not designed to be a general-purpose automated theorem prover for category theory. Under the current plan, its proof capabilities will be confined to carefully circumscribed algebraic problems like normalization and word problems. Also, the system does not produce formal certificates of correctness (aka proofs).

Proof assistant: Likewise, Catlab is not a proof assistant because it does not produce formally verifiable proofs.

You can’t perform that action at this time.