202505300205

Univalence Implies Function Extensionality

Lemma

Weak Function Extensionality implies Function Extensionality.

We want to show that:

A : U \prod (P : A \to U) \prod (f, g) : \prod_{x : A} P (x) \prod is-equiv (happly (f, g))

Since a fiberwise map induces equivalence on total space if it is fiberwise an equivalence, by A Fiberwise Transformation is an Equivalence if its Total is an Equivalence, we get:

g : \prod_{x : A} P (x) \sum (f = g) \to g : \prod_{x : A} P (x) \sum f \sim g

which is induced by $γ (g : \prod_{(x : A)} P (x))$ . We get $happly (f, g)$ is an equivalence, since the type on the left is contractible by Some Contractible Types, it suffices to show that the type on right is contractibe, that is

g : \prod_{x : A} P (x) \sum x : A \prod f (x) = g (x)

But since Sigma Types respect Universal Properties, the above is equivalence to

x : A \prod u : P (x) \sum f (x) = u

The equivalence requires function extensionality, but we can prove the former is the retract of the latter without function extensionality.

The latter is a product of contractible types, so is a contractible type by weak function extensionality, thus we make the right hand side of the main equation a contractible, so we are done.

🏠 No Place Like ~

Explorer

Univalence Implies Function Extensionality

References

Graph View

Table of Contents

Backlinks