Colimit Theory of colimits in Homotopy Type Theory : Work in progress coq_makefile -R . "" *.v -o Makefile COQC = hoqc COQDEP = hoqdep