FunExt vs Weak FunExt

Nicolas Tabareau

Set Universe Polymorphism. From Coq Require Import ssreflect ssrfun ssrbool. From CASS.HoTT Require Import HoTT.

For every $A:\mathsf{Type}$, $B : A \rightarrow \mathsf{Type}$ and $f \ g : \forall x:A. B \ x$, we define pointwise equality as

Definition pw_eq A (B : A -> Type) (f g : forall x, B x) := forall x, f x = g x. Infix "f == g" := (pw_eq _ _ f g) (at level 50).

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

Definition weak_funext := forall A (B : A -> Type) (f g : forall x, B x), f == g -> f = g.

Recall that the axiom of (strong) function extensionality is stated as the fact that the canonical map

$$\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

$$\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

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

is a retraction of the space

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

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

Definition retract_of A B := {f : A -> B & {g : B -> A & forall x, g (f x) = x}}. Definition lemma1 A (B : A -> Type) (f : forall x, B x) : retract_of {g : forall x, B x & f == g} (forall x, {y : B x & f x = y}). Proof. Admitted.

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

$$\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

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

Definition lemma2 (wf: weak_funext) A (B : A -> Type) (f : forall x, B x) : IsContr (forall x, {y : B x & f x = y}). Proof. Admitted.

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

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

then

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

Definition lemma3 A (B : A -> Type) (f : forall x, B x) (wf : weak_funext) : wf A B f f (fun x => refl _) = refl _ -> forall g (h: f == g), apD10 (wf _ _ f g h) = h. Proof. Admitted.

Lemma 4

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

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

Definition lemma4 (wf : weak_funext) : {wf' : forall A B (f g: forall x:A, B x), f == g -> f = g & forall A B f, wf' A B f f (fun x => refl _) = refl _}. Proof. Admitted.

Conclude that

$$\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