This repository implements an experimental typechecker for the languages Catt, Catt_su, and Catt_sua; type theories which model various semi-strictifications of higher categories (see this thesis). The typechecker here uses a bidirectional type checking algorithm to perform inference and utilises NbE to reduce terms to normal forms.
The tool can be built with cargo, and should require no extra dependencies. A development environment is also provided through a nix flake with the correct versions of each tool, but it should not be necessary to use this.
To install locally run:
cargo installalternatively, one can run cargo run from the build directory to directly compile and run the executable instead of installing it.
To see all the available options run:
catt_strict --helpFiles can be typechecked by adding them as command line arguments:
catt_strict examples/eh.catt examples/monoidal.cattTo turn on "sua" (or "su") normalisation, add the --sua (or --su) flag:
catt_strict --sua examples/syllepsis.cattThe -i flag starts an interactive command line REPL.
The tool comes with a very primitive LSP server, which supports reporting diagnostics for parsing and type errors. The server can be activated with the --lsp flag. Enabling this within your editor will be editor specific.