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.Base
open import UF.Equiv
open import UF.Equiv-FunExt
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}

\begin{code}

univalence-gives-funext : is-univalent đ¤ â funext đ¤ đ¤
univalence-gives-funext ua = naive-funext-gives-funext
(naive-univalence-gives-funext ua)

\end{code}

\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
open import UF.Subsingletons-FunExt

ÎŠ-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}