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
tree: 74965674ca

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
Main_Library
Proof_of_Extensionality
README

README

This is the current version (as of May 17, 2011) of the mathematical library for the proof assistant Coq based on the univalent semantics for the calculus of inductive constructions. The most important new thing in this release is the construction of true set-quotients of types. This opens the way for multiple further developments from the definition of the type of real numbers, to true quotients in universal algebra to the definition of homotopy groups of types. 

There are two sub-directories  ./Main Library and ./Proof of Extensionality . The best way to see in detail what the files in these subdirectories are about is to look at the tables of content (files toc.html ) produced by coqdoc. 

The first one contains subdirectories Generalities/ hlevel1/ and hlevel2/ . The first of those contains two identical files uu0.v and uu1.v and file uu1uu0.v . The need for two files is explained by the fact that we need to work with two universe levels later and since Coq does not support universe polymorphism at the moment we had to repeat the general constructions twice.  In these files we prove main results which apply to all types and which require only one universe level to be proved. They are more or less the same as the files u0.v etc. of the previous release except that the part related to finite sets has been moved to a separate file in hlevel2/. The file uu1uu0 contains the definitions of functions connecting the definitions from uu0 and uu1. 

Some of the results in uu0 and uu1 use the extensionality axiom for functions (introduced in the same file). No other axioms or resizings (see below) are used and these files should compile with the standard version of Coq. 

Directory hlevel1/ contains results and constructions related to types of h-level 1 i.e. to types which correspond to "propositions" in our formalization which require two universe levels. The content of individual files is explained in the headers of the files. Starting from this point we use the following convention. If the filename contains _up it means that its results depend on the univalence axiom for hProp. If the filename contains _r it means that its results depend on "resizing axioms". Since resizing axioms are not implemented in the current versions of Coq it means, in practice, that in order to compile these files one has to use a patch for Coq which removes the universe consistency checking. Note that we continue to keep track of universe levels in these files "by hand" and use only those "universe re-assigments" or "resizings" which are semantically justified.  

Directory hlevel2/ contains results related to types of hlevel 2 i.e. to types corresponding to sets in our formalization which require two universe levels. The content of individual files is explained in the headers of the files. This directory contains in particular the construction of set-quotients of types. 

The second directory contains file univ01.v with the formulation of the general univalence axiom and the proof of functional extensionality based on this axiom. Due to the proof that functional extensionality for "straight" functions implies functional extensionality for dependent functions given in u*.v the proof now does not require three universe levels. There is also a proof that the univalence axiom follows from two simplier statements.



Something went wrong with that request. Please try again.