Martin Escardo 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes

 https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/HoTT-UF-Agda.html
 https://github.com/martinescardo/HoTT-UF.Agda-Lecture-Notes

\begin{code}

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

module MGS.FunExt-from-Univalence where

open import MGS.Equivalence-Induction public

funext : βˆ€ 𝓀 π“₯ β†’ (𝓀 βŠ” π“₯)⁺ Μ‡
funext 𝓀 π“₯ = {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {f g : X β†’ Y} β†’ f ∼ g β†’ f ＝ g

precomp-is-equiv : is-univalent 𝓀
                 β†’ (X Y : 𝓀 Μ‡ ) (f : X β†’ Y)
                 β†’ is-equiv f
                 β†’ (Z : 𝓀 Μ‡ ) β†’ is-equiv (Ξ» (g : Y β†’ Z) β†’ g ∘ f)

precomp-is-equiv {𝓀} ua =
   𝕁-equiv ua
     (Ξ» X Y (f : X β†’ Y) β†’ (Z : 𝓀 Μ‡ ) β†’ is-equiv (Ξ» g β†’ g ∘ f))
     (Ξ» X Z β†’ id-is-equiv (X β†’ Z))

univalence-gives-funext : is-univalent 𝓀 β†’ funext π“₯ 𝓀
univalence-gives-funext {𝓀} {π“₯} ua {X} {Y} {fβ‚€} {f₁} = Ξ³
 where
  Ξ” : 𝓀 Μ‡
  Ξ” = Ξ£ yβ‚€ κž‰ Y , Ξ£ y₁ κž‰ Y , yβ‚€ ＝ y₁

  Ξ΄ : Y β†’ Ξ”
  Ξ΄ y = (y , y , refl y)

  Ο€β‚€ π₁ : Ξ” β†’ Y
  Ο€β‚€ (yβ‚€ , y₁ , p) = yβ‚€
  π₁ (yβ‚€ , y₁ , p) = y₁

  Ξ΄-is-equiv : is-equiv Ξ΄
  Ξ΄-is-equiv = invertibles-are-equivs Ξ΄ (Ο€β‚€ , Ξ· , Ξ΅)
   where
    Ξ· : (y : Y) β†’ Ο€β‚€ (Ξ΄ y) ＝ y
    Ξ· y = refl y

    Ξ΅ : (d : Ξ”) β†’ Ξ΄ (Ο€β‚€ d) ＝ d
    Ξ΅ (y , y , refl y) = refl (y , y , refl y)

  Ο† : (Ξ” β†’ Y) β†’ (Y β†’ Y)
  Ο† Ο€ = Ο€ ∘ Ξ΄

  Ο†-is-equiv : is-equiv Ο†
  Ο†-is-equiv = precomp-is-equiv ua Y Ξ” Ξ΄ Ξ΄-is-equiv Y

  p : Ο† Ο€β‚€ ＝ Ο† π₁
  p = refl (𝑖𝑑 Y)

  q : Ο€β‚€ ＝ π₁
  q = equivs-are-lc Ο† Ο†-is-equiv p

  Ξ³ : fβ‚€ ∼ f₁ β†’ fβ‚€ ＝ f₁
  Ξ³ h = ap (Ξ» Ο€ x β†’ Ο€ (fβ‚€ x , f₁ x , h x)) q

  Ξ³' : fβ‚€ ∼ f₁ β†’ fβ‚€ ＝ f₁
  Ξ³' h = fβ‚€                             ＝⟨ refl _ ⟩
         (Ξ» x β†’ fβ‚€ x)                   ＝⟨ refl _ ⟩
         (Ξ» x β†’ Ο€β‚€ (fβ‚€ x , f₁ x , h x)) ＝⟨ ap (Ξ» - x β†’ - (fβ‚€ x , f₁ x , h x)) q ⟩
         (Ξ» x β†’ π₁ (fβ‚€ x , f₁ x , h x)) ＝⟨ refl _ ⟩
         (Ξ» x β†’ f₁ x)                   ＝⟨ refl _ ⟩
         f₁                             ∎

dfunext : βˆ€ 𝓀 π“₯ β†’ (𝓀 βŠ” π“₯)⁺ Μ‡
dfunext 𝓀 π“₯ = {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {f g : Ξ  A} β†’ f ∼ g β†’ f ＝ g

happly : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (f g : Ξ  A) β†’ f ＝ g β†’ f ∼ g
happly f g p x = ap (Ξ» - β†’ - x) p

hfunext : βˆ€ 𝓀 π“₯ β†’ (𝓀 βŠ” π“₯)⁺ Μ‡
hfunext 𝓀 π“₯ = {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (f g : Ξ  A) β†’ is-equiv (happly f g)

hfunext-gives-dfunext : hfunext 𝓀 π“₯ β†’ dfunext 𝓀 π“₯
hfunext-gives-dfunext hfe {X} {A} {f} {g} = inverse (happly f g) (hfe f g)

vvfunext : βˆ€ 𝓀 π“₯ β†’ (𝓀 βŠ” π“₯)⁺ Μ‡
vvfunext 𝓀 π“₯ = {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
             β†’ ((x : X) β†’ is-singleton (A x))
             β†’ is-singleton (Ξ  A)

dfunext-gives-vvfunext : dfunext 𝓀 π“₯ β†’ vvfunext 𝓀 π“₯
dfunext-gives-vvfunext fe {X} {A} i = Ξ³
 where
  f : Ξ  A
  f x = center (A x) (i x)

  c : (g : Ξ  A) β†’ f ＝ g
  c g = fe (Ξ» (x : X) β†’ centrality (A x) (i x) (g x))

  Ξ³ : is-singleton (Ξ  A)
  Ξ³ = f , c

postcomp-invertible : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ }
                    β†’ funext 𝓦 𝓀
                    β†’ funext 𝓦 π“₯
                    β†’ (f : X β†’ Y)
                    β†’ invertible f
                    β†’ invertible (Ξ» (h : A β†’ X) β†’ f ∘ h)

postcomp-invertible {𝓀} {π“₯} {𝓦} {X} {Y} {A} nfe nfe' f (g , Ξ· , Ξ΅) = Ξ³
 where
  f' : (A β†’ X) β†’ (A β†’ Y)
  f' h = f ∘ h

  g' : (A β†’ Y) β†’ (A β†’ X)
  g' k = g ∘ k

  Ξ·' : (h : A β†’ X) β†’ g' (f' h) ＝ h
  η' h = nfe (η ∘ h)

  Ξ΅' : (k : A β†’ Y) β†’ f' (g' k) ＝ k
  Ρ' k = nfe' (Ρ ∘ k)

  Ξ³ : invertible f'
  Ξ³ = (g' , Ξ·' , Ξ΅')

postcomp-is-equiv : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ }
                  β†’ funext 𝓦 𝓀
                  β†’ funext 𝓦 π“₯
                  β†’ (f : X β†’ Y)
                  β†’ is-equiv f
                  β†’ is-equiv (Ξ» (h : A β†’ X) β†’ f ∘ h)

postcomp-is-equiv fe fe' f e =
 invertibles-are-equivs
  (Ξ» h β†’ f ∘ h)
  (postcomp-invertible fe fe' f (equivs-are-invertible f e))

vvfunext-gives-hfunext : vvfunext 𝓀 π“₯ β†’ hfunext 𝓀 π“₯
vvfunext-gives-hfunext vfe {X} {Y} f = Ξ³
 where
  a : (x : X) β†’ is-singleton (Ξ£ y κž‰ Y x , f x ＝ y)
  a x = singleton-types'-are-singletons (Y x) (f x)

  c : is-singleton (Ξ  x κž‰ X , Ξ£ y κž‰ Y x , f x ＝ y)
  c = vfe a

  ρ : (Ξ£ g κž‰ Ξ  Y , f ∼ g) ◁ (Ξ  x κž‰ X , Ξ£ y κž‰ Y x , f x ＝ y)
  ρ = ≃-gives-β–· Ξ Ξ£-distr-≃

  d : is-singleton (Ξ£ g κž‰ Ξ  Y , f ∼ g)
  d = retract-of-singleton ρ c

  e : (Ξ£ g κž‰ Ξ  Y , f ＝ g) β†’ (Ξ£ g κž‰ Ξ  Y , f ∼ g)
  e = NatΞ£ (happly f)

  i : is-equiv e
  i = maps-of-singletons-are-equivs e (singleton-types'-are-singletons (Ξ  Y) f) d

  Ξ³ : (g : Ξ  Y) β†’ is-equiv (happly f g)
  Ξ³ = NatΞ£-equiv-gives-fiberwise-equiv (happly f) i

funext-gives-vvfunext : funext 𝓀 (𝓀 βŠ” π“₯) β†’ funext 𝓀 𝓀 β†’ vvfunext 𝓀 π“₯
funext-gives-vvfunext {𝓀} {π“₯} fe fe' {X} {A} Ο† = Ξ³
 where
  f : Ξ£ A β†’ X
  f = pr₁

  f-is-equiv : is-equiv f
  f-is-equiv = pr₁-equiv Ο†

  g : (X β†’ Ξ£ A) β†’ (X β†’ X)
  g h = f ∘ h

  e : is-equiv g
  e = postcomp-is-equiv fe fe' f f-is-equiv

  i : is-singleton (Ξ£ h κž‰ (X β†’ Ξ£ A), f ∘ h ＝ 𝑖𝑑 X)
  i = e (𝑖𝑑 X)

  r : (Ξ£ h κž‰ (X β†’ Ξ£ A), f ∘ h ＝ 𝑖𝑑 X) β†’ Ξ  A
  r (h , p) x = transport A (happly (f ∘ h) (𝑖𝑑 X) p x) (prβ‚‚ (h x))

  s : Ξ  A β†’ (Ξ£ h κž‰ (X β†’ Ξ£ A), f ∘ h ＝ 𝑖𝑑 X)
  s Ο† = (Ξ» x β†’ x , Ο† x) , refl (𝑖𝑑 X)

  Ξ· : βˆ€ Ο† β†’ r (s Ο†) ＝ Ο†
  Ξ· Ο† = refl (r (s Ο†))

  Ξ³ : is-singleton (Ξ  A)
  Ξ³ = retract-of-singleton (r , s , Ξ·) i

abstract
 funext-gives-hfunext       : funext 𝓀 (𝓀 βŠ” π“₯) β†’ funext 𝓀 𝓀 β†’ hfunext 𝓀 π“₯
 dfunext-gives-hfunext      : dfunext 𝓀 π“₯ β†’ hfunext 𝓀 π“₯
 funext-gives-dfunext       : funext 𝓀 (𝓀 βŠ” π“₯) β†’ funext 𝓀 𝓀 β†’ dfunext 𝓀 π“₯
 univalence-gives-dfunext'  : is-univalent 𝓀 β†’ is-univalent (𝓀 βŠ” π“₯) β†’ dfunext 𝓀 π“₯
 univalence-gives-hfunext'  : is-univalent 𝓀 β†’ is-univalent (𝓀 βŠ” π“₯) β†’ hfunext 𝓀 π“₯
 univalence-gives-vvfunext' : is-univalent 𝓀 β†’ is-univalent (𝓀 βŠ” π“₯) β†’ vvfunext 𝓀 π“₯
 univalence-gives-hfunext   : is-univalent 𝓀 β†’ hfunext 𝓀 𝓀
 univalence-gives-dfunext   : is-univalent 𝓀 β†’ dfunext 𝓀 𝓀
 univalence-gives-vvfunext  : is-univalent 𝓀 β†’ vvfunext 𝓀 𝓀

 funext-gives-hfunext fe fe' = vvfunext-gives-hfunext (funext-gives-vvfunext fe fe')

 funext-gives-dfunext fe fe' = hfunext-gives-dfunext (funext-gives-hfunext fe fe')

 dfunext-gives-hfunext fe = vvfunext-gives-hfunext (dfunext-gives-vvfunext fe)

 univalence-gives-dfunext' ua ua' = funext-gives-dfunext
                                     (univalence-gives-funext ua')
                                     (univalence-gives-funext ua)

 univalence-gives-hfunext' ua ua' = funext-gives-hfunext
                                      (univalence-gives-funext ua')
                                      (univalence-gives-funext ua)

 univalence-gives-vvfunext' ua ua' = funext-gives-vvfunext
                                      (univalence-gives-funext ua')
                                      (univalence-gives-funext ua)

 univalence-gives-hfunext ua = univalence-gives-hfunext' ua ua

 univalence-gives-dfunext ua = univalence-gives-dfunext' ua ua

 univalence-gives-vvfunext ua = univalence-gives-vvfunext' ua ua

\end{code}