Sheafification

Sheafification functor in type theory.

Usage

These files compile with the HoTT library https://github.com/HoTT/HoTT, commit c0eb4f701824516a13b5c20bf2bbfa11e0c25278 (11 May) (Coq 8.5pl1).

One can use the library with

/path/to/coq_makefile -f _CoqProject -o Makefile

with adapted modification in _CoqProject, then simply compiling with make (this can take some time (30 minutes on a 2013 Macbook air, processor Intel Core I7 ; never finished on an older computer)).