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.Subsingleton-Theorems where

open import MGS.FunExt-from-Univalence public

Ξ -is-subsingleton : dfunext π€ π₯
β {X : π€ Μ } {A : X β π₯ Μ }
β ((x : X) β is-subsingleton (A x))
β is-subsingleton (Ξ  A)

Ξ -is-subsingleton fe i f g = fe (Ξ» x β i x (f x) (g x))

being-singleton-is-subsingleton : dfunext π€ π€
β {X : π€ Μ }
β is-subsingleton (is-singleton X)

being-singleton-is-subsingleton fe {X} (x , Ο) (y , Ξ³) = p
where
i : is-subsingleton X
i = singletons-are-subsingletons X (y , Ξ³)

s : is-set X
s = subsingletons-are-sets X i

a : (z : X) β is-subsingleton ((t : X) β z οΌ t)
a z = Ξ -is-subsingleton fe (s z)

b : x οΌ y
b = Ο y

p : (x , Ο) οΌ (y , Ξ³)
p = to-subtype-οΌ a b

being-equiv-is-subsingleton : dfunext π₯ (π€ β π₯) β dfunext (π€ β π₯) (π€ β π₯)
β {X : π€ Μ } {Y : π₯ Μ } (f : X β Y)
β is-subsingleton (is-equiv f)

being-equiv-is-subsingleton fe fe' f = Ξ -is-subsingleton fe
(Ξ» x β being-singleton-is-subsingleton fe')

subsingletons-are-retracts-of-logically-equivalent-types : {X : π€ Μ } {Y : π₯ Μ }
β is-subsingleton X
β (X β Y)
β X β Y

subsingletons-are-retracts-of-logically-equivalent-types i (f , g) = g , f , Ξ·
where
Ξ· : g β f βΌ id
Ξ· x = i (g (f x)) x

equivalence-property-is-retract-of-invertibility-data : dfunext π₯ (π€ β π₯) β dfunext (π€ β π₯) (π€ β π₯)
β {X : π€ Μ } {Y : π₯ Μ } (f : X β Y)
β is-equiv f β invertible f

equivalence-property-is-retract-of-invertibility-data fe fe' f =
subsingletons-are-retracts-of-logically-equivalent-types
(being-equiv-is-subsingleton fe fe' f) (equivs-are-invertible f , invertibles-are-equivs f)

univalence-is-subsingleton : is-univalent (π€ βΊ)
β is-subsingleton (is-univalent π€)

univalence-is-subsingleton {π€} uaβΊ = subsingleton-criterion' Ξ³
where
Ξ³ : is-univalent π€ β is-subsingleton (is-univalent π€)
Ξ³ ua = i
where
dfeβ : dfunext  π€    (π€ βΊ)
dfeβ : dfunext (π€ βΊ) (π€ βΊ)

dfeβ = univalence-gives-dfunext' ua uaβΊ
dfeβ = univalence-gives-dfunext uaβΊ

i : is-subsingleton (is-univalent π€)
i = Ξ -is-subsingleton dfeβ
(Ξ» X β Ξ -is-subsingleton dfeβ
(Ξ» Y β being-equiv-is-subsingleton dfeβ dfeβ (IdβEq X Y)))

Univalence : π€Ο
Univalence = β π€ β is-univalent π€

univalence-is-subsingletonΟ : Univalence β is-subsingleton (is-univalent π€)
univalence-is-subsingletonΟ {π€} Ξ³ = univalence-is-subsingleton (Ξ³ (π€ βΊ))

univalence-is-a-singleton : Univalence β is-singleton (is-univalent π€)
univalence-is-a-singleton {π€} Ξ³ = pointed-subsingletons-are-singletons
(is-univalent π€)
(Ξ³ π€)
(univalence-is-subsingletonΟ Ξ³)

global-dfunext : π€Ο
global-dfunext = β {π€ π₯} β dfunext π€ π₯

univalence-gives-global-dfunext : Univalence β global-dfunext
univalence-gives-global-dfunext ua {π€} {π₯} = univalence-gives-dfunext'
(ua π€) (ua (π€ β π₯))

global-hfunext : π€Ο
global-hfunext = β {π€ π₯} β hfunext π€ π₯

univalence-gives-global-hfunext : Univalence β global-hfunext
univalence-gives-global-hfunext ua {π€} {π₯} = univalence-gives-hfunext'
(ua π€) (ua (π€ β π₯))

Ξ -is-subsingleton' : dfunext π€ π₯ β {X : π€ Μ } {A : X β π₯ Μ }
β ((x : X) β is-subsingleton (A x))
β is-subsingleton ({x : X} β A x)

Ξ -is-subsingleton' fe {X} {A} i = Ξ³
where
Ο : ({x : X} β A x) β Ξ  A
Ο = (Ξ» f {x} β f x) , (Ξ» g x β g {x}) , (Ξ» f β refl (Ξ» {x} β f))

Ξ³ : is-subsingleton ({x : X} β A x)
Ξ³ = retract-of-subsingleton Ο (Ξ -is-subsingleton fe i)

vv-and-hfunext-are-subsingletons-lemma  : dfunext (π€ βΊ)       (π€ β (π₯ βΊ))
β dfunext (π€ β (π₯ βΊ)) (π€ β π₯)
β dfunext (π€ β π₯)     (π€ β π₯)

β is-subsingleton (vvfunext π€ π₯)
Γ is-subsingleton (hfunext  π€ π₯)

vv-and-hfunext-are-subsingletons-lemma {π€} {π₯} dfe dfe' dfe'' = Ο , Ξ³
where
Ο : is-subsingleton (vvfunext π€ π₯)
Ο = Ξ -is-subsingleton' dfe
(Ξ» X β Ξ -is-subsingleton' dfe'
(Ξ» A β Ξ -is-subsingleton dfe''
(Ξ» i β being-singleton-is-subsingleton dfe'')))

Ξ³ : is-subsingleton (hfunext π€ π₯)
Ξ³ = Ξ -is-subsingleton' dfe
(Ξ» X β Ξ -is-subsingleton' dfe'
(Ξ» A β Ξ -is-subsingleton dfe''
(Ξ» f β Ξ -is-subsingleton dfe''
(Ξ» g β being-equiv-is-subsingleton dfe'' dfe''
(happly f g)))))

vv-and-hfunext-are-singletons : Univalence
β is-singleton (vvfunext π€ π₯)
Γ is-singleton (hfunext  π€ π₯)

vv-and-hfunext-are-singletons {π€} {π₯} ua =

f (vv-and-hfunext-are-subsingletons-lemma
(univalence-gives-dfunext' (ua (π€ βΊ))       (ua ((π€ βΊ) β (π₯ βΊ))))
(univalence-gives-dfunext' (ua (π€ β (π₯ βΊ))) (ua (π€ β (π₯ βΊ))))
(univalence-gives-dfunext' (ua (π€ β π₯))     (ua (π€ β π₯))))

where
f : is-subsingleton (vvfunext π€ π₯) Γ is-subsingleton (hfunext π€ π₯)
β is-singleton (vvfunext π€ π₯) Γ is-singleton (hfunext π€ π₯)

f (i , j) = pointed-subsingletons-are-singletons (vvfunext π€ π₯)
(univalence-gives-vvfunext' (ua π€) (ua (π€ β π₯))) i ,

pointed-subsingletons-are-singletons (hfunext π€ π₯)
(univalence-gives-hfunext' (ua π€) (ua (π€ β π₯))) j
\end{code}