# Weak function extensionality

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-01-31.

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.function-extensionality
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-types
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.torsorial-type-families


## 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

instance-weak-function-extensionality :
{l1 l2 : Level} (A : UU l1) (B : A → UU l2) → UU (l1 ⊔ l2)
instance-weak-function-extensionality A B =
((x : A) → is-contr (B x)) → is-contr ((x : A) → B x)

weak-function-extensionality-Level : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
weak-function-extensionality-Level l1 l2 =
(A : UU l1) (B : A → UU l2) → instance-weak-function-extensionality A B

weak-function-extensionality : UUω
weak-function-extensionality =
{l1 l2 : Level} → weak-function-extensionality-Level l1 l2


### Weaker function extensionality

instance-weaker-function-extensionality :
{l1 l2 : Level} (A : UU l1) (B : A → UU l2) → UU (l1 ⊔ l2)
instance-weaker-function-extensionality A B =
((x : A) → is-prop (B x)) → is-prop ((x : A) → B x)

weaker-function-extensionality-Level : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
weaker-function-extensionality-Level l1 l2 =
(A : UU l1) (B : A → UU l2) → instance-weaker-function-extensionality A B

weaker-function-extensionality : UUω
weaker-function-extensionality =
{l1 l2 : Level} → weaker-function-extensionality-Level l1 l2


## Properties

### Weak function extensionality is logically equivalent to function extensionality

abstract
weak-funext-funext :
{l1 l2 : Level} →
function-extensionality-Level l1 l2 →
weak-function-extensionality-Level l1 l2
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 (λ x → center (is-contr-B x)) f)
( λ x → contraction (is-contr-B x) (f x))

abstract
funext-weak-funext :
{l1 l2 : Level} →
weak-function-extensionality-Level l1 l2 →
function-extensionality-Level l1 l2
funext-weak-funext weak-funext {A = 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-eq-fiber refl))
( weak-funext A
( λ x → Σ (B x) (λ b → f x ＝ b))
( λ x → is-torsorial-Id (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} →
instance-weaker-function-extensionality A B →
instance-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))