Agda UALib β

MartΓ­n EscardΓ³ 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes, which are available online from the following links.

html lecture notes

Source code repository

```
{-# OPTIONS --without-K --exact-split --safe #-}

module MGS-More-FunExt-Consequences where

open import MGS-HAE public
open import MGS-Subsingleton-Theorems public

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

being-subsingleton-is-subsingleton fe {X} i j = c
where
l : is-set X
l = subsingletons-are-sets X i

a : (x y : X) β i x y β‘ j x y
a x y = l x y (i x y) (j x y)

b : (x : X) β i x β‘ j x
b x = fe (a x)

c : i β‘ j
c = fe b

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

being-center-is-subsingleton fe {X} c Ο Ξ³ = k
where
i : is-singleton X
i = c , Ο

j : (x : X) β is-subsingleton (c β‘ x)
j x = singletons-are-sets X i c x

k : Ο β‘ Ξ³
k = fe (Ξ» x β j x (Ο x) (Ξ³ x))

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

Ξ -is-set hfe s f g = b
where
a : is-subsingleton (f βΌ g)
a p q = Ξ³
where
h : β x β  p x β‘ q x
h x = s x (f x) (g x) (p x) (q x)
Ξ³ : p β‘  q
Ξ³ = hfunext-gives-dfunext hfe h

e : (f β‘ g) β (f βΌ g)
e = (happly f g , hfe f g)

b : is-subsingleton (f β‘ g)
b = equiv-to-subsingleton e a

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

being-set-is-subsingleton fe = Ξ -is-subsingleton fe
(Ξ» x β Ξ -is-subsingleton fe
(Ξ» y β being-subsingleton-is-subsingleton fe))

hlevel-relation-is-subsingleton : dfunext π€ π€
β (n : β) (X : π€ Μ )
β is-subsingleton (X is-of-hlevel n)

hlevel-relation-is-subsingleton {π€} fe zero X =
being-singleton-is-subsingleton fe

hlevel-relation-is-subsingleton fe (succ n) X =
Ξ -is-subsingleton fe
(Ξ» x β Ξ -is-subsingleton fe
(Ξ» x' β hlevel-relation-is-subsingleton fe n (x β‘ x')))

β-assoc : dfunext π£ (π€ β π£) β dfunext (π€ β π£) (π€ β π£)
β {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ } {T : π£ Μ }
(Ξ± : X β Y) (Ξ² : Y β Z) (Ξ³ : Z β T)
β Ξ± β (Ξ² β Ξ³) β‘ (Ξ± β Ξ²) β Ξ³

β-assoc fe fe' (f , a) (g , b) (h , c) = ap (h β g β f ,_) q
where
d e : is-equiv (h β g β f)
d = β-is-equiv (β-is-equiv c b) a
e = β-is-equiv c (β-is-equiv b a)

q : d β‘ e
q = being-equiv-is-subsingleton fe fe' (h β g β f) _ _

β-sym-involutive : dfunext π₯ (π€ β π₯) β dfunext (π€ β π₯) (π€ β π₯) β
{X : π€ Μ } {Y : π₯ Μ } (Ξ± : X β Y)
β β-sym (β-sym Ξ±) β‘ Ξ±

β-sym-involutive fe fe' (f , a) = to-subtype-β‘
(being-equiv-is-subsingleton fe fe')
(inversion-involutive f a)

β-sym-is-equiv : dfunext π₯ (π€ β π₯) β dfunext π€ (π€ β π₯) β dfunext (π€ β π₯) (π€ β π₯)
β {X : π€ Μ } {Y : π₯ Μ }
β is-equiv (β-sym {π€} {π₯} {X} {Y})

β-sym-is-equiv feβ feβ feβ = invertibles-are-equivs β-sym
(β-sym ,
β-sym-involutive feβ feβ ,
β-sym-involutive feβ feβ)

β-sym-β : dfunext π₯ (π€ β π₯) β dfunext π€ (π€ β π₯) β dfunext (π€ β π₯) (π€ β π₯)
β (X : π€ Μ ) (Y : π₯ Μ )
β (X β Y) β (Y β X)

β-sym-β feβ feβ feβ X Y = β-sym , β-sym-is-equiv feβ feβ feβ

Ξ -cong : dfunext π€ π₯ β dfunext π€ π¦
β {X : π€ Μ } {Y : X β π₯ Μ } {Y' : X β π¦ Μ }
β ((x : X) β Y x β Y' x) β Ξ  Y β Ξ  Y'

Ξ -cong fe fe' {X} {Y} {Y'} Ο = invertibility-gives-β F (G , GF , FG)
where
f : (x : X) β Y x β Y' x
f x = β Ο x β

e : (x : X) β is-equiv (f x)
e x = ββ-is-equiv (Ο x)

g : (x : X) β Y' x β Y x
g x = inverse (f x) (e x)

fg : (x : X) (y' : Y' x) β f x (g x y') β‘ y'
fg x = inverses-are-sections (f x) (e x)

gf : (x : X) (y : Y x) β g x (f x y) β‘ y
gf x = inverses-are-retractions (f x) (e x)

F : ((x : X) β Y x) β ((x : X) β Y' x)
F Ο x = f x (Ο x)

G : ((x : X) β Y' x) β (x : X) β Y x
G Ξ³ x = g x (Ξ³ x)

FG : (Ξ³ : ((x : X) β Y' x)) β F(G Ξ³) β‘ Ξ³
FG Ξ³ = fe' (Ξ» x β fg x (Ξ³ x))

GF : (Ο : ((x : X) β Y x)) β G(F Ο) β‘ Ο
GF Ο = fe (Ξ» x β gf x (Ο x))

hfunext-β : hfunext π€ π₯
β {X : π€ Μ } {A : X β π₯ Μ } (f g : Ξ  A)
β (f β‘ g) β (f βΌ g)

hfunext-β hfe f g = (happly f g , hfe f g)

hfunextβ-β : hfunext π€ (π₯ β π¦) β hfunext π₯ π¦
β {X : π€ Μ } {Y : X β π₯ Μ } {A : (x : X) β Y x β π¦ Μ }
(f g : (x : X) (y : Y x) β A x y)
β (f β‘ g) β (β x y β f x y β‘ g x y)

hfunextβ-β fe fe' {X} f g =

(f β‘ g)                  ββ¨ i  β©
(β x β f x β‘ g x)        ββ¨ ii β©
(β x y β f x y β‘ g x y)  β

where
i  = hfunext-β fe f g
ii = Ξ -cong
(hfunext-gives-dfunext fe)
(hfunext-gives-dfunext fe)
(Ξ» x β hfunext-β fe' (f x) (g x))

precomp-invertible : dfunext π₯ π¦ β dfunext π€ π¦
β {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ } (f : X β Y)
β invertible f
β invertible (Ξ» (h : Y β Z) β h β f)

precomp-invertible fe fe' {X} {Y} {Z} f (g , Ξ· , Ξ΅) = (g' , Ξ·' , Ξ΅')
where
f' : (Y β Z) β (X β Z)
f' h = h β f

g' : (X β Z) β (Y β Z)
g' k = k β g

Ξ·' : (h : Y β Z) β g' (f' h) β‘ h
Ξ·' h = fe (Ξ» y β ap h (Ξ΅ y))

Ξ΅' : (k : X β Z) β f' (g' k) β‘ k
Ξ΅' k = fe' (Ξ» x β ap k (Ξ· x))

at-most-one-section : dfunext π₯ π€ β hfunext π₯ π₯
β {X : π€ Μ } {Y : π₯ Μ } (f : X β Y)
β has-retraction f
β is-subsingleton (has-section f)

at-most-one-section {π₯} {π€} fe hfe {X} {Y} f (g , gf) (h , fh) = d
where
fe' : dfunext π₯ π₯
fe' = hfunext-gives-dfunext hfe

a : invertible f
a = joyal-equivs-are-invertible f ((h , fh) , (g , gf))

b : is-singleton (fiber (Ξ» h β  f β h) id)
b = invertibles-are-equivs (Ξ» h β f β h) (postcomp-invertible fe fe' f a) id

r : fiber (Ξ» h β  f β h) id β has-section f
r (h , p) = (h , happly (f β h) id p)

s : has-section f β fiber (Ξ» h β f β h) id
s (h , Ξ·) = (h , fe' Ξ·)

rs : (Ο : has-section f) β r (s Ο) β‘ Ο
rs (h , Ξ·) = to-Ξ£-β‘' q
where
q : happly (f β h) id (inverse (happly (f β h) id) (hfe (f β h) id) Ξ·) β‘ Ξ·
q = inverses-are-sections (happly (f β h) id) (hfe (f β h) id) Ξ·

c : is-singleton (has-section f)
c = retract-of-singleton (r , s , rs) b

d : (Ο : has-section f) β h , fh β‘ Ο
d = singletons-are-subsingletons (has-section f) c (h , fh)

at-most-one-retraction : hfunext π€ π€ β dfunext π₯ π€
β {X : π€ Μ } {Y : π₯ Μ } (f : X β Y)
β has-section f
β is-subsingleton (has-retraction f)

at-most-one-retraction {π€} {π₯} hfe fe' {X} {Y} f (g , fg) (h , hf) = d
where
fe : dfunext π€ π€
fe = hfunext-gives-dfunext hfe

a : invertible f
a = joyal-equivs-are-invertible f ((g , fg) , (h , hf))

b : is-singleton (fiber (Ξ» h β  h β f) id)
b = invertibles-are-equivs (Ξ» h β h β f) (precomp-invertible fe' fe f a) id

r : fiber (Ξ» h β  h β f) id β has-retraction f
r (h , p) = (h , happly (h β f) id p)

s : has-retraction f β fiber (Ξ» h β  h β f) id
s (h , Ξ·) = (h , fe Ξ·)

rs : (Ο : has-retraction f) β r (s Ο) β‘ Ο
rs (h , Ξ·) = to-Ξ£-β‘' q
where
q : happly (h β f) id (inverse (happly (h β f) id) (hfe (h β f) id) Ξ·) β‘ Ξ·
q = inverses-are-sections (happly (h β f) id) (hfe (h β f) id) Ξ·

c : is-singleton (has-retraction f)
c = retract-of-singleton (r , s , rs) b

d : (Ο : has-retraction f) β h , hf β‘ Ο
d = singletons-are-subsingletons (has-retraction f) c (h , hf)

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

being-joyal-equiv-is-subsingleton feβ feβ feβ f = Γ-is-subsingleton'
(at-most-one-section    feβ feβ f ,
at-most-one-retraction feβ feβ f)

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

being-hae-is-subsingleton feβ feβ feβ {X} {Y} f = subsingleton-criterion' Ξ³
where
a = Ξ» g Ξ΅ x
β ((g (f x) , Ξ΅ (f x)) β‘ (x , refl (f x)))                                   ββ¨ i  g Ξ΅ x β©
(Ξ£ p κ g (f x) β‘ x , transport (Ξ» - β f - β‘ f x) p (Ξ΅ (f x)) β‘ refl (f x)) ββ¨ ii g Ξ΅ x β©
(Ξ£ p κ g (f x) β‘ x , ap f p β‘ Ξ΅ (f x))                                     β
where
i  = Ξ» g Ξ΅ x β Ξ£-β‘-β (g (f x) , Ξ΅ (f x)) (x , refl (f x))
ii = Ξ» g Ξ΅ x β Ξ£-cong (Ξ» p β transport-ap-β f p (Ξ΅ (f x)))

b = (Ξ£ (g , Ξ΅) κ has-section f , β x β (g (f x) , Ξ΅ (f x)) β‘ (x , refl (f x)))         ββ¨ i   β©
(Ξ£ (g , Ξ΅) κ has-section f , β x β Ξ£  p κ g (f x) β‘ x , ap f p β‘ Ξ΅ (f x))          ββ¨ ii  β©
(Ξ£ g κ (Y β X) , Ξ£ Ξ΅ κ f β g βΌ id , β x β Ξ£  p κ g (f x) β‘ x , ap f p β‘ Ξ΅ (f x))   ββ¨ iii β©
(Ξ£ g κ (Y β X) , Ξ£ Ξ΅ κ f β g βΌ id , Ξ£ Ξ· κ g β f βΌ id , β x β ap f (Ξ· x) β‘ Ξ΅ (f x)) ββ¨ iv  β©
is-hae f                                                                           β
where
i   = Ξ£-cong (Ξ» (g , Ξ΅) β Ξ -cong feβ feβ (a g Ξ΅))
ii  = Ξ£-assoc
iii = Ξ£-cong (Ξ» g β Ξ£-cong (Ξ» Ξ΅ β Ξ Ξ£-distr-β))
iv  = Ξ£-cong (Ξ» g β Ξ£-flip)

Ξ³ : is-hae f β is-subsingleton (is-hae f)
Ξ³ (gβ , Ξ΅β , Ξ·β , Οβ) = i
where
c : (x : X) β is-set (fiber f (f x))
c x = singletons-are-sets (fiber f (f x)) (haes-are-equivs f (gβ , Ξ΅β , Ξ·β , Οβ) (f x))

d : ((g , Ξ΅) : has-section f) β is-subsingleton (β x β (g (f x) , Ξ΅ (f x)) β‘ (x , refl (f x)))
d (g , Ξ΅) = Ξ -is-subsingleton feβ (Ξ» x β c x (g (f x) , Ξ΅ (f x)) (x , refl (f x)))

e : is-subsingleton (Ξ£ (g , Ξ΅) κ has-section f , β x β (g (f x) , Ξ΅ (f x)) β‘ (x , refl (f x)))
e = Ξ£-is-subsingleton (at-most-one-section feβ feβ f (gβ , Ξ΅β)) d

i : is-subsingleton (is-hae f)
i = equiv-to-subsingleton (β-sym b) e

emptiness-is-subsingleton : dfunext π€ π€β β (X : π€ Μ )
β is-subsingleton (is-empty X)

emptiness-is-subsingleton fe X f g = fe (Ξ» x β !π (f x β‘ g x) (f x))

+-is-subsingleton : {P : π€ Μ } {Q : π₯ Μ }
β is-subsingleton P
β is-subsingleton Q
β (P β Q β π) β is-subsingleton (P + Q)

+-is-subsingleton {π€} {π₯} {P} {Q} i j f = Ξ³
where
Ξ³ : (x y : P + Q) β x β‘ y
Ξ³ (inl p) (inl p') = ap inl (i p p')
Ξ³ (inl p) (inr q)  = !π (inl p β‘ inr q) (f p q)
Ξ³ (inr q) (inl p)  = !π (inr q β‘ inl p) (f p q)
Ξ³ (inr q) (inr q') = ap inr (j q q')

+-is-subsingleton' : dfunext π€ π€β
β {P : π€ Μ } β is-subsingleton P β is-subsingleton (P + Β¬ P)

+-is-subsingleton' fe {P} i = +-is-subsingleton i
(emptiness-is-subsingleton fe P)
(Ξ» p n β n p)

EM-is-subsingleton : dfunext (π€ βΊ) π€ β dfunext π€ π€ β dfunext π€ π€β
β is-subsingleton (EM π€)

EM-is-subsingleton feβΊ fe feβ = Ξ -is-subsingleton feβΊ
(Ξ» P β Ξ -is-subsingleton fe
(Ξ» i β +-is-subsingleton' feβ i))
```