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