Colimit

Theory of colimits in Homotopy Type Theory : Work in progress

coq_makefile -R . "" *.v -o Makefile COQC = hoqc COQDEP = hoqdep

Name		Name	Last commit message	Last commit date
Latest commit History 41 Commits
.gitignore		.gitignore
MyTacs.v		MyTacs.v
README.md		README.md
VD_truncation.v		VD_truncation.v
cech_nerve.v		cech_nerve.v
colim_coeq.v		colim_coeq.v
colimit.v		colimit.v
colimit2.v		colimit2.v
colimit_CN_base_case.v		colimit_CN_base_case.v
colimit_examples.v		colimit_examples.v
colimit_kernel_pair.v		colimit_kernel_pair.v
descent.v		descent.v
equivalence.v		equivalence.v
gpd.v		gpd.v
lemmas.v		lemmas.v
nat_lemmas.v		nat_lemmas.v
with_compo.v		with_compo.v
with_compo_sim.v		with_compo_sim.v

Provide feedback