- Working export of catt term into coq
- Computation of 1-naturality
- Computation of functorialisation
- Computation of inverses and cancellation witnesses
- Computation of opposites
- Builtin identities and compositions
- Computation of suspension and implicit suspension
- Inference of implicit variables
- Basic type checker