Sheafification functor in type theory.
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)).