CZF model in type theory
Go to file
Dan Frumin 8bac5d98fe add README 2019-01-21 18:48:29 +01:00
README.md add README 2019-01-21 18:48:29 +01:00
czf.v Subset relation and extensionality 2019-01-21 18:47:18 +01:00

README.md

Cumulative hierarchy in Coq

Aczel's model of CZF done in Coq.

Uses std++.