**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

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

Recall that a retraction between two types and is given by

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

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

Show assuming that for every type , and , we have

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

Show for every type , and assuming , that if

Show that from any , we can define such that

This document was generated using the LaTeX2HTML translator Version 2019 (Released January 1, 2019)

The command line arguments were:

`latex2html -split 0 -no_navigation funext.tex`

The translation was initiated on 2020-01-05