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