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 --without-K --exact-split --safe #-}

module UF-UA-FunExt where

open import SpartanMLTT
open import UF-Base
open import UF-Equiv
open import UF-Univalence
open import UF-LeftCancellable
open import UF-FunExt
open import UF-FunExt-Properties
open import UF-Equiv-FunExt

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))  โ‰กโŸจ ap (ฮป ฯ€ x โ†’ ฯ€ (fโ‚€ x , fโ‚ x , h x)) ฯ€โ‚€-equals-ฯ€โ‚ โŸฉ
      (ฮป x โ†’ ฯ€โ‚ (fโ‚€ x , fโ‚ x , h x))  โ‰กโŸจ refl โŸฉ
      (ฮป x โ†’ fโ‚ x)                    โ‰กโŸจ refl โŸฉ
      fโ‚                              โˆŽ

\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
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-funext ua)
                                         (univalence-gives-propext 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}