Function Extensionality from Univalence | Homotopy Type Theory

Function Extensionality from Univalence

Andrej Bauer and Peter Lumsdaine have worked out a proof of Function Extensionality from Univalence that is somewhat different from Vladimir Voevodsky’s original.  In it, they identify and employ a very useful consequence of Univalence: induction along weak-equivalences.  Andrej has written it up using CoqDoc, which produces a very readable pdf available from his GitHub repository or directly here.  Peter has a neatly organized Coq treatment in his repository here.

Here is the Introduction from Andrej’s CoqDoc:

This is a self-contained presentation of the proof that the Univalence Axiom implies Functional Extensionality. It was developed by Peter LeFanu Lumsdaine and Andrej Bauer, following a suggestion by Steve Awodey. Peter has his own Coq file with essentially the same proof.

Our proof contains a number of ideas from Voevodsky’s proof. Perhaps the most important difference is our use of the induction principle for weak equivalences, see weq induction below. We outline the proof in human language at the end of the file, just before the proof of extensionality.

This file is an adaptation of a small part of Vladimir Voevodsky’s Coq files on homotopy theory and univalent foundations, see https://github.com/vladimirias/Foundations/.

The main difference with Voevodsky’s file is rather liberal use of standard Coq tricks, such as notation, implicit arguments and tactics. Also, we are lucky enough to avoid universe inconsistencies. Coq is touchy-feely about universes and one unfortunate definition seems to be enough to cause it to encounter a universe inconsistency. In fact, an early version of this file encountered a universe inconsistency in the last line of the main proof. By removing some auxiliary definitions, we managed to make it go away.

This file also contains extensive comments about Coq. This is meant to increase its instructional value.