The univalence axiom implies function extensionality
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-02-16.
Last modified on 2024-02-06.
module foundation.univalence-implies-function-extensionality where
Imports
open import foundation.dependent-pair-types open import foundation.equivalence-induction open import foundation.function-extensionality open import foundation.postcomposition-functions open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import foundation.weak-function-extensionality open import foundation-core.contractible-maps open import foundation-core.contractible-types open import foundation-core.fibers-of-maps open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.transport-along-identifications
Idea
The univalence axiom implies function extensionality.
Theorem
abstract weak-funext-univalence : {l : Level} → weak-function-extensionality-Level l l weak-funext-univalence A B is-contr-B = is-contr-retract-of ( fiber (postcomp A pr1) id) ( ( λ f → ((λ x → (x , f x)) , refl)) , ( λ h x → tr B (htpy-eq (pr2 h) x) (pr2 (pr1 h x))) , ( refl-htpy)) ( is-contr-map-is-equiv ( is-equiv-postcomp-univalence A (equiv-pr1 is-contr-B)) ( id)) abstract funext-univalence : {l : Level} → function-extensionality-Level l l funext-univalence f = funext-weak-funext weak-funext-univalence f
Recent changes
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
- 2023-12-21. Fredrik Bakke. Action on homotopies of functions (#973).
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-10-22. Egbert Rijke and Fredrik Bakke. Refactor synthetic homotopy theory (#654).
- 2023-10-22. Fredrik Bakke. Refactor funext (#878).