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