Comparison between CaTT generated EH and HoTT EH

This is not a release of the software. This is the exact conditions that were used to compare the Eckmann-Hilton generated by CaTT in Coq with the one present in the HoTT library, for reproducibility.

1.0

CHANGES:

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

Support for basic theory and easier constructs

First feature-complete release.

I do not expect to publish it anywhere, but it marks a milestone where we have reached a feature-complete state, where catt is actually usable in a reasonably convenient way