Benedikt Ahrens
Benedikt Ahrens
We should activate all warnings, to be motivated to keep our code in good shape. Currently, we have ``` -w '-notation-overridden,-local-declaration,+uniform-inheritance,-deprecated-option' ``` We should replace that by ``` -w all...
in CT.categories.grs, morphisms of groups are defined to be monoid morphisms - probably this is a trick with the goal of making the proof of univalence easier. While this is...
Point to emacs configuration file template relates to #1537
``` --- checking the ordering prescribed by the files UniMath/*/.packages/files --- make: bash: Argument list too long make: *** [Makefile:330: .check-prescribed-ordering.okay] Error 127 ``` at https://github.com/UniMath/UniMath/actions/runs/7396394616/job/20121464106?pr=1817, when checking PR https://github.com/UniMath/UniMath/pull/1817....
I am seeing this error on Debian: ``` $ make install ulimit -v unlimited ; make -f build/CoqMakefile.make all make[1]: Entering directory '/home/ahrens/github/UniMath/UniMath' make[2]: Nothing to be done for 'real-all'....
@mikeshulman suggested that the systematic use of `PathOver` (Mike also called it "displayed identity") could simplify definitions and constructions of displayed things. It would be great to try it out.
They are both in Foundations/PartA. One of them should be removed.
It seems to me that this file shows what happens when one does not use access functions. Could we add access functions instead of those projections? _Originally posted by @benediktahrens...
Jason Gross has a bug minimizer that aims to produce a minimal Coq file reproducing a given Coq error, using a brute-force approach. Using a similar approach, we could try...
https://unimath.org is timing out. @DanGrayson : could you take a look? Thanks to @tomdjong for the notification!