Weak function extensionality
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-01-31.
Last modified on 2023-09-13.
module foundation.weak-function-extensionality where
Imports
open import foundation.action-on-identifications-functions open import foundation.decidable-equality open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.coproduct-types open import foundation-core.empty-types open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.identity-types open import foundation-core.propositions
Idea
Weak function extensionality is the principle that any dependent product of contractible types is contractible. This principle is equivalent to the function extensionality axiom.
Definition
Weak function extensionality
weak-function-extensionality : {l1 l2 : Level} (A : UU l1) (B : A → UU l2) → UU (l1 ⊔ l2) weak-function-extensionality A B = ((x : A) → is-contr (B x)) → is-contr ((x : A) → B x)
Weaker function extensionality
weaker-function-extensionality : {l1 l2 : Level} (A : UU l1) (B : A → UU l2) → UU (l1 ⊔ l2) weaker-function-extensionality A B = ((x : A) → is-prop (B x)) → is-prop ((x : A) → B x)
Properties
Weak function extensionality is logically equivalent to function extensionality
abstract weak-funext-funext : { l1 l2 : Level} → ( (A : UU l1) (B : A → UU l2) (f : (x : A) → B x) → function-extensionality f) → ( (A : UU l1) (B : A → UU l2) → weak-function-extensionality A B) pr1 (weak-funext-funext funext A B is-contr-B) x = center (is-contr-B x) pr2 (weak-funext-funext funext A B is-contr-B) f = map-inv-is-equiv ( funext A B (λ x → center (is-contr-B x)) f) ( λ x → contraction (is-contr-B x) (f x)) abstract funext-weak-funext : { l1 l2 : Level} → ( (A : UU l1) (B : A → UU l2) → weak-function-extensionality A B) → ( A : UU l1) (B : A → UU l2) (f : (x : A) → B x) → function-extensionality f funext-weak-funext weak-funext A B f = fundamental-theorem-id ( is-contr-retract-of ( (x : A) → Σ (B x) (λ b → f x = b)) ( ( λ t x → (pr1 t x , pr2 t x)) , ( λ t → (pr1 ∘ t , pr2 ∘ t)) , ( λ t → eq-pair-Σ refl refl)) ( weak-funext A ( λ x → Σ (B x) (λ b → f x = b)) ( λ x → is-contr-total-path (f x)))) ( λ g → htpy-eq {g = g})
A partial converse to weak function extensionality
module _ {l1 l2 : Level} {I : UU l1} {A : I → UU l2} (d : has-decidable-equality I) (H : is-contr ((i : I) → A i)) where cases-function-converse-weak-funext : (i : I) (x : A i) (j : I) (e : is-decidable (i = j)) → A j cases-function-converse-weak-funext i x .i (inl refl) = x cases-function-converse-weak-funext i x j (inr f) = center H j function-converse-weak-funext : (i : I) (x : A i) (j : I) → A j function-converse-weak-funext i x j = cases-function-converse-weak-funext i x j (d i j) cases-eq-function-converse-weak-funext : (i : I) (x : A i) (e : is-decidable (i = i)) → cases-function-converse-weak-funext i x i e = x cases-eq-function-converse-weak-funext i x (inl p) = ap ( λ t → cases-function-converse-weak-funext i x i (inl t)) ( eq-is-prop ( is-set-has-decidable-equality d i i) { p} { refl}) cases-eq-function-converse-weak-funext i x (inr f) = ex-falso (f refl) eq-function-converse-weak-funext : (i : I) (x : A i) → function-converse-weak-funext i x i = x eq-function-converse-weak-funext i x = cases-eq-function-converse-weak-funext i x (d i i) converse-weak-funext : (i : I) → is-contr (A i) pr1 (converse-weak-funext i) = center H i pr2 (converse-weak-funext i) y = ( htpy-eq ( contraction H (function-converse-weak-funext i y)) ( i)) ∙ ( eq-function-converse-weak-funext i y)
Weaker function extensionality implies weak function extensionality
weak-funext-weaker-funext : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → weaker-function-extensionality A B → weak-function-extensionality A B weak-funext-weaker-funext H C = is-proof-irrelevant-is-prop ( H (λ x → is-prop-is-contr (C x))) ( λ x → center (C x))
Recent changes
- 2023-09-13. Fredrik Bakke and Egbert Rijke. Refactor structured monoids (#761).
- 2023-08-01. Fredrik Bakke. Small constructions from large ones in order theory (#680).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-28. Fredrik Bakke. Enforce even indentation and automate some conventions (#635).