Formalisation of strict ω-categories and the homotopy hypothesis in type theory, using coinduction
To compile the coq files, you need the trunk branch of Coq (avalaible at https://github.com/coq, commit c2d053c6).
Simply type 'make' in the repository, coq_makefile will do the rest.