This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Weak function extensionality

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