This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

View the Project on GitHub UniMath/UniMath

Installing CoqIDE

If you wish also to build the program coqide, then issue the following command.

$ make BUILD_COQIDE=yes

Alternatively, you can specify the value of the BUILD_COQIDE option more permanently by following the instructions in the file build/Makefile-configuration-template.

Later on, after running the command make install as instructed below, in order to run the program coqide, you may use the following command.

$ sub/coq/bin/coqide <flags>

where <flags> are the options passed to coq as per the Emacs configuration file.