Contents

  1. Preparatory lemmas
  2. Universe liftings
  3. Univalence implies function extensionality
    1. Postcomposition with weak equivalences
    2. Univalence implies function extensionality

{-# OPTIONS --without-K --safe #-}

module univalence-funext where 

open import mltt
open import twocatconstructions
open import basichomotopy
open import univalence-base
open import funext-equiv

open ≡-Reasoning
open ◾-lemmas

We prove that the univalence axiom implies function extensionality. We already know that all versions of function extensionality are equivalent, so we specifically prove that the univalence axiom, assumed at level ℓ ⊔ ℓ', implies the Voevodsky’s function extensionality at levels and ℓ'.

Before plunging into the proof we need a few preparatory statements about total spaces of fibrations that may be of independent interest.

Preparatory lemmas

First we prove that given a fibration, corresponding to the dependent type P : A → 𝓤, the homotopy fiber hfib π₁ a, where π₁ is the projection to the base, is weakly equivalent to the “fiber” at a, namely P a:

hfib-of-proj-equiv-fiber :  { ℓ'} {A : Set } {P : A  Set ℓ'}
                   (a : A)  (hfib (π₁ {E = P}) a)  P a
hfib-of-proj-equiv-fiber {A = A} {P} a = f , qinv→iseq f qif
  where
    f : hfib (π₁ {E = P}) a  P a
    f (u , p) = transport P p (π₂ u)

    qif : qinv f
    Σ.fst qif = λ s  (a , s) , refl
    Σ.fst (Σ.snd qif) = λ s  refl
    Σ.snd (Σ.snd qif) ((x , s) , refl) = refl --here destroy the path in ((x , s) , p)

We also have that if the family is fiberwise contractible then the projection from the total space is a weak equivalence:

fiberwise-contr-π₁-isweq :  { ℓ'} {A : Set } {P : A  Set ℓ'}  
                           ((x : A)  iscontr (P x))  isweq (π₁ {E = P})
fiberwise-contr-π₁-isweq {} {ℓ'} {A} {P} φ u = we-and-contr-implies-contr ((hfib-of-proj-equiv-fiber u) ≃⁻¹) (φ u)
  where
    open ≃-lemmas
An application, which is of independent interest, is that for any function f : A → B the domain is equivalent of the Σ-type consisting of the homotopy fibers:
domain-is-Σ :  { ℓ'} {A : Set } {B : Set ℓ'} (f : A  B) 
              A  Σ B  b  hfib f b)
domain-is-Σ {} {ℓ'} {A} {B} f = ( e ≃◾≃ l ) ≃⁻¹
  where
    open ≃-lemmas
    
    e : Σ[ b  B ] hfib f b  Σ[ a  A ] Σ[ b  B ] (f a  b)
    Σ.fst e (b , a , γ) = a , b , γ
    Σ.fst (Σ.snd e) =  { (a , b , γ)  b , a , γ}) , λ _  refl
    Σ.snd (Σ.snd e) =  { (a , b , γ)  b , a , γ}) , λ _  refl

    p : Σ[ a  A ] Σ[ b  B ] (f a  b)  A
    p = π₁ {E = λ a  Σ[ b  B ] (f a  b)}

    ll : isweq p
    ll = fiberwise-contr-π₁-isweq  a  star-iscontr (f a))

    l : Σ[ a  A ] Σ[ b  B ] (f a  b)  A
    l = p , qinv→iseq p (weq→qinv p ll)

There is also a very interesting characterization of the type Π A P, namely if we call α the operation of post-composing with the projection π₁, then Π A P is a retract of the homotopy fiber of α at the identity map of A.

α :  { ℓ'} {A : Set } {P : A  Set ℓ'}  (A  Σ A P)  (A  A)
α f = π₁ ∘′ f

product-is-retract-hfib-id :  { ℓ'} {A : Set } {P : A  Set ℓ'}  (Π A P)  hfib (α {} {ℓ'} {A} {P}) (id {A = A})
product-is-retract-hfib-id {} {ℓ'} {A} {P} = ρ , (σ , ρσ)
  where
    ρ : hfib (α {} {ℓ'} {A} {P}) id  Π A P
    ρ (f , p) = λ x  transport P (ap (ev' x) p) (π₂ (f x))

    σ : Π A P  hfib (α {} {ℓ'} {A} {P}) id
    σ f =  x  x , f x) , refl

    ρσ :  x  ρ (σ x)) ~  x  x)
    ρσ f = refl

top ⇑


Universe liftings

Here we prove a few facts concerning universe liftings.

  1. Lifts of weak equivalences are weak equivalences.

  2. Compositions or pre-compositions with lifts give rise to retractions. More precisely, we consider the following situations:

    Suppose that we are given φ : B → C between types at levels ℓ' and ℓ'', respectively. Consider also another level ν : Level. Then, for any type A : Set ℓ, the diagram

    \[ \begin{array}{ccccc} (A → B) & \xrightarrow{=} & (A → B) & \xrightarrow{=} & (A → B) \\ \downarrow & & \downarrow & & \downarrow \\ (A → C) & → & (A → \hat C) & → & (A → C) \end{array} \]

    is a retraction, where Ĉ = Lift ν C.

module yoga-lift where

  unlift :  {} {A : Set } {ν : Level}  Lift ν A  A
  unlift (lift lower₁) = lower₁

  unlift-path :  {} {A : Set } {x y : A} {ν : Level} (p : lift { = ν} x  lift y)  x  y
  unlift-path p = ap unlift p

  unlift-path' :  {} {A : Set } {x y : A} {ν : Level} (p : lift { = ν} x  lift y)  x  y
  unlift-path' refl = refl

  →lift :  { ℓ'} {A : Set } {B : Set ℓ'} (f : A  B) (ν : Level)  (A  Lift ν B)
  →lift f ν = λ a  lift (f a)

  →unlift :  { ℓ'} {A : Set } {B : Set ℓ'} {ν : Level} (f : A  Lift ν B)   (A  B)
  →unlift {B = B} {ν} f  = (unlift {A = B} {ν}) ∘′ f

  →unlift→lift-is-id :  { ℓ'} {A : Set } {B : Set ℓ'} {ν : Level} 
                       {f : A  B}  →unlift (→lift f ν)  f
  →unlift→lift-is-id = refl

  function-type-is-retract :  { ℓ'} {A : Set } {B : Set ℓ'} {ν : Level} 
                             (A  B)  (A  Lift ν B)
  function-type-is-retract {A = A} {B} {ν} = r , (s , γ)
    where
      r : (A  Lift ν B)  (A  B)
      r = →unlift

      s : (A  B)  (A  Lift ν B)
      s = λ f  →lift {A = A} {B = B} f ν

      γ : r ∘′ s ~ id
      γ = λ f  →unlift→lift-is-id {A = A} {B} {ν} {f}



  lift→ :  { ℓ'} {A : Set } {B : Set ℓ'} (ν : Level) (f : A  B)  (Lift ν A)  B
  lift→ ν f = λ{ (lift lower₁)  f lower₁ }

  unlift→ :  { ℓ'} {A : Set } {ν : Level} {B : Set ℓ'} (f : Lift ν A  B)  A  B
  unlift→ {A = A} f a = f (lift a)

  lift→unlift→-is-id :  { ℓ'} {A : Set } {B : Set ℓ'} {ν : Level} 
                       {f : A  B}  unlift→ (lift→ ν f)  f
  lift→unlift→-is-id = refl

  function-type-is-retract₁ :  { ℓ'} {A : Set } {B : Set ℓ'} {ν : Level} 
                              (A  B)  (Lift ν A  B)
  function-type-is-retract₁ {A = A} {B} {ν} = r , s , γ
    where
      r : (Lift ν A  B)  (A  B)
      r = unlift→ 

      s : (A  B)  (Lift ν A  B)
      s = λ f  lift→ ν f

      γ : r ∘′ s ~ id
      γ = λ f  refl

  ≃lift :  { ℓ'} {A : Set } {B : Set ℓ'} 
          (f : A  B) (is : isweq f) {ν : Level}  isweq (→lift f ν)
  ≃lift f is {ν} = qinv→weq qis-lift
    where
      qis : qinv f
      qis = weq→qinv f is

      qis-lift : qinv (→lift f ν)
      Σ.fst qis-lift = lift→ ν (π₁ qis)
      Σ.fst (Σ.snd qis-lift) = λ { (lift lower₁)  ap lift (π₁ (π₂ qis) lower₁)}
      Σ.snd (Σ.snd qis-lift) = λ x  π₂ (π₂ qis) x

  ≃unlift : ∀{  ℓ'} {A : Set } {B : Set ℓ'} {ν : Level} 
            (f : A  Lift ν B) (is : isweq f)  isweq (→unlift f)
  ≃unlift {ν = ν} f is = qinv→weq qis-unlift
    where
      qis : qinv f
      qis = weq→qinv f is

      qis-unlift : qinv (→unlift f)
      Σ.fst qis-unlift = unlift→ (π₁ qis)
      Σ.fst (Σ.snd qis-unlift) = λ x  ap unlift (π₁ (π₂ qis) (lift x))
      Σ.snd (Σ.snd qis-unlift) = λ x  π₂ (π₂ qis) x

  lift≃ :  { ℓ'} {A : Set } {B : Set ℓ'} 
          (f : A  B) (is : isweq f) {ν : Level}  isweq (lift→ ν f)
  lift≃ f is {ν} = qinv→weq lift-qis
    where
      qis : qinv f
      qis = weq→qinv f is

      lift-qis : qinv (lift→ ν f)
      Σ.fst lift-qis = →lift (π₁ qis) ν
      Σ.fst (Σ.snd lift-qis) = λ x  π₁ (π₂ qis) x
      Σ.snd (Σ.snd lift-qis) = λ { (lift lower₁)  ap lift (π₂ (π₂ qis) lower₁)}

  unlift≃ : ∀{  ℓ'} {A : Set } {B : Set ℓ'} {ν : Level} 
            (f : Lift ν A  B) (is : isweq f)  isweq (unlift→ f)
  unlift≃ {ν = ν} f is = qinv→weq unlift-qis
    where
      qis : qinv f
      qis = weq→qinv f is

      unlift-qis : qinv (unlift→ f)
      Σ.fst unlift-qis = →unlift (π₁ qis)
      Σ.fst (Σ.snd unlift-qis) = λ x  π₁ (π₂ qis) x
      Σ.snd (Σ.snd unlift-qis) = λ x  ap unlift (π₂ (π₂ qis) (lift x))

  -- Lifting the identity as a weak equivalence
  -- Every type is equivelent to its own lift
  ≃id-lift :  { ℓ'} (A : Set )  A  Lift ℓ' A
  Σ.fst (≃id-lift {} {ℓ'} A) = →lift id ℓ'
  Σ.fst (Σ.snd (≃id-lift {} {ℓ'} A)) = (lift→ ℓ' id) ,  x  refl)
  Σ.snd (Σ.snd (≃id-lift {} {ℓ'} A)) = (lift→ ℓ' id) ,  x  refl)

  -- Combinations for convenience
  →lift→ :  { ℓ'} {A : Set } {B : Set ℓ'} (f : A  B) {ν : Level}  
           (Lift ν A  Lift ν B)
  →lift→ f {ν} = →lift (lift→ ν f) ν

  →unlift→ :  { ℓ'} {A : Set } {B : Set ℓ'} {ν : Level}  
             (f : Lift ν A  Lift ν B)  (A  B)
  →unlift→ f = →unlift (unlift→ f)

  ≃lift≃ :  { ℓ'} {A : Set } {B : Set ℓ'} 
           (f : A  B) (is : isweq f) {ν : Level}  isweq (→lift→ f {ν})
  ≃lift≃ f is {ν} = ≃lift (lift→ ν f) (lift≃ f is {ν}) {ν}

  ≃unlift≃ :  { ℓ'} {A : Set } {B : Set ℓ'} {ν : Level} 
             (f : Lift ν A  Lift ν B) (is : isweq f)  isweq (→unlift→ f)
  ≃unlift≃ f is = ≃unlift (unlift→ f) (unlift≃ f is)



  module LiftedFunctionType↓ { ℓ' ℓ'' : Level}
                             (ν : Level)
                             (A : Set )
                             (B : Set ℓ')
                             (C : Set ℓ'')
                             (φ : B  C) where

    $_ : (A  B)  (A  C)
    $ f = φ ∘′ f

    <$_ : (A  Lift ν B)  (A  C)
    <$ f = (lift→ ν φ) ∘′ f

    is-id-L : (f : A  B)  <$ (→lift f ν)  $ f
    is-id-L f = refl

    is-id-K : (f : A  Lift ν B)  $ (→unlift f)  <$ f
    is-id-K f = refl

    thm : $_ ◅→ <$_
    _◅→_.φ thm = function-type-is-retract
    _◅→_.ψ thm = ◅-id (A  C)
    _◅→_.L thm = is-id-L
    _◅→_.K thm = is-id-K
    _◅→_.H thm = λ f  refl


  module LiftedFunctionType↑ { ℓ' ℓ'' : Level}
                             (ν : Level)
                             (A : Set )
                             (B : Set ℓ')
                             (C : Set ℓ'')
                             (φ : B  C) where

    $_ : (A  B)  (A  C)
    $ f = φ ∘′ f

    $>_ : (A  B)  (A  Lift ν C)
    $> f = (→lift φ ν) ∘′ f

    is-id-L : (f : A  B)  $> f  →lift ($ f) ν  
    is-id-L f = refl

    is-id-K : (f : A  B)  $ f  →unlift ($> f)
    is-id-K f = refl

    thm : $_ ◅→ $>_
    _◅→_.φ thm = ◅-id (A  B)
    _◅→_.ψ thm = function-type-is-retract
    _◅→_.L thm = is-id-L
    _◅→_.K thm = is-id-K
    _◅→_.H thm = λ f  refl

top ⇑


Univalence implies function extensionality

The to prove that univalence implies function extensionality, we specifically assume univalence at level ℓ ⊔ ℓ' and deduce that function extensionality in Voevodsky’s sense holds. Thanks to the equivalence between all formulations of function extensionality we can then obtain the other forms of the principle by using the material in Function Extensionality.

Postcomposition with weak equivalences

Let us assume the universe 𝓤 = Set ℓ is univalent:

module PostCompositionWithEq { : Level}
                             (ua : is-univalent ) where

       open U-Rules ua

We first prove that if e : A → B is a weak equivalence, then post-composition with it induces a weak equivalence (X → A) → (X → B): this is easily seen to be a consequence of function extensionality, but the important point is that it actually follows from univalence:

       post-composition-with-eq-is-eq :  {ν} {X : Set ν} {A B : Set } ((e , ise) : A  B) 
                                        (X  A)  (X  B)
       Σ.fst (post-composition-with-eq-is-eq {ν} {X} (e , ise)) = λ f  e ∘′ f
       Σ.snd (post-composition-with-eq-is-eq {ν} {X} (e , ise)) = homot-to-we-is-we φ is⟨p⟩
         where
           A B : Set 
           A = domain e
           B = codomain e
           
           -- post-composition with…
           _∘ : (A  B)  (X  A)  (X  B)
           e  = λ f  e ∘′ f

Now we use univalence to obtain p : A ≡ B from e : A → B:

           p : A  B
           p = Eq→Id A B (e , ise)

Transporting along p gives a new function (X → A) → (X → B) which is an equivalence, because so is transport from one fiber to another:

           -- define the family of functions from X
           Q : Set   Set (ν  )
           Q = λ Z  (X  Z)

           ⟨_⟩ : (A  B)  (X  A)  (X  B)
            p  = transport Q p

           is⟨p⟩ : iseq  p 
           is⟨p⟩ = transport-is-≃ Q p

Finally we prove that post-composition with e : A → B is homotopic to the transport along p : A ≡ B. Since the latter, i.e. ⟨ p ⟩ is a weak equivalence, so must be the former, which is used above in the main statement.

           φ : e  ~  p 
           φ f = (γ2 f)  (γ1 f p)
             where

               open ~-lemmas
               γ1 : (f : X  A) (p : A  B)   ((Id→Fun p ) f)  ( p   f)
               γ1 f refl = refl

               γ2 : (f : X  A)  ((e ) f)  ((Id→Fun p) ) f
               γ2 f = ap  g  (g ) f) δ
                 where
                   δ : e  transport  x  x) (Σ.fst (Σ.fst (ua A B)) (e , ise))
                   δ = (ap π₁ (Eq→Id-is-rinv (e , ise)) ⁻¹)

Univalence implies function extensionality

Finally, we are ready to prove that the Univalence Axiom implies Function Extensionality. We assume univalence at level ℓ ⊔ ℓ', or in other words that 𝓤 = Set (ℓ ⊔ ℓ') is univalent, and we deduce function extensionality in Voevodsky’s sense.

univalence→vfunext :  { ℓ'} {A : Set } {P : A  Set ℓ'} (ua : is-univalent (  ℓ'))  vfunext  ℓ' 
univalence→vfunext {} {ℓ'} ua {A} {P} γ = retract-of-contr-is-contr Π-type-is-retract (isw-α̂  (→lift id ℓ'))
  where
    open yoga-lift
    
    p₁ : Σ A P  A
    p₁ = π₁ {E = P}
First we open the above module, where we proved that postcomposition with a weak equivalence gives a weak equivalence, passing the correct term to assume univalence univalence at level ℓ ⊔ ℓ'
    open PostCompositionWithEq ua
next, we open the submodule where we proved the retraction property of the lifts, again passing the types and functions we need:
    open LiftedFunctionType↑ ℓ' A (Σ A P) A p₁
The rest proceeds by simply defining the required terms and proving they are weak equivalences:
    p̑₁ : (Σ A P)  Lift ℓ' A
    p̑₁ = →lift p₁ ℓ'

    is : isweq p₁
    is = fiberwise-contr-π₁-isweq {A = A} {P} γ 

    is^ : isweq p̑₁
    is^ = ≃lift p₁ is 

    α̑ : (A  Σ A P)  (A  Lift ℓ' A)
    α̑ = post-composition-with-eq-is-eq is^≃ 
      where
        is^≃ : Σ A P  Lift ℓ' A
        is^≃ = p̑₁ , qinv→iseq p̑₁ (weq→qinv _ is^)

    isw-α̂ : isweq (π₁ α̑)
    isw-α̂ = qinv→weq ( iseq→qinv (π₁ α̑) (π₂ α̑) )
At this point we check that the newly defined maps agree—definitionally—with those defined in the module LiftedFunctionType.
    --sanity checks
    --------------------------------
    same-map : α  $_
    same-map = refl

    same-underlying-map : π₁ α̑  $>_
    same-underlying-map = refl
    --------------------------------
The above check puts us in position to use the retraction theorem and we are done:
    hfib-is-retract : hfib $_ (id {A = A})  hfib $>_ (→lift id ℓ')
    hfib-is-retract = hfibs-of-retracts-are-retracts thm id

    Π-type-is-retract : Π A P  hfib $>_ (→lift id ℓ')
    Π-type-is-retract =  Π A P                   ◅⟨ product-is-retract-hfib-id {} {ℓ'} {A} {P} 
                         (hfib $_ (id {A = A}))  ◅⟨ hfib-is-retract 
                         hfib $>_ (→lift id ℓ')  ◅∎
       where
         open ◅-Reasoning

We finish by writing the statements that allow us to obtain the other forms of function extensionality from the univalence axiom:

univalence→hfunext :  { ℓ'} (ua : is-univalent (  ℓ'))  hfunext  ℓ'
univalence→hfunext {} {ℓ'} ua {A} {P} = vfunext→hfunext {} {ℓ'} vfe {A} {P}
  where
    vfe : vfunext  ℓ'
    vfe {A} {P} = univalence→vfunext {} {ℓ'} {A} {P} ua

univalence→dfunext :  { ℓ'} (ua : is-univalent (  ℓ'))  dfunext  ℓ'
univalence→dfunext {} {ℓ'} ua = hfunext→dfunext {} {ℓ'} (univalence→hfunext ua)

top ⇑