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 #-}

module MGS-Equivalences where

open import MGS-Retracts public

invertible : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
invertible f = Ξ£ g κž‰ (codomain f β†’ domain f) , (g ∘ f ∼ id) Γ— (f ∘ g ∼ id)

fiber : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) β†’ Y β†’ 𝓀 βŠ” π“₯ Μ‡
fiber f y = Ξ£ x κž‰ domain f , f x ≑ y

fiber-point : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {f : X β†’ Y} {y : Y}
            β†’ fiber f y β†’ X

fiber-point (x , p) = x

fiber-identification : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {f : X β†’ Y} {y : Y}
                     β†’ (w : fiber f y) β†’ f (fiber-point w) ≑ y

fiber-identification (x , p) = p

is-equiv : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
is-equiv f = (y : codomain f) β†’ is-singleton (fiber f y)

inverse : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) β†’ is-equiv f β†’ (Y β†’ X)
inverse f e y = fiber-point (center (fiber f y) (e y))

inverses-are-sections : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) (e : is-equiv f)
                      β†’ f ∘ inverse f e ∼ id

inverses-are-sections f e y = fiber-identification (center (fiber f y) (e y))

inverse-centrality : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                     (f : X β†’ Y) (e : is-equiv f) (y : Y) (t : fiber f y)
                   β†’ (inverse f e y , inverses-are-sections f e y) ≑ t

inverse-centrality f e y = centrality (fiber f y) (e y)

inverses-are-retractions : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) (e : is-equiv f)
                         β†’ inverse f e ∘ f ∼ id

inverses-are-retractions f e x = ap fiber-point p
 where
  p : inverse f e (f x) , inverses-are-sections f e (f x) ≑ x , refl (f x)
  p = inverse-centrality f e (f x) (x , (refl (f x)))

equivs-are-invertible : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                      β†’ is-equiv f β†’ invertible f

equivs-are-invertible f e = inverse f e ,
                            inverses-are-retractions f e ,
                            inverses-are-sections f e

invertibles-are-equivs : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                       β†’ invertible f β†’ is-equiv f

invertibles-are-equivs {𝓀} {π“₯} {X} {Y} f (g , Ξ· , Ξ΅) yβ‚€ = iii
 where
  i : (y : Y) β†’ (f (g y) ≑ yβ‚€) ◁ (y ≑ yβ‚€)
  i y =  r , s , transport-is-section (_≑ yβ‚€) (Ξ΅ y)
   where
    s : f (g y) ≑ yβ‚€ β†’ y ≑ yβ‚€
    s = transport (_≑ yβ‚€) (Ξ΅ y)

    r : y ≑ yβ‚€ β†’ f (g y) ≑ yβ‚€
    r = transport (_≑ yβ‚€) ((Ξ΅ y)⁻¹)

  ii : fiber f yβ‚€ ◁ singleton-type yβ‚€
  ii = (Ξ£ x κž‰ X , f x ≑ yβ‚€)     β—βŸ¨ Ξ£-reindexing-retract g (f , Ξ·) ⟩
       (Ξ£ y κž‰ Y , f (g y) ≑ yβ‚€) β—βŸ¨ Ξ£-retract i ⟩
       (Ξ£ y κž‰ Y , y ≑ yβ‚€)       β—€

  iii : is-singleton (fiber f yβ‚€)
  iii = retract-of-singleton ii (singleton-types-are-singletons Y yβ‚€)

inverses-are-equivs : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) (e : is-equiv f)
                    β†’ is-equiv (inverse f e)

inverses-are-equivs f e = invertibles-are-equivs
                           (inverse f e)
                           (f , inverses-are-sections f e , inverses-are-retractions f e)

inversion-involutive : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) (e : is-equiv f)
                     β†’ inverse (inverse f e) (inverses-are-equivs f e) ≑ f

inversion-involutive f e = refl f

id-invertible : (X : 𝓀 Μ‡ ) β†’ invertible (𝑖𝑑 X)
id-invertible X = 𝑖𝑑 X , refl , refl

∘-invertible : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } {f : X β†’ Y} {f' : Y β†’ Z}
             β†’ invertible f' β†’ invertible f β†’ invertible (f' ∘ f)

∘-invertible {𝓀} {π“₯} {𝓦} {X} {Y} {Z} {f} {f'} (g' , gf' , fg') (g , gf , fg) =
  g ∘ g' , η , Ρ
 where
  Ξ· = Ξ» x β†’ g (g' (f' (f x))) β‰‘βŸ¨ ap g (gf' (f x)) ⟩
            g (f x)           β‰‘βŸ¨ gf x ⟩
            x                 ∎

  Ξ΅ = Ξ» z β†’ f' (f (g (g' z))) β‰‘βŸ¨ ap f' (fg (g' z)) ⟩
            f' (g' z)         β‰‘βŸ¨ fg' z ⟩
            z                 ∎

id-is-equiv : (X : 𝓀 Μ‡ ) β†’ is-equiv (𝑖𝑑 X)
id-is-equiv = singleton-types-are-singletons

∘-is-equiv : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } {f : X β†’ Y} {g : Y β†’ Z}
           β†’ is-equiv g β†’ is-equiv f β†’ is-equiv (g ∘ f)

∘-is-equiv {𝓀} {π“₯} {𝓦} {X} {Y} {Z} {f} {g} i j = Ξ³
 where
  abstract
   γ : is-equiv (g ∘ f)
   γ = invertibles-are-equivs (g ∘ f)
         (∘-invertible (equivs-are-invertible g i)
         (equivs-are-invertible f j))

inverse-of-∘ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
               (f : X β†’ Y) (g : Y β†’ Z)
               (i : is-equiv f) (j : is-equiv g)
             β†’ inverse f i ∘ inverse g j ∼ inverse (g ∘ f) (∘-is-equiv j i)

inverse-of-∘ f g i j z =

  f' (g' z)             β‰‘βŸ¨ (ap (f' ∘ g') (s z))⁻¹ ⟩
  f' (g' (g (f (h z)))) β‰‘βŸ¨ ap f' (inverses-are-retractions g j (f (h z))) ⟩
  f' (f (h z))          β‰‘βŸ¨ inverses-are-retractions f i (h z) ⟩
  h z                   ∎

 where
  f' = inverse f i
  g' = inverse g j
  h  = inverse (g ∘ f) (∘-is-equiv j i)

  s : g ∘ f ∘ h ∼ id
  s = inverses-are-sections (g ∘ f) (∘-is-equiv j i)

_≃_ : 𝓀 Μ‡ β†’ π“₯ Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡
X ≃ Y = Ξ£ f κž‰ (X β†’ Y), is-equiv f

Eqβ†’fun ⌜_⌝ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X ≃ Y β†’ X β†’ Y
Eq→fun (f , i) = f
⌜_⌝            = Eqβ†’fun

Eqβ†’fun-is-equiv ⌜⌝-is-equiv : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (e : X ≃ Y) β†’ is-equiv (⌜ e ⌝)
Eq→fun-is-equiv (f , i) = i
⌜⌝-is-equiv             = Eqβ†’fun-is-equiv

invertibility-gives-≃ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                      β†’ invertible f β†’ X ≃ Y

invertibility-gives-≃ f i = f , invertibles-are-equivs f i

Ξ£-induction-≃ : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {A : Ξ£ Y β†’ 𝓦 Μ‡ }
              β†’ ((x : X) (y : Y x) β†’ A (x , y)) ≃ ((z : Ξ£ Y) β†’ A z)

Ξ£-induction-≃ = invertibility-gives-≃ Ξ£-induction (curry , refl , refl)

Ξ£-flip : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : X β†’ Y β†’ 𝓦 Μ‡ }
       β†’ (Ξ£ x κž‰ X , Ξ£ y κž‰ Y , A x y) ≃ (Ξ£ y κž‰ Y , Ξ£ x κž‰ X , A x y)

Ξ£-flip = invertibility-gives-≃ (Ξ» (x , y , p) β†’ (y , x , p))
          ((Ξ» (y , x , p) β†’ (x , y , p)) , refl , refl)

Γ—-comm : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
       β†’ (X Γ— Y) ≃ (Y Γ— X)

Γ—-comm = invertibility-gives-≃ (Ξ» (x , y) β†’ (y , x))
          ((Ξ» (y , x) β†’ (x , y)) , refl , refl)

id-≃ : (X : 𝓀 Μ‡ ) β†’ X ≃ X
id-≃ X = 𝑖𝑑 X , id-is-equiv X

_●_ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } β†’ X ≃ Y β†’ Y ≃ Z β†’ X ≃ Z
(f , d) ● (f' , e) = f' ∘ f , ∘-is-equiv e d

≃-sym : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X ≃ Y β†’ Y ≃ X
≃-sym (f , e) = inverse f e , inverses-are-equivs f e

_β‰ƒβŸ¨_⟩_ : (X : 𝓀 Μ‡ ) {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } β†’ X ≃ Y β†’ Y ≃ Z β†’ X ≃ Z
_ β‰ƒβŸ¨ d ⟩ e = d ● e

_β–  : (X : 𝓀 Μ‡ ) β†’ X ≃ X
_β–  = id-≃

transport-is-equiv : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) {x y : X} (p : x ≑ y)
                   β†’ is-equiv (transport A p)

transport-is-equiv A (refl x) = id-is-equiv (A x)

Ξ£-≑-≃ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (Οƒ Ο„ : Ξ£ A)
      β†’ (Οƒ ≑ Ο„) ≃ (Ξ£ p κž‰ pr₁ Οƒ ≑ pr₁ Ο„ , transport A p (prβ‚‚ Οƒ) ≑ prβ‚‚ Ο„)

Ξ£-≑-≃ {𝓀} {π“₯} {X} {A}  Οƒ Ο„ = invertibility-gives-≃ from-Ξ£-≑ (to-Ξ£-≑ , Ξ· , Ξ΅)
 where
  Ξ· : (q : Οƒ ≑ Ο„) β†’ to-Ξ£-≑ (from-Ξ£-≑ q) ≑ q
  Ξ· (refl Οƒ) = refl (refl Οƒ)

  Ξ΅ : (w : Ξ£ p κž‰ pr₁ Οƒ ≑ pr₁ Ο„ , transport A p (prβ‚‚ Οƒ) ≑ prβ‚‚ Ο„)
    β†’ from-Ξ£-≑ (to-Ξ£-≑ w) ≑ w

  Ξ΅ (refl p , refl q) = refl (refl p , refl q)

to-Γ—-≑ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {z t : X Γ— Y}
       β†’ (pr₁ z ≑ pr₁ t) Γ— (prβ‚‚ z ≑ prβ‚‚ t) β†’ z ≑ t

to-Γ—-≑ (refl x , refl y) = refl (x , y)

from-Γ—-≑ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {z t : X Γ— Y}
         β†’ z ≑ t β†’ (pr₁ z ≑ pr₁ t) Γ— (prβ‚‚ z ≑ prβ‚‚ t)

from-Γ—-≑ {𝓀} {π“₯} {X} {Y} (refl (x , y)) = (refl x , refl y)

Γ—-≑-≃ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (z t : X Γ— Y)
      β†’ (z ≑ t) ≃ (pr₁ z ≑ pr₁ t) Γ— (prβ‚‚ z ≑ prβ‚‚ t)

Γ—-≑-≃ {𝓀} {π“₯} {X} {Y} z t = invertibility-gives-≃ from-Γ—-≑ (to-Γ—-≑ , Ξ· , Ξ΅)
 where
  Ξ· : (p : z ≑ t) β†’ to-Γ—-≑ (from-Γ—-≑ p) ≑ p
  Ξ· (refl z) = refl (refl z)

  Ξ΅ : (q : (pr₁ z ≑ pr₁ t) Γ— (prβ‚‚ z ≑ prβ‚‚ t)) β†’ from-Γ—-≑ (to-Γ—-≑ q) ≑ q
  Ξ΅ (refl x , refl y) = refl (refl x , refl y)

ap-pr₁-to-Γ—-≑ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {z t : X Γ— Y}
              β†’ (p₁ : pr₁ z ≑ pr₁ t)
              β†’ (pβ‚‚ : prβ‚‚ z ≑ prβ‚‚ t)
              β†’ ap pr₁ (to-Γ—-≑ (p₁ , pβ‚‚)) ≑ p₁

ap-pr₁-to-Γ—-≑ (refl x) (refl y) = refl (refl x)

ap-prβ‚‚-to-Γ—-≑ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {z t : X Γ— Y}
              β†’ (p₁ : pr₁ z ≑ pr₁ t)
              β†’ (pβ‚‚ : prβ‚‚ z ≑ prβ‚‚ t)
              β†’ ap prβ‚‚ (to-Γ—-≑ (p₁ , pβ‚‚)) ≑ pβ‚‚

ap-prβ‚‚-to-Γ—-≑ (refl x) (refl y) = refl (refl y)

Ξ£-cong : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ }
       β†’ ((x : X) β†’ A x ≃ B x) β†’ Ξ£ A ≃ Ξ£ B

Ξ£-cong {𝓀} {π“₯} {𝓦} {X} {A} {B} Ο† =
  invertibility-gives-≃ (NatΞ£ f) (NatΞ£ g , NatΞ£-Ξ· , NatΞ£-Ξ΅)
 where
  f : (x : X) β†’ A x β†’ B x
  f x = ⌜ Ο† x ⌝

  g : (x : X) β†’ B x β†’ A x
  g x = inverse (f x) (⌜⌝-is-equiv (Ο† x))

  Ξ· : (x : X) (a : A x) β†’ g x (f x a) ≑ a
  Ξ· x = inverses-are-retractions (f x) (⌜⌝-is-equiv (Ο† x))

  Ξ΅ : (x : X) (b : B x) β†’ f x (g x b) ≑ b
  Ξ΅ x = inverses-are-sections (f x) (⌜⌝-is-equiv (Ο† x))

  NatΞ£-Ξ· : (w : Ξ£ A) β†’ NatΞ£ g (NatΞ£ f w) ≑ w
  NatΞ£-Ξ· (x , a) = x , g x (f x a) β‰‘βŸ¨ to-Ξ£-≑' (Ξ· x a) ⟩
                   x , a           ∎

  NatΞ£-Ξ΅ : (t : Ξ£ B) β†’ NatΞ£ f (NatΞ£ g t) ≑ t
  NatΞ£-Ξ΅ (x , b) = x , f x (g x b) β‰‘βŸ¨ to-Ξ£-≑' (Ξ΅ x b) ⟩
                   x , b           ∎

≃-gives-◁ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X ≃ Y β†’ X ◁ Y
≃-gives-◁ (f , e) = (inverse f e , f , inverses-are-retractions f e)

≃-gives-β–· : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X ≃ Y β†’ Y ◁ X
≃-gives-β–· (f , e) = (f , inverse f e , inverses-are-sections f e)

equiv-to-singleton : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                   β†’ X ≃ Y β†’ is-singleton Y β†’ is-singleton X

equiv-to-singleton e = retract-of-singleton (≃-gives-◁ e)

infix  10 _≃_
infixl 30 _●_
infixr  0 _β‰ƒβŸ¨_⟩_
infix   1 _β– 

\end{code}