Benedikt Ahrens
Benedikt Ahrens
We have different ways to name builder functions, e.g., there are `makecategory` and `mk_precategory`. We should have one way, e.g., always use prefix `mk_`.
thanks to @tomdjong for pointing it out.
That lengthy section is cluttering the INSTALL, which should be short and clean. It should be moved to a separate file, with a link to it in INSTALL.md It might...
CategoryTheory is the package with the longest compile time. It seems reasonable to split it into several (here: two).
Headers should describe content and its provenance.
To be done at the end of the import from https://github.com/nmvdw/groupoids.
It has been advertised to never close proofs with `Qed`, and to opacify with `Opaque` afterwards instead. It has also been pointed out that those two options are not equivalent....
The style guide should mention a ban on automated proofs. Relying on automation makes debugging a problem harder when it occurs, e.g., when switching to a new version of Coq....
The file https://github.com/UniMath/TypeTheory/blob/master/TypeTheory/Auxiliary/Auxiliary.v contains stuff on - Foundations (equivalences of types, transport - Adjunctions and equivalences of categories which should be upstreamed asap, to avoid (further) duplication of efforts (see...
While a functorial action can be derived from the substitution of relative monads (and modules), it seems good both for structuring the definitions as well as for working with the...