Switch branches/tags
Nothing to show
Find file History
Pull request Compare This branch is even with andrejbauer:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
..
Failed to load latest commit information.
doc
.gitignore
Equivalence.v
ExtraPrinciples.v
Homotopy.v
HomotopyDefinitions.v
Makefile
README.txt
coqdoc.sty
homotopy.css

README.txt

This folder contains a Coq implementation of Univalent Foundations.

It is based on Vladimir Voevodsky's initial implementation. So far we have
only reimplemented a small proportion of Vladimir's files.

Type "make" to compile the Coq files and generate documentation. You will have
to have installed:

1. Coq 8.3 (it might work with 8.2 and if there is enough interest, we can make sure
   that the files are compatible with 8.2).

2. For generation of the PDF files you need pdflatex. The latexmk utility is desirable
   but not required.