Catt - An infinity-categorical coherence typechecker

Catt is an implementation of a type system for coherence in Grothendieck-Maltsiniotis infinity categories.

In order to test it, you can try the web version.

This typechecker is written in OCaml, in the case you would rather like elegant Haskell, please have a look at Eric Finster's implementation.