HoTT Classes

This repository used to contain formalizations of algebra based on Math Classes but for HoTT. They have been merged in upstream HoTT (commit dd7c823).

Here remain results depending on inductive-inductive types, an experimental feature not yet merged in Coq, mostly about defining Cauchy real numbers.

Related Publications

See SCIENCE.md

Build

You can follow what travis does (.travis.yml, build-dependencies.sh and build-HoTTClasses.sh), or:

• Install dependencies:

  • Coq with inductive-inductive types including its depencies (some Ocaml libraries)
  • HoTT modified to compile with Coq IR

• In this guide they are installed respectively in directories coq/ and HoTT/.

• ./configure --hoqdir HoTT/ --coqbin coq/bin/

• make

Using IDEs

Coqide

The ./ide script only works if HoTT/ is in your $PATH, use /path/to/HoTT/hoqide -R theories HoTTClasses otherwise.

Proof General

Proof General understands the _CoqProject produced by ./configure. ./configure also sets up .dir-locals.el so that PG calls the right hoqtop program.