Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Development of the univalent foundations of mathematics in Coq
Coq
tree: bc0ec24f07

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
Main Library
Proof of Extensionality
.#a
Makefile
README
diagrams_and_comments.pdf
u0.v
u01.v
u012.v
u0a.v
u0b.v
u1.v
u12.v
u2.v
uuu.v

README

This directory contains two sub-directories ./Main Library and ./Proof of Extensionality . 

The first one contains the file univ.v with the current  state of the math library for Coq  based on Univalent Foundations and several auxiliary files. In particular it contains the documentation, in the HTML format,  for univ.v which was generated by Coqdoc . The table of content for univ.html is in univ_toc.html and this is a good starting point for exploration.  Additional info about the univalent foundations can be found on my web page ( http://www.math.ias.edu/~vladimir/Site3/home.html ). 

The second sub-directory contains several Coq files which together provide the code for the proof of the fact that univalence axiom implies functional extensionality as well as the related documentation in HTML. Unlike the proofs of the main library univ.v this proof uses several levels of universes which makes it a little awkward in the present version of Coq. The common table of context is in toc.html .

Something went wrong with that request. Please try again.