Martin Escardo, 9th April 2018 We first give Voevodsky's original proof that univalence implies non-dependent, naive function extensionality, as presented by Gambino, Kapulkin and Lumsdaine in http://www.math.uwo.ca/faculty/kapulkin/notes/ua_implies_fe.pdf. We then deduce dependent function extensionality applying a second argument by Voevodsky, developed in another module, which doesn't depend on univalence. \begin{code} {-# OPTIONS --safe --without-K #-} module UF.UA-FunExt where open import MLTT.Spartan open import UF.Equiv open import UF.FunExt open import UF.FunExt-Properties open import UF.LeftCancellable open import UF.SubtypeClassifier open import UF.Univalence naive-univalence-gives-funext : is-univalent đ¤ â â {đĽ} â naive-funext đĽ đ¤ naive-univalence-gives-funext {đ¤} ua {đĽ} {X} {Y} {fâ} {fâ} h = Îł where Î = ÎŁ yâ ę Y , ÎŁ yâ ę Y , yâ ďź yâ δ : Y â Πδ y = (y , y , refl) Ďâ Ďâ : Î â Y Ďâ (yâ , yâ , p) = yâ Ďâ (yâ , yâ , p) = yâ δ-is-equiv : is-equiv δ δ-is-equiv = (Ďâ , Ρ) , (Ďâ , Îľ) where Ρ : (d : Î) â δ (Ďâ d) ďź d Ρ (yâ , yâ , refl) = refl Îľ : (y : Y) â Ďâ (δ y) ďź y Îľ y = refl Ďδ : Ďâ â δ ďź Ďâ â δ Ďδ = refl Ď : (Î â Y) â (Y â Y) Ď Ď = Ď â δ Ď-is-equiv : is-equiv Ď Ď-is-equiv = pre-comp-is-equiv ua δ δ-is-equiv Ďâ-equals-Ďâ : Ďâ ďź Ďâ Ďâ-equals-Ďâ = is-equiv-lc Ď Ď-is-equiv Ďδ Îł : fâ ďź fâ Îł = fâ ďźâ¨ refl ⊠(Îť x â fâ x) ďźâ¨ refl ⊠(Îť x â Ďâ (fâ x , fâ x , h x)) ďźâ¨ I ⊠(Îť x â Ďâ (fâ x , fâ x , h x)) ďźâ¨ refl ⊠(Îť x â fâ x) ďźâ¨ refl ⊠fâ â where I = ap (Îť Ď x â Ď (fâ x , fâ x , h x)) Ďâ-equals-Ďâ \end{code} Added 19th May 2018: \begin{code} univalence-gives-funext : is-univalent đ¤ â funext đ¤ đ¤ univalence-gives-funext ua = naive-funext-gives-funext (naive-univalence-gives-funext ua) \end{code} Added 27 Jun 2018: \begin{code} univalence-gives-funext' : â đ¤ đĽ â is-univalent đ¤ â is-univalent (đ¤ â đĽ) â funext đ¤ đĽ univalence-gives-funext' đ¤ đĽ ua ua' = naive-funext-gives-funext' (naive-univalence-gives-funext ua') (naive-univalence-gives-funext ua) Univalence-gives-FunExt : Univalence â FunExt Univalence-gives-FunExt ua đ¤ đĽ = univalence-gives-funext' đ¤ đĽ (ua đ¤) (ua (đ¤ â đĽ)) Univalence-gives-Fun-Ext : Univalence â Fun-Ext Univalence-gives-Fun-Ext ua {đ¤} {đĽ} = Univalence-gives-FunExt ua đ¤ đĽ funext-from-successive-univalence : â đ¤ â is-univalent đ¤ â is-univalent (đ¤ âş) â funext đ¤ (đ¤ âş) funext-from-successive-univalence đ¤ = univalence-gives-funext' đ¤ (đ¤ âş) open import UF.Subsingletons Ί-ext-from-univalence : is-univalent đ¤ â {p q : Ί đ¤} â (p holds â q holds) â (q holds â p holds) â p ďź q Ί-ext-from-univalence {đ¤} ua {p} {q} = Ί-extensionality (univalence-gives-propext ua) (univalence-gives-funext ua) \end{code} April 2020. How much function extensionality do we get from propositional univalence? \begin{code} naive-prop-valued-funext : (đ¤ đĽ : Universe) â (đ¤ â đĽ)âş Ě naive-prop-valued-funext đ¤ đĽ = (X : đ¤ Ě ) (Y : đĽ Ě ) â is-prop Y â is-prop (X â Y) propositional-univalence : (đ¤ : Universe) â đ¤ âş Ě propositional-univalence đ¤ = (P : đ¤ Ě ) â is-prop P â (Y : đ¤ Ě ) â is-equiv (idtoeq P Y) prop-eqtoid : propositional-univalence đ¤ â (P : đ¤ Ě ) â is-prop P â (Y : đ¤ Ě ) â P â Y â P ďź Y prop-eqtoid pu P i Y = inverse (idtoeq P Y) (pu P i Y) propositional-â-induction : (đ¤ đĽ : Universe) â (đ¤ â đĽ)âş Ě propositional-â-induction đ¤ đĽ = (P : đ¤ Ě ) â is-prop P â (A : (Y : đ¤ Ě ) â P â Y â đĽ Ě ) â A P (â-refl P) â (Y : đ¤ Ě ) (e : P â Y) â A Y e propositional-JEq : propositional-univalence đ¤ â (đĽ : Universe) â propositional-â-induction đ¤ đĽ propositional-JEq {đ¤} pu đĽ P i A b Y e = Îł where A' : (Y : đ¤ Ě ) â P ďź Y â đĽ Ě A' Y q = A Y (idtoeq P Y q) b' : A' P refl b' = b f' : (Y : đ¤ Ě ) (q : P ďź Y) â A' Y q f' = Jbased P A' b' g : A Y (idtoeq P Y (prop-eqtoid pu P i Y e)) g = f' Y (prop-eqtoid pu P i Y e) Îł : A Y (id e) Îł = transport (A Y) (inverses-are-sections (idtoeq P Y) (pu P i Y) e) g prop-precomp-is-equiv : propositional-univalence đ¤ â (X Y Z : đ¤ Ě ) â is-prop X â (f : X â Y) â is-equiv f â is-equiv (Îť (g : Y â Z) â g â f) prop-precomp-is-equiv {đ¤} pu X Y Z i f ise = propositional-JEq pu đ¤ X i (Îť W e â is-equiv (Îť g â g â â e â)) (id-is-equiv (X â Z)) Y (f , ise) prop-precomp-is-equiv' : propositional-univalence đ¤ â (X Y Z : đ¤ Ě ) â is-prop Y â (f : X â Y) â is-equiv f â is-equiv (Îť (g : Y â Z) â g â f) prop-precomp-is-equiv' {đ¤} pu X Y Z i f ise = prop-precomp-is-equiv pu X Y Z j f ise where j : is-prop X j = equiv-to-prop (f , ise) i propositional-univalence-gives-naive-prop-valued-funext : propositional-univalence đ¤ â naive-prop-valued-funext đĽ đ¤ propositional-univalence-gives-naive-prop-valued-funext {đ¤} {đĽ} pu X Y Y-is-prop fâ fâ = Îł where Î : đ¤ Ě Î = ÎŁ yâ ę Y , ÎŁ yâ ę Y , yâ ďź yâ δ : Y â Πδ y = (y , y , refl) Ďâ Ďâ : Î â Y Ďâ (yâ , yâ , p) = yâ Ďâ (yâ , yâ , p) = yâ δ-is-equiv : is-equiv δ δ-is-equiv = (Ďâ , Ρ) , (Ďâ , Îľ) where Ρ : (d : Î) â δ (Ďâ d) ďź d Ρ (yâ , yâ , refl) = refl Îľ : (y : Y) â Ďâ (δ y) ďź y Îľ y = refl Ďδ : Ďâ â δ ďź Ďâ â δ Ďδ = refl Ď : (Î â Y) â (Y â Y) Ď Ď = Ď â δ Ď-is-equiv : is-equiv Ď Ď-is-equiv = prop-precomp-is-equiv pu Y Î Y Y-is-prop δ δ-is-equiv Ďâ-equals-Ďâ : Ďâ ďź Ďâ Ďâ-equals-Ďâ = equivs-are-lc Ď Ď-is-equiv Ďδ Îł : fâ ďź fâ Îł = fâ ďźâ¨ refl ⊠(Îť x â fâ x) ďźâ¨ refl ⊠(Îť x â Ďâ (fâ x , fâ x , h x)) ďźâ¨ ap (Îť Ď x â Ď (fâ x , fâ x , h x)) Ďâ-equals-Ďâ ⊠(Îť x â Ďâ (fâ x , fâ x , h x)) ďźâ¨ refl ⊠(Îť x â fâ x) ďźâ¨ refl ⊠fâ â where h : (x : X) â fâ x ďź fâ x h x = Y-is-prop (fâ x) (fâ x) \end{code}