TypeTheory
TypeTheory copied to clipboard
UniMath
The mathematical study of type theories, in univalent foundations
Make sure each definition of a structure is carefully referenced — citation to somewhere giving _that precise form_ of the definition, where possible.
Provide a summary file which re-exports the whole library (or perhaps individual packages?), for easier wholesale importing by others.
In CI, it was visible that Coq dev (an alpha version of Coq 8.21) does not compile this satellite, but it is even worse. The first error message is: ``coqc...
