FunExt vs Weak FunExt

Nicolas Tabareau

For every $A:\mathsf{Type}$, $B : A \rightarrow \mathsf{Type}$ and $f \ g : \forall x:A.
B \ x$, 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

$\displaystyle \mathrm{apD_{10}}: \forall A (B : A \rightarrow \mathsf{Type}) (f \ g : \forall x:A,
                B \ x). f = g \rightarrow f == g.

is an equivalence

$\displaystyle \mathrm{funext}_{strong}:= \forall A (B : A \rightarrow \mathsf{T...
         ...rall x:A,
                B \ x). \mathop{\mathrm{IsEquiv}}(\mathrm{apD_{10}}\ A \ B \ f \ g).

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 $A:\mathsf{Type}$ $B : A \rightarrow \mathsf{Type}$ and $f : \forall x:A. B\
x$, the space

$\displaystyle \Sigma g : \forall x:A. B\ x \ \& \ f == g$

is a retraction of the space

$\displaystyle \forall x:A.\Sigma y : B \ x \ \& \ f \ x = y.$

Recall that a retraction between two types $A$ and $B$ is given by

As usual, $\Sigma x: A \ \& \ B$ denotes the dependent sum, with first and second projections noted $.1$ and $.2$.

Singleton are contractible

Show that singletons are contractible, that is for every type $A$ and $a:A$, we have

$\displaystyle \mathop{\mathrm{IsContr}}(\Sigma a' : A \ \& \ a = a')$

where $\mathop{\mathrm{IsContr}}X := \Sigma x:X \ \& \ \forall x': X. x = x'$.

Lemma 2

Show assuming $\mathrm{funext}_{weak}$ that for every type $A$, $B : A \rightarrow \mathsf{Type}$ and $f : \forall x:A. B\
x$, we have

$\displaystyle \mathop{\mathrm{IsContr}}(\forall x:A. \ \Sigma y : B \ x \ \& \ f \ x = y).$

Iscontr $\Rightarrow$ retract

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

Lemma 3

Show for every type $A$, $B : A \rightarrow \mathsf{Type}$ $f : \forall x:A. B\
x$ and assuming $w\! f : \mathrm{funext}_{weak}$, that if

$\displaystyle w\! f \ A \ B \ f \ f (\lambda x. \ \mathsf{refl}\,{(}f \ x)) = \mathsf{refl}\,{f}


$\displaystyle \forall (g : \forall x:A. B \ x) (h: f == g), \mathrm{apD_{10}}(w\! f \ A \ B \ f \
                g \ h) = h.

Lemma 4

Show that from any $w\! f : \mathrm{funext}_{weak}$, we can define $w\! f' : \mathrm{funext}_{weak}$ such that

$\displaystyle w\! f' \ A \ B \ f \ f (\lambda x. \ \mathsf{refl}\,{(}f \ x)) = \mathsf{refl}\,{f}.

Conclude that

$\displaystyle \mathrm{funext}_{weak}\rightarrow \mathrm{funext}_{strong}.

About this document ...

FunExt vs Weak FunExt

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