We construct the Rezk completion as a higher inductive type (as described in the HoTT book). The code makes use of the UniMath. The code is adapted from (https://github.com/UniMath/GrpdHITs).
- Make sure to have UniMath (https://github.com/UniMath/UniMath) installed
- coq_makefile -f _CoqProject -o Makefile
- make