Benedikt Ahrens
Benedikt Ahrens
explain that - location of Coq binaries needs to be given manually (by PATH or locally) - UniMath files are found automatically after `make install` if using the right Coq...
In Fibrations.v, it reads "We make the cloven version the default, so is_fibration etc are the cloven notions, and call the mere-existence versions un-cloven." So `is_fibration` is actually a structure,...
Some links point to old repository - can they be made relative?
Does `Parameter` yield an axiom? The documentation seems to say so: https://coq.inria.fr/doc/V8.19.0/refman/language/core/assumptions.html#coq:cmd.Parameter In this case, we do not want `Parameter`. _Originally posted by @benediktahrens in https://github.com/UniMath/UniMath/issues/1874#issuecomment-2050168552_
``` File "./UniMath/AlgebraicTheories/LambdaTheories.v", line 227, characters 0-76: Warning: Variable π does not occur in the right-hand side. The notation will not be used for printing as it is not reversible....
I would feel much better if I knew that UniMath were backed up regularly. By "backup", I mean a clone of the repository being taken every day, tarballed and stored...
The material at https://github.com/UniMath/Schools should be added to UniMath CI, so that it is always compatible with current UniMath.
We are using the booleans of Coq.Init.Datatypes, which are defined as an inductive type: ``` Inductive bool : Set := | true : bool | false : bool. ``` Should...
Recent outage of bitbucket (a github-like service) made me think about having a mirror of the UniMath repository. A mirror is a copy of the UniMath repository that is synced...