Internalizing intensional type theory
HTML TeX Coq Other
Switch branches/tags
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
html
tex
theories
.gitattributes
.gitignore
Makefile
README
_CoqProject

README

Internalization of the Setoid Interpretation of Type Theory - Coq development
========================================================================
Copyright 2013-2015 Matthieu Sozeau & Nicolas Tabareau <first.last@inria.fr>
Distributed under the terms of the LGPL.

To compile the development, simply run [coq_makefile -f _CoqProject -o
Makefile; make] in the toplevel directory, with coqc in your path. You
need at least Coq 8.5beta1 to compile this code, as it makes use of
universe polymorphism and fast projections.