package catt

1.0 (2024-10)

Coq catt plugin

• Working export of catt term into coq

Catt

• 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