From Cory Knapp's PhD thesis (Chapter 2.4).

Transcribed to Agda by Martin Escardo and Cory 9th April and 24th May
2018.

Function extensionality follows from a generalization of
univalence. Using this, we formulate a condition equivalent to
the univalence of the universe U, namely

 (X Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ qinv f β†’ Ξ£ p κž‰ X ＝ Y , transport id p ＝ f

\begin{code}

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

module UF.Knapp-UA where

open import MLTT.Spartan
open import UF.Base
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.Univalence
open import UF.FunExt
open import UF.FunExt-Properties
open import UF.Yoneda

\end{code}

We first define when a map is a path-induced equivalence, and the type
of path-induced equivalences.

\begin{code}

isPIE : {X Y : 𝓀 Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 ⁺ Μ‡
isPIE {𝓀} {X} {Y} = fiber (idtofun X Y)

isPIE-remark : {X Y : 𝓀 Μ‡ } (f : X β†’ Y) β†’ isPIE f ＝ (Ξ£ p κž‰ X ＝ Y , idtofun X Y p ＝ f)
isPIE-remark f = refl

_⋍_ : 𝓀 Μ‡ β†’ 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
X ⋍ Y = Ξ£ f κž‰ (X β†’ Y) , isPIE f

idtopie : {X Y : 𝓀 Μ‡ } β†’ X ＝ Y β†’ X ⋍ Y
idtopie p = (idtofun _ _ p , p , refl)

pietofun : {X Y : 𝓀 Μ‡ } β†’ X ⋍ Y β†’ X β†’ Y
pietofun (f , (p , q)) = f

pietoid : {X Y : 𝓀 Μ‡ } β†’ X ⋍ Y β†’ X ＝ Y
pietoid (f , (p , q)) = p

pietofun-factors-through-idtofun : {X Y : 𝓀 Μ‡ } (e : X ⋍ Y) β†’ idtofun X Y (pietoid e) ＝ pietofun e
pietofun-factors-through-idtofun (f , (p , q)) = q

pietoid-idtopie : {X Y : 𝓀 Μ‡ } (p : X ＝ Y) β†’ pietoid (idtopie p) ＝ p
pietoid-idtopie refl = refl

idtopie-pietoid : {X Y : 𝓀 Μ‡ } (e : X ⋍ Y) β†’ idtopie (pietoid e) ＝ e
idtopie-pietoid (_ , refl , refl) = refl

PIE-induction : {X : 𝓀 Μ‡ } (A : {Y : 𝓀 Μ‡ } β†’ (X β†’ Y) β†’ π“₯ Μ‡ )
              β†’ A id β†’ {Y : 𝓀 Μ‡ } (f : X β†’ Y) β†’ isPIE f β†’ A f
PIE-induction {𝓀} {π“₯} {X} A g {Y} f (p , q) = transport A r (Ο† p)
  where
   Ο† : {Y : 𝓀 Μ‡ } (p : X ＝ Y) β†’ A (idtofun _ _ p)
   Ο† refl = g
   r : idtofun _ _ p ＝ f
   r = ap pr₁ (idtopie-pietoid (f , p , q))

isPIE-lc : {X Y : 𝓀 Μ‡ } (f : X β†’ Y) β†’ isPIE f β†’ left-cancellable f
isPIE-lc = PIE-induction left-cancellable (Ξ» {x} {x'} (p : id x ＝ id x') β†’ p)

\end{code}

The following maps are considered in the original proof that
univalence implies function extensionality by Voevodsky as presented
by Gambino, Kapulkin and Lumsdaine in
http://www.math.uwo.ca/faculty/kapulkin/notes/ua_implies_fe.pdf:

\begin{code}

Ξ” : 𝓀 Μ‡ β†’ 𝓀 Μ‡
Ξ” X = Ξ£ x κž‰ X , Ξ£ y κž‰ X , x ＝ y

Ξ΄ : {X : 𝓀 Μ‡ } β†’ X β†’ Ξ” X
Ξ΄ x = (x , x , refl)

π₁ : {X : 𝓀 Μ‡ } β†’ Ξ” X β†’ X
π₁ (x , _ , _) = x

Ο€β‚‚ : {X : 𝓀 Μ‡ } β†’ Ξ” X β†’ X
Ο€β‚‚ (_ , y , _) = y

πδ : (X : 𝓀 Μ‡ ) β†’ π₁ ∘ Ξ΄ ＝ Ο€β‚‚ ∘ Ξ΄
πδ {𝓀} X = refl {𝓀} {X β†’ X}

\end{code}

We now give Cory Knapp's criterion for (naive and hence proper)
function extensionality:

\begin{code}

knapps-funext-criterion :
              ({X Y : 𝓀 Μ‡ } {f : X β†’ Y} {g : X β†’ Y} β†’ isPIE f β†’ f ∼ g β†’ isPIE g)
            β†’ ({X : 𝓀 Μ‡ } β†’ isPIE (Ξ΄ {𝓀} {X}))
            β†’ βˆ€ {π“₯} β†’ naive-funext π“₯ 𝓀
knapps-funext-criterion {𝓀} H D {π“₯} {X} {Y} {f₁} {fβ‚‚} h = Ξ³
 where
  transport-isPIE : βˆ€ {𝓀 π“₯} {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {x y : X} (p : x ＝ y) β†’ isPIE (transport A p)
  transport-isPIE refl = refl , refl

  back-transport-isPIE : βˆ€ {𝓀 π“₯} {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {x y : X} (p : x ＝ y)
                       β†’ isPIE (transport⁻¹ A p)
  back-transport-isPIE p = transport-isPIE (p ⁻¹)

  back-transport-is-pre-comp'' : βˆ€ {𝓀} {X X' Y : 𝓀 Μ‡ } (e : X ⋍ X') (g : X' β†’ Y)
                               β†’ transport⁻¹ (Ξ» - β†’ - β†’ Y) (pietoid e) g ＝ g ∘ pr₁ e
  back-transport-is-pre-comp'' {𝓀} {X} {X'} e g = transport⁻¹-is-pre-comp (pietoid e) g βˆ™ q βˆ™ r
   where
    Ο† : βˆ€ {𝓀} (X Y : 𝓀 Μ‡ ) (p : X ＝ Y) β†’ Idtofun p ＝ pr₁ (idtopie p)
    Ο† X .X refl = refl
    q : g ∘ Idtofun (pietoid e) ＝ g ∘ pr₁ (idtopie (pietoid e))
    q = ap (Ξ» - β†’ g ∘ -) (Ο† X X' (pr₁ (prβ‚‚ e)))
    r : g ∘ pr₁ (idtopie (pietoid e)) ＝ g ∘ pr₁ e
    r = ap (Ξ» - β†’ g ∘ -) (ap pr₁ (idtopie-pietoid e))

  preComp-isPIE : {X X' Y : 𝓀 Μ‡ } (e : X ⋍ X') β†’ isPIE (Ξ» (g : X' β†’ Y) β†’ g ∘ (pr₁ e))
  preComp-isPIE {X} {X'} e = H (back-transport-isPIE (pietoid e)) (back-transport-is-pre-comp'' e)

  π₁-equals-Ο€β‚‚ : {X : 𝓀 Μ‡ } β†’ π₁ ＝ Ο€β‚‚
  π₁-equals-Ο€β‚‚ {X} = isPIE-lc (Ξ»(g : Ξ” X β†’ X) β†’ g ∘ Ξ΄) (preComp-isPIE (Ξ΄ , D)) (πδ X)

  Ξ³ : 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β‚‚                               ∎

knapps-funext-Criterion :
              ({X Y : 𝓀 Μ‡ } {f : X β†’ Y} {g : X β†’ Y} β†’ isPIE f β†’ f ∼ g β†’ isPIE g)
            β†’ ({X : 𝓀 Μ‡ } β†’ isPIE (Ξ΄ {𝓀} {X}))
            β†’ funext 𝓀 𝓀
knapps-funext-Criterion H D = naive-funext-gives-funext (knapps-funext-criterion H D)

\end{code}

Clearly, if univalence holds, then every equivalence is path induced:

\begin{code}

UA-is-equiv-isPIE : is-univalent 𝓀 β†’ {X Y : 𝓀 Μ‡ } (f : X β†’ Y) β†’ is-equiv f β†’ isPIE f
UA-is-equiv-isPIE ua f i = (eqtoid ua _ _ (f , i) , ap pr₁ (idtoeq-eqtoid ua _ _ (f , i)))

\end{code}

Next, we show that, conversely, if every equivalence is path induced,
then univalence holds.

\begin{code}

Ξ΄-is-equiv : {X : 𝓀 Μ‡ } β†’ is-equiv (Ξ΄ {𝓀} {X})
Ξ΄-is-equiv {𝓀} {X} = (π₁ , Ξ·) , (π₁ , Ξ΅)
 where
  Ξ· : (d : Ξ” X) β†’ Ξ΄ (π₁ d) ＝ d
  Ξ· (x , .x , refl) = refl
  Ξ΅ : (x : X) β†’ π₁ (Ξ΄ x) ＝ x
  Ξ΅ x = refl

isPIE-is-equiv : {X Y : 𝓀 Μ‡ } (f : X β†’ Y) β†’ isPIE f β†’ is-equiv f
isPIE-is-equiv = PIE-induction is-equiv (prβ‚‚ (≃-refl _))

is-equiv-isPIE-UA : ({X Y : 𝓀 Μ‡ } (f : X β†’ Y) β†’ is-equiv f β†’ isPIE f) β†’ is-univalent 𝓀
is-equiv-isPIE-UA {𝓀} Ο† X = Ξ³
 where
  H : {X Y : 𝓀 Μ‡ } {f : X β†’ Y} {g : X β†’ Y} β†’ isPIE f β†’ f ∼ g β†’ isPIE g
  H {X} {Y} {f} {g} isp h = Ο† g (equiv-closed-under-∼ f g (isPIE-is-equiv f isp) Ξ» x β†’ (h x)⁻¹)
  D : {X : 𝓀 Μ‡ } β†’ isPIE (Ξ΄ {𝓀} {X})
  D = Ο† Ξ΄ Ξ΄-is-equiv
  k : funext 𝓀 𝓀
  k = knapps-funext-Criterion {𝓀} H D
  s : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ X ＝ Y
  s Y (f , i) = pietoid (f , Ο† f i)
  Ξ· : {Y : 𝓀 Μ‡ } (e : X ≃ Y) β†’ idtoeq X Y (s Y e) ＝ e
  η {Y} (f , i) = to-Σ-＝ (p , being-equiv-is-prop'' k f _ _)
   where
    p : pr₁ (idtoeq X Y (s Y (f , i))) ＝ f
    p = pietofun-factors-through-idtofun (f , Ο† f i)
  Ξ³ : (Y : 𝓀 Μ‡ ) β†’ is-equiv (idtoeq X Y)
  Ξ³ = nats-with-sections-are-equivs X (idtoeq X) (Ξ» Y β†’ (s Y) , Ξ·)

\end{code}

We get the following characterization of univalence, where, as we can
see from the proof, we can replace qinv by is-equiv:

\begin{code}

UA-characterization :
                     ((X Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ qinv f β†’ fiber (transport id) f)
                   ↔ is-univalent 𝓀
UA-characterization {𝓀} = (forth , back)
 where
  forth : ((X Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ qinv f β†’ Ξ£ p κž‰ X ＝ Y , transport id p ＝ f) β†’ is-univalent 𝓀
  forth Ξ³ = is-equiv-isPIE-UA (Ξ» {X} {Y} β†’ Ο† X Y)
   where
    Ο† : (X Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ is-equiv f β†’ isPIE f
    Ο† X Y f i = p , r
     where
      p : X ＝ Y
      p = pr₁ (Ξ³ X Y f (equivs-are-qinvs f i))
      q : transport id p ＝ f
      q = prβ‚‚ (Ξ³ X Y f (equivs-are-qinvs f i))
      r : idtofun X Y p ＝ f
      r = idtofun-agreement X Y p βˆ™ q
  back : is-univalent 𝓀 β†’ ((X Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ qinv f β†’ Ξ£ p κž‰ X ＝ Y , transport id p ＝ f)
  back ua X Y f q = p , s
   where
    Οƒ : Ξ£ p κž‰ X ＝ Y , idtofun X Y p ＝ f
    Οƒ = UA-is-equiv-isPIE ua f (qinvs-are-equivs f q)
    p : X ＝ Y
    p = pr₁ Οƒ
    r : idtofun X Y p ＝ f
    r = prβ‚‚ Οƒ
    s : Idtofun p ＝ f
    s = (idtofun-agreement X Y p)⁻¹ βˆ™ r

\end{code}

TODO: Show that for any U, the type

  ({X Y : 𝓀 Μ‡ } (f : X β†’ Y) β†’ qinv f β†’  fiber (transport id) f))

is a proposition. Or give a counter-example or counter-model.

\end{code}