GitHub - roglo/mycoqhott: Experiments with HOTT. Trying to implement it in Coq.

roglo / mycoqhott Public

Notifications You must be signed in to change notification settings
Fork 0
Star 0

Experiments with HOTT. Trying to implement it in Coq.

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 2,006 Commits
.depend		.depend
.gitignore		.gitignore
Makefile		Makefile
README		README
adjunction.v		adjunction.v
areSet.v		areSet.v
category.v		category.v
chap1.v		chap1.v
chap2.v		chap2.v
chap3.v		chap3.v
chap4.v		chap4.v
chap5.v		chap5.v
cone_lim.v		cone_lim.v
funext.v		funext.v
funib.v		funib.v
h4c.v		h4c.v
misc_cat.v		misc_cat.v
prop_ext_irr.v		prop_ext_irr.v
yoneda.v		yoneda.v

Repository files navigation

The Coq Proof Assistant, version 8.14+alpha

Trying to implement the HoTT book in Coq (files chap1.v to chap4.v):
not terminated.

File h4c.v holds specific hott tools needed for categories, borrowed
from chap*.v above. Other useful file: areSet.v.

Work in progress:

Implementing categories in Coq.
  files: category.v misc_cat.v cone_lim.v adjunction.v yoneda.v.