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

module MGS.Equivalence-Induction where

open import MGS.Univalence public
open import MGS.Solved-Exercises public

equiv-singleton-lemma : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X)
                        (f : (y : X) β†’ x ＝ y β†’ A y)
                      β†’ ((y : X) β†’ is-equiv (f y))
                      β†’ is-singleton (Ξ£ A)

equiv-singleton-lemma {𝓀} {π“₯} {X} {A} x f i = Ξ³
 where
  e : (y : X) β†’ (x ＝ y) ≃ A y
  e y = (f y , i y)

  d : singleton-type' x ≃ Ξ£ A
  d = Ξ£-cong e

  abstract
   Ξ³ : is-singleton (Ξ£ A)
   Ξ³ = equiv-to-singleton (≃-sym d) (singleton-types'-are-singletons X x)

singleton-equiv-lemma : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X)
                        (f : (y : X) β†’ x ＝ y β†’ A y)
                      β†’ is-singleton (Ξ£ A)
                      β†’ (y : X) β†’ is-equiv (f y)

singleton-equiv-lemma {𝓀} {π“₯} {X} {A} x f i = Ξ³
 where
  g : singleton-type' x β†’ Ξ£ A
  g = NatΞ£ f

  e : is-equiv g
  e = maps-of-singletons-are-equivs g (singleton-types'-are-singletons X x) i

  abstract
   Ξ³ : (y : X) β†’ is-equiv (f y)
   Ξ³ = NatΞ£-equiv-gives-fiberwise-equiv f e

univalenceβ‡’ : is-univalent 𝓀
            β†’ (X : 𝓀 Μ‡ ) β†’ is-singleton (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y)

univalence⇒ ua X = equiv-singleton-lemma X (Id→Eq X) (ua X)

β‡’univalence : ((X : 𝓀 Μ‡ ) β†’ is-singleton (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y))
            β†’ is-univalent 𝓀

⇒univalence i X = singleton-equiv-lemma X (Id→Eq X) (i X)

univalenceβ†’ : is-univalent 𝓀
            β†’ (X : 𝓀 Μ‡ ) β†’ is-subsingleton (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y)

univalence→ ua X = singletons-are-subsingletons
                    (Ξ£ (X ≃_)) (univalenceβ‡’ ua X)

β†’univalence : ((X : 𝓀 Μ‡ ) β†’ is-subsingleton (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y))
            β†’ is-univalent 𝓀

β†’univalence i = β‡’univalence (Ξ» X β†’ pointed-subsingletons-are-singletons
                                    (Ξ£ (X ≃_)) (X , id-≃ X) (i X))

𝔾-≃ : is-univalent 𝓀
    β†’ (X : 𝓀 Μ‡ ) (A : (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y) β†’ π“₯ Μ‡ )
    β†’ A (X , id-≃ X) β†’ (Y : 𝓀 Μ‡ ) (e : X ≃ Y) β†’ A (Y , e)

𝔾-≃ {𝓀} ua X A a Y e = transport A p a
 where
  t : Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y
  t = (X , id-≃ X)

  p : t ＝ (Y , e)
  p = univalenceβ†’ {𝓀} ua X t (Y , e)

𝔾-≃-equation : (ua : is-univalent 𝓀)
             β†’ (X : 𝓀 Μ‡ ) (A : (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y) β†’ π“₯ Μ‡ ) (a : A (X , id-≃ X))
             β†’ 𝔾-≃ ua X A a X (id-≃ X) ＝ a

𝔾-≃-equation {𝓀} {π“₯} ua X A a =

  𝔾-≃ ua X A a X (id-≃ X) ＝⟨ refl _ ⟩
  transport A p a         ＝⟨ ap (Ξ» - β†’ transport A - a) q ⟩
  transport A (refl t) a  ＝⟨ refl _ ⟩
  a                       ∎

 where
  t : Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y
  t = (X , id-≃ X)

  p : t ＝ t
  p = univalenceβ†’ {𝓀} ua X t t

  q : p ＝ refl t
  q = subsingletons-are-sets (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y)
       (univalenceβ†’ {𝓀} ua X) t t p (refl t)

ℍ-≃ : is-univalent 𝓀
    β†’ (X : 𝓀 Μ‡ ) (A : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ )
    β†’ A X (id-≃ X) β†’ (Y : 𝓀 Μ‡ ) (e : X ≃ Y) β†’ A Y e

ℍ-≃ ua X A = 𝔾-≃ ua X (Ξ£-induction A)

ℍ-≃-equation : (ua : is-univalent 𝓀)
             β†’ (X : 𝓀 Μ‡ ) (A : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ ) (a : A X  (id-≃ X))
             β†’ ℍ-≃ ua X A a X (id-≃ X) ＝ a

ℍ-≃-equation ua X A = 𝔾-≃-equation ua X (Ξ£-induction A)

𝕁-≃ : is-univalent 𝓀
    β†’ (A : (X Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ )
    β†’ ((X : 𝓀 Μ‡ ) β†’ A X X (id-≃ X))
    β†’ (X Y : 𝓀 Μ‡ ) (e : X ≃ Y) β†’ A X Y e

𝕁-≃ ua A Ο† X = ℍ-≃ ua X (A X) (Ο† X)

𝕁-≃-equation : (ua : is-univalent 𝓀)
             β†’ (A : (X Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ )
             β†’ (Ο† : (X : 𝓀 Μ‡ ) β†’ A X X (id-≃ X))
             β†’ (X : 𝓀 Μ‡ ) β†’ 𝕁-≃ ua A Ο† X X (id-≃ X) ＝ Ο† X

𝕁-≃-equation ua A Ο† X = ℍ-≃-equation ua X (A X) (Ο† X)

ℍ-equiv : is-univalent 𝓀
        β†’ (X : 𝓀 Μ‡ ) (A : (Y : 𝓀 Μ‡ ) β†’ (X β†’ Y) β†’ π“₯ Μ‡ )
        β†’ A X (𝑖𝑑 X) β†’ (Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ is-equiv f β†’ A Y f

ℍ-equiv {𝓀} {π“₯} ua X A a Y f i = Ξ³ (f , i)
 where
  B : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡
  B Y (f , i) = A Y f

  b : B X (id-≃ X)
  b = a

  Ξ³ : (e : X ≃ Y) β†’ B Y e
  Ξ³ = ℍ-≃ ua X B b Y

𝕁-equiv : is-univalent 𝓀
        β†’ (A : (X Y : 𝓀 Μ‡ ) β†’ (X β†’ Y) β†’ π“₯ Μ‡ )
        β†’ ((X : 𝓀 Μ‡ ) β†’ A X X (𝑖𝑑 X))
        β†’ (X Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ is-equiv f β†’ A X Y f

𝕁-equiv ua A Ο† X = ℍ-equiv ua X (A X) (Ο† X)

𝕁-invertible : is-univalent 𝓀
             β†’ (A : (X Y : 𝓀 Μ‡ ) β†’ (X β†’ Y) β†’ π“₯ Μ‡ )
             β†’ ((X : 𝓀 Μ‡ ) β†’ A X X (𝑖𝑑 X))
             β†’ (X Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ invertible f β†’ A X Y f

𝕁-invertible ua A Ο† X Y f i = 𝕁-equiv ua A Ο† X Y f (invertibles-are-equivs f i)

automatic-equiv-functoriality :

      (F : 𝓀 Μ‡ β†’ 𝓀 Μ‡ )
      (𝓕 : {X Y : 𝓀 Μ‡ }  β†’ (X β†’ Y) β†’ F X β†’ F Y)
      (𝓕-id : {X : 𝓀 Μ‡ } β†’ 𝓕 (𝑖𝑑 X) ＝ 𝑖𝑑 (F X))
      {X Y Z : 𝓀 Μ‡ }
      (f : X β†’ Y)
      (g : Y β†’ Z)

    β†’ is-univalent 𝓀 β†’ is-equiv f + is-equiv g β†’ 𝓕 (g ∘ f) ＝ 𝓕 g ∘ 𝓕 f

automatic-equiv-functoriality {𝓀} F 𝓕 𝓕-id {X} {Y} {Z} f g ua = Ξ³
  where
   Ξ³ :  is-equiv f + is-equiv g β†’ 𝓕 (g ∘ f) ＝ 𝓕 g ∘ 𝓕 f
   Ξ³ (inl i) = ℍ-equiv ua X A a Y f i g
    where
     A : (Y : 𝓀 Μ‡ ) β†’ (X β†’ Y) β†’ 𝓀 Μ‡
     A Y f = (g : Y β†’ Z) β†’ 𝓕 (g ∘ f) ＝ 𝓕 g ∘ 𝓕 f

     a : (g : X β†’ Z) β†’ 𝓕 g ＝ 𝓕 g ∘ 𝓕 id
     a g = ap (𝓕 g ∘_) (𝓕-id ⁻¹)

   Ξ³ (inr j) = ℍ-equiv ua Y B b Z g j f
    where
     B : (Z : 𝓀 Μ‡ ) β†’ (Y β†’ Z) β†’ 𝓀 Μ‡
     B Z g = (f : X β†’ Y) β†’ 𝓕 (g ∘ f) ＝ 𝓕 g ∘ 𝓕 f

     b : (f : X β†’ Y) β†’ 𝓕 f ＝ 𝓕 (𝑖𝑑 Y) ∘ 𝓕 f
     b f = ap (_∘ 𝓕 f) (𝓕-id ⁻¹)

Ξ£-change-of-variable' : is-univalent 𝓀
                      β†’ {X : 𝓀 Μ‡ } {Y : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (f : X β†’ Y)
                      β†’ (i : is-equiv f)
                      β†’ (Ξ£ x κž‰ X , A x) ＝ (Ξ£ y κž‰ Y , A (inverse f i y))

Ξ£-change-of-variable' {𝓀} {π“₯} ua {X} {Y} A f i = ℍ-≃ ua X B b Y (f , i)
 where
   B : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’  (𝓀 βŠ” π“₯)⁺ Μ‡
   B Y (f , i) = Σ A ＝ (Σ (A ∘ inverse f i))

   b : B X (id-≃ X)
   b = refl (Ξ£ A)

Ξ£-change-of-variable'' : is-univalent 𝓀
                       β†’ {X : 𝓀 Μ‡ } {Y : 𝓀 Μ‡ } (A : Y β†’ π“₯ Μ‡ ) (f : X β†’ Y)
                       β†’ is-equiv f
                       β†’ (Ξ£ y κž‰ Y , A y) ＝ (Ξ£ x κž‰ X , A (f x))

Ξ£-change-of-variable'' ua A f i = Ξ£-change-of-variable' ua A
                                  (inverse f i)
                                  (inverses-are-equivs f i)

transport-map-along-＝ : {X Y Z : 𝓀 Μ‡ }
                        (p : X ＝ Y) (g : X β†’ Z)
                      β†’ transport (Ξ» - β†’ - β†’ Z) p g
                      ＝ g ∘ Idβ†’fun (p ⁻¹)

transport-map-along-＝ (refl X) = refl

transport-map-along-≃ : (ua : is-univalent 𝓀) {X Y Z : 𝓀 Μ‡ }
                        (e : X ≃ Y) (g : X β†’ Z)
                      → transport (λ - → - → Z) (Eq→Id ua X Y e) g
                      ＝ g ∘ ⌜ ≃-sym e ⌝

transport-map-along-≃ {𝓀} ua {X} {Y} {Z} = 𝕁-≃ ua A a X Y
 where
  A : (X Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ 𝓀 Μ‡
  A X Y e = (g : X → Z) → transport (λ - → - → Z) (Eq→Id ua X Y e) g
                        ＝ g ∘ ⌜ ≃-sym e ⌝
  a : (X : 𝓀 Μ‡ ) β†’ A X X (id-≃ X)
  a X g = transport (Ξ» - β†’ - β†’ Z) (Eqβ†’Id ua X X (id-≃ X)) g ＝⟨ q ⟩
          transport (Ξ» - β†’ - β†’ Z) (refl X) g                ＝⟨ refl _ ⟩
          g                                                 ∎
    where
     p : Eqβ†’Id ua X X (id-≃ X) ＝ refl X
     p = inverses-are-retractions (Id→Eq X X) (ua X X) (refl X)

     q = ap (Ξ» - β†’ transport (Ξ» - β†’ - β†’ Z) - g) p

\end{code}