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


Weak function extensionality is the principle that any dependent product of contractible types is contractible. This principle is equivalent to the function extensionality axiom.


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)


Weak function extensionality is logically equivalent to function extensionality

  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 =
      ( funext A B  x  center (is-contr-B x)) f)
      ( λ x  contraction (is-contr-B x) (f x))

  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 =
      ( 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))

  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) =
      ( λ 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 =
    ( H  x  is-prop-is-contr (C x)))
    ( λ x  center (C x))

Recent changes