Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

120 lines (75 sloc) 4.438 kB
1. Install a custom Coq from This is a fork
of the trunk and is compatible with standard Coq 8.4 trunk, except that
it supports special command-line options that turn on the homotopy theory
2. Get the HoTT library at
3. If you installed custom Coq so that it is found in the `PATH`, run
If you installed custom Coq in a secret place, tell ./configure
where to find it as follows:
./configure COQBIN=<absolute-directory-containing-coq-executables>
4. You can now use the HoTT library in place by running ./hoqtop and ./hoqc.
The library is loaded with `Require Import HoTT.Hopotopy`.
5. You can install the library globally with `make install`.
The HoTT library requires a custom version of Coq which supports the command-line options
`-relevant-equality` and `-warn-universe-inconsistencies`. The first one changes the
interpretation of equality to one that conforms to the homotopy-theoretic interpretation,
while the second one is an ugly temporary hack that turns universe inconsistencies intro
warning rather than errors.
At present only a fork of the Coq trunk supports these options, but we hope to get them
into the official Coq soon. Unfortunately for you that means you will have to compile a
version of Coq, available at
If you have never compiled Coq you may prefer to ask a friend for help. If you feel brave
you should try doing it yourself:
1. Obtain the custom Coq fork. If you have git clone the fork with
git clone
If you do not have git, you may still download the files as an archive file at (but it is better for you in the long run to
learn git).
2. Compile Coq, as explained in the INSTALL.txt file of Coq distribution. You will need
some prerequisites for compilation, such as OCaml 3.11.2 or later.
If you do not want the custom Coq to override one that you already have installed,
configure Coq with either `./configure -local` so that it will work in-place, or use
`./configure -prefix <dir>`, as explained by `./configure -help`.
Once you have installed the correct version of Coq, as explained in PREREQUISITES, you
proceed as follows. Clone the HoTT repository with
git clone
Even better, if you would like to contribute to HoTT, first fork the repository on
github and then use your own fork. This way you will be able to make pull requests.
If you do not want to deal with git at all, you may download an archive of HoTT at and unpack that. We do not recommend this
option because the HoTT library is under heavy development and you want to be able to
easily track changes.
Next you should configure the HoTT library:
1. If you installed the custom Coq as your default version of Coq, which means that it
it can be fond in PATH, run
in the HoTT directory.
2. If you installed the custom Coq somewhere special or configured it with `-local`,
you should tell ./configure where to find the custom Coq:
./configure COQBIN=<directory-containing-coq-executables>
where you should specify the *absolute* path name (starting with /) of the
directory which contains `coqtop`, `coqc`, etc.
To compile the HoTT library type
Because it is a bit tricky to run Coq with a custom standard library, we provided
scripts `hoqtop` and `hoqc` that do this for you, so you can run
directly from the HoTT directory to start using the library. Load it with
Require Import HoTT.Homotopy.
There is also `hoqc` for compiling files. You may prefer to install `hoqtop`, `hoqc` and
the library files globally, in which case you type
sudo make install
By default the files will be installed in `/usr/local/bin` and `/usr/local/share/hott`.
You can change the location by using standard `configure` parameters when you run it.
For example
./configure --bindir=$HOME/bin --datadir-$HOME/stuff
will install `hoqtop` and `hoqc` in the `bin` subdirectory of your home directory
and the HoTT library in `stuff/hott` subdirectory of your home directory.
Jump to Line
Something went wrong with that request. Please try again.