# 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