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.

About these ads
This entry was posted in Univalence. Bookmark the permalink.

6 Responses to Function Extensionality from Univalence

  1. Mike Shulman says:

    This is great. It looks like both proofs only go up to the point of “plain” functional extensionality. Andrej and Peter, have either of you formalized the additional fact that plain functional extensionality implies dependent functional extensionality?

  2. Mike Shulman says:

    Also, it looks like both proofs only show that if two functions are pointwise homotopic, then they are connected by a path. Vladimir had a stronger version of functional extensionality saying that the canonical map from the path space between two functions to the space of pointwise homotopies is an equivalence, and also a weaker version saying only that the dependent product of contractible spaces is contractible. I haven’t understood his proof that the weaker version implies the stronger yet; have you? It would be nice to have a good exposition of the relationship of all the different versions of “functional extensionality”, in addition to their derivations from univalence.

  3. Bas Spitters says:

    Does Hugo’s patch allow one to replace
    path_induction with subst and path_via with transitivity?

    http://github.com/herbelin/coq-hh/tree/8.3-homotopy

    Bas

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s