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-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 _β_