FunExt vs Weak FunExt

Nicolas Tabareau

For every , and , we define pointwise equality as

The axiom of weak extensionality is stated as the existence of a function

Recall that the axiom of (strong) function extensionality is stated as the fact that the canonical map is an equivalence It is clear that strong function extensionality implies weak function extensionality, but the converse is not obvious and even looks wrong.

In this exercise, we show that weak function extensionality implies strong funextionality.

Lemma 1

Show that for every  and , the space is a retraction of the space Recall that a retraction between two types and is given by

As usual, denotes the dependent sum, with first and second projections noted and .

Singleton are contractible

Show that singletons are contractible, that is for every type and , we have where .

Lemma 2

Show assuming that for every type , and , we have Iscontr retract

Show that if a type is contractible and is a retract of , then is contractible.

Lemma 3

Show for every type ,  and assuming , that if then Lemma 4

Show that from any , we can define such that Conclude that 