A formalization of category theory that supports commutative diagrams as described here. Build with: git submodule init git submodule update make