Contents

  1. Equivalence of function extensionality axioms
    1. hfunext implies dfunext
    2. dfunext implies vfunext
    3. vfunext implies hfunext
{-# OPTIONS --without-K --safe #-}

module funext-equiv where

open import mltt
open import twocatconstructions
open import negation hiding (Id-to-Fun; Id-to-Fun') --redefined in univalence-base
open import basichomotopy
open import univalence-base


open ≡-Reasoning
open ◾-lemmas
open ap-lemmas
open transport-lemmas

Equivalence of function extensionality axioms

We prove the equivalence of all versions of function extensionality we introduced. There are three of them.

hfunext implies dfunext

The function happly f g : f ≡ g → f ~ g converts an identification of functions to a point-wise homotopy. The function extensionality axiom hfunext states that it is an equivalence. The version dfunext simply asserts the existence of a function in the opposite direction. Thus

hfunext→dfunext : ∀ {ℓ ℓ'} → hfunext ℓ ℓ' → dfunext ℓ ℓ'
hfunext→dfunext {ℓ} {ℓ'} hfe = λ f g  → π₁ (π₁ (hfe f g) )

by simply extracting the (right) inverse. Recall that π₁ (π₁ (hfe f g) ) is definitionally equal to π₁ (iseq→qinv (hfe f g) ).

top ⇑

dfunext implies vfunext

Now we prove the implication dfunext → vfunext, that assuming the existence of an inverse to happly implies extensionality in the sense of Voevodsky: the product of contractible types is contractible

dfunext→vfunext : ∀ {ℓ ℓ'} → dfunext ℓ ℓ' → vfunext ℓ ℓ'
dfunext→vfunext dfe {A} {P} is =  center , contraction
  where
    center : Π A P
    center = λ x → iscontr-center (P x) (is x)

    contraction : Π[ f ∈ (Π A P) ] (center ≡ f)
    contraction f =  dfe center f η
      where 
        η : center ~ f
        η x = iscontr-path-center (P x) (is x) (f x)

top ⇑

vfunext implies hfunext

Next, we want to prove that Voevodsky’s version implies the homotopy equivalence one.

vfunext→hfunext : ∀ {ℓ ℓ'} → vfunext ℓ ℓ' → hfunext ℓ ℓ'
vfunext→hfunext {ℓ} {ℓ'} vfe {A} {P} f g = qinv→iseq (happly f g) (weq→qinv (happly f g) is)
  where
First, we fix f, and consider happly as fiberwise map: happly f : (g : Π A P) → f ≡ g → f ~ g, of which we take the total space map: 
    φ : Hom (λ g → f ≡ g) (λ g → f ~ g)
    φ = happly f

    φφ : Σ[ g ∈ (Π A P) ] (f ≡ g) → Σ[ g ∈ (Π A P) ] (f ~ g)
    φφ = Hom→total φ
The domain is contractible, because it is the star of f: 
    γ : iscontr (Σ[ g ∈ (Π A P) ] (f ≡ g))
    γ = star-iscontr f
Therefore we are left to prove that the codomain is also contractible. To this end, we use the (semi)universal property for products and Σ-types to get that the domain of φφ is a retract of the codomain: 
    isretract : ( Σ[ g ∈ (Π A P) ] (Π[ x ∈ A ] (f x ≡ g x) )) ◅ ( Π[ x ∈ A ] ( Σ[ u ∈ P x ]  (f x ≡ u ) ) )
    isretract = ΣΠ-univ {A = A} {P} {Q = λ x u → (f x ≡ u)}
By Voevodsky’s function extensionality, which we have assumed in our statement, codomain φφ is contractible if each factor is contractible: 
    δ : iscontr ( Π[ x ∈ A ] ( Σ[ u ∈ P x ]  (f x ≡ u ) ) )
    δ = vfe (λ x → star-iscontr (f x))
And finally we can prove that domain φφ is contractible because it is a retract of a contractible type. 
    ε : iscontr (Σ[ g ∈ Π A P ] (f ~ g))
    ε = retract-of-contr-is-contr isretract δ
We now prove that φφ is a weak equivalence and we are done: 
    iseq-φφ : iseq φφ
    iseq-φφ = map-of-contractibles-is-we φφ γ ε

    isweq-φφ : isweq φφ
    isweq-φφ = qinv→weq (iseq→qinv φφ iseq-φφ)

    is : isweq (happly f g)
    is = π₁ (contr-fiber-total-iff-contr-fiber-Hom φ) isweq-φφ g

top ⇑