Univalence—Ⅱ
Contents
{-# 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 ≃-lemmasAn 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
Universe liftings
Here we prove a few facts concerning universe liftings.
Lifts of weak equivalences are weak equivalences.
Compositions or pre-compositions with lifts give rise to retractions. More precisely, we consider the following situations:
Suppose that we are given
φ : B → Cbetween types at levelsℓ'andℓ'', respectively. Consider also another levelν : Level. Then, for any typeA : 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
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 uanext, 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)