Introduction to univalence in Coq
Some exercises leading up to the formulation of the univalence axiom using the Coq proof assistant.
Files ending in *Solution.v contain proofs; other *.v files have the proofs removed.
Install Coq here.
If developing in emacs place the following lines:
(setq coq-load-path-include-current t) (setq coq-compile-before-require t)
in your init file. If not then you may have to run coqc on the various dependencies to run the proofs. For instance in CoqIde (which is automatically installed alongside Coq) you may need to do
Compile > Compile buffer
Intended order of files
- inductionAndFunctions.v introduces the Inductive and Definition keywords as well as the induction, destruct and apply tactics.
- lemmas.v introduces proofs as programmes and the simpl and rewrite tactics.
- propositionsSets.v introduces the basic ideas to analyse equivalences.
- equivalencesDefinitions.v introduces the various different types of equivalence.
- equivalences.v proves that the type of contractible maps is a proposition; introduces assert.
- univalence.v formulates the univalence axiom using contractible maps.
- productStrictlyAssoc.v uses the univalence axiom to prove that the product type construction is strictly associative in the appropriate sense.
- Coq - Proof Assistant
- The HoTT book - available here
- Using Yoneda rather than J to present the identity type - Martin Escardo
- A self-contained, brief and complete formulation of Voevodsky's univalence Axiom - Martin Escardo