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