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.

This entry was posted in Univalence. Bookmark the permalink.

6 Responses to Function Extensionality from Univalence

Mike Shulman says:

18 March 2011 at 11:51

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?

- Nils Anders Danielsson says:
  
  6 April 2011 at 13:29
  
  I have used Agda to formalise this:
  
  http://www.cse.chalmers.se/~nad/listings/equality/Univalence-axiom.html
  
  Overview of the code:
  
  http://www.cse.chalmers.se/~nad/listings/equality/README.html
  
  Darcs repository:
  
  http://www.cse.chalmers.se/~nad/repos/equality/
  
- Mike Shulman says:
  
  8 April 2011 at 00:17
  
  Very nice, thanks for the links! For those who don’t want to read the code, the idea seems to be this. Dependent FE follows from Vladimir’s “weak” FE axiom that dependent products preserve contractibility, by considering the type $\prod_{x\colon A} \sum_{y\colon B(x)} (y \rightsquigarrow g x)$ — weak FE makes it contractible, while two sections f and g of B that are pointwise homotopic give two points of it, which are therefore related by a path. So it suffices to prove weak FE.
  
  Now suppose $\prod_{x\colon A} \mathrm{Contractible}(B(x))$ . Then each B(x) is equivalent to a point, hence (by univalence) we have $\prod_{x\colon A} (B(x) \rightsquigarrow \mathrm{unit})$ . Therefore, by non-dependent FE applied to $B\colon A \to \mathrm{Type}$ and $\mathrm{const} \mathrm{unit} \colon A \to \mathrm{Type}$ w, have $B \rightsquigarrow \mathrm{const} \mathrm{unit}$ . But $\prod_{x\colon A} \mathrm{unit}$ is certainly contractible, hence so also is $\prod_{x\colon A} B(x)$ .
  
  I wonder, is it necessary to use univalence again in that proof? Does dependent FE follow from non-dependent FE without univalence?
  
Mike Shulman says:

22 March 2011 at 01:06

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.

Bas Spitters says:

31 March 2011 at 10:12

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

- Mike Shulman says:
  
  31 March 2011 at 14:38
  
  I can’t figure out from the description of Hugo’s patch what it is supposed to do. What is meant by “level”?