/catt

Coherence typechecker for Grothendieck/Maltsiniotis style infinity categories

Primary LanguageHaskellMIT LicenseMIT

Catt - An infinity-categorical coherence typechecker

Catt is an implementation of a type system for coherence in Grothendieck/Maltsiniotis style infinity categories, whose theory is outline here.

Building

You will need the bnfc converter to generate the syntax. Follow the instructions on the site to install the tool on your machine

  1. Clone the repository
  2. Run the "regen" script in the src directory to generate the grammar
  3. In the repo directory, run "cabal build"

You can then try out some of the examples in the examples directory.