mirror of https://github.com/nmvdw/HITs-Examples
470 B
470 B
Formalization of Kuratowski-finite sets in homotopy type theory
The Coq docs can be found here
Building instructions
Prerequisites: the HoTT library.
- Generate the Makefile:
coq_makefile -f _CoqProject -o Makefile - Compile the library using make:
make -j 2 - The HTML coqdoc can be obtained via
make html
An overview of some of the main results can be found in the file CPP.v