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.Embeddings where

open import MGS.More-FunExt-Consequences public

is-embedding : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ Μ
is-embedding f = (y : codomain f) β is-subsingleton (fiber f y)

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

being-embedding-is-subsingleton fe f =
Ξ -is-subsingleton fe
(Ξ» x β being-subsingleton-is-subsingleton fe)

prβ-embedding : (A : π€ Μ ) (X : π₯ Μ )
β is-subsingleton A
β is-embedding (Ξ» (z : A Γ X) β prβ z)

prβ-embedding A X i x ((a , x) , refl x) ((b , x) , refl x) = p
where
p : ((a , x) , refl x) οΌ ((b , x) , refl x)
p = ap (Ξ» - β ((- , x) , refl x)) (i a b)

prβ-embedding : {X : π€ Μ } {A : X β π₯ Μ }
β ((x : X) β is-subsingleton (A x))
β is-embedding (Ξ» (Ο : Ξ£ A) β prβ Ο)

prβ-embedding i x ((x , a) , refl x) ((x , a') , refl x) = Ξ³
where
p : a οΌ a'
p = i x a a'

Ξ³ : (x , a) , refl x οΌ (x , a') , refl x
Ξ³ = ap (Ξ» - β (x , -) , refl x) p

equivs-are-embeddings : {X : π€ Μ } {Y : π₯ Μ }
(f : X β Y)
β is-equiv f β is-embedding f

equivs-are-embeddings f i y = singletons-are-subsingletons (fiber f y) (i y)

id-is-embedding : {X : π€ Μ } β is-embedding (ππ X)
id-is-embedding {π€} {X} = equivs-are-embeddings id (id-is-equiv X)

β-embedding : {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ }
{f : X β Y} {g : Y β Z}
β is-embedding g  β is-embedding f β is-embedding (g β f)

β-embedding {π€} {π₯} {π¦} {X} {Y} {Z} {f} {g} d e = h
where
A : (z : Z) β π€ β π₯ β π¦ Μ
A z = Ξ£ (y , p) κ fiber g z , fiber f y

i : (z : Z) β is-subsingleton (A z)
i z = Ξ£-is-subsingleton (d z) (Ξ» w β e (prβ w))

Ο : (z : Z) β fiber (g β f) z β A z
Ο z (x , p) = (f x , p) , x , refl (f x)

Ξ³ : (z : Z) β A z β fiber (g β f) z
Ξ³ z ((_ , p) , x , refl _) = x , p

Ξ· : (z : Z) (t : fiber (g β f) z) β Ξ³ z (Ο z t) οΌ t
Ξ· _ (x , refl _) = refl (x , refl ((g β f) x))

h : (z : Z) β is-subsingleton (fiber (g β f) z)
h z = lc-maps-reflect-subsingletons (Ο z) (sections-are-lc (Ο z) (Ξ³ z , Ξ· z)) (i z)

embedding-lemma : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y)
β ((x : X) β is-singleton (fiber f (f x)))
β is-embedding f

embedding-lemma f Ο = Ξ³
where
Ξ³ : (y : codomain f) (u v : fiber f y) β u οΌ v
Ξ³ y (x , p) v = j (x , p) v
where
q : fiber f (f x) οΌ fiber f y
q = ap (fiber f) p

i : is-singleton (fiber f y)
i = transport is-singleton q (Ο x)

j : is-subsingleton (fiber f y)
j = singletons-are-subsingletons (fiber f y) i

embedding-criterion : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y)
β ((x x' : X) β (f x οΌ f x') β (x οΌ x'))
β is-embedding f

embedding-criterion f e = embedding-lemma f b
where
X = domain f

a : (x : X) β (Ξ£ x' κ X , f x' οΌ f x) β (Ξ£ x' κ X , x' οΌ x)
a x = Ξ£-cong (Ξ» x' β e x' x)

a' : (x : X) β fiber f (f x) β singleton-type x
a' = a

b : (x : X) β is-singleton (fiber f (f x))
b x = equiv-to-singleton (a' x) (singleton-types-are-singletons X x)

ap-is-equiv-gives-embedding : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y)
β ((x x' : X) β is-equiv (ap f {x} {x'}))
β is-embedding f

ap-is-equiv-gives-embedding f i = embedding-criterion f
(Ξ» x' x β β-sym (ap f {x'} {x} , i x' x))

embedding-gives-ap-is-equiv : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y)
β is-embedding f
β (x x' : X) β is-equiv (ap f {x} {x'})

embedding-gives-ap-is-equiv {π€} {π₯} {X} f e = Ξ³
where
d : (x' : X) β (Ξ£ x κ X , f x' οΌ f x) β (Ξ£ x κ X , f x οΌ f x')
d x' = Ξ£-cong (Ξ» x β β»ΒΉ-β (f x') (f x))

s : (x' : X) β is-subsingleton (Ξ£ x κ X , f x' οΌ f x)
s x' = equiv-to-subsingleton (d x') (e (f x'))

Ξ³ : (x x' : X) β is-equiv (ap f {x} {x'})
Ξ³ x = singleton-equiv-lemma x (Ξ» x' β ap f {x} {x'})
(pointed-subsingletons-are-singletons
(Ξ£ x' κ X , f x οΌ f x') (x , (refl (f x))) (s x))

embedding-criterion-converse : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y)
β is-embedding f
β ((x' x : X) β (f x' οΌ f x) β (x' οΌ x))

embedding-criterion-converse f e x' x = β-sym
(ap f {x'} {x} ,
embedding-gives-ap-is-equiv f e x' x)

embeddings-are-lc : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y)
β is-embedding f
β left-cancellable f

embeddings-are-lc f e {x} {y} = β embedding-criterion-converse f e x y β

embedding-with-section-is-equiv : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y)
β is-embedding f
β has-section f
β is-equiv f
embedding-with-section-is-equiv f i (g , Ξ·) y = pointed-subsingletons-are-singletons
(fiber f y) (g y , Ξ· y) (i y)

NatΞ  : {X : π€ Μ } {A : X β π₯ Μ } {B : X β π¦ Μ } β Nat A B β Ξ  A β Ξ  B
NatΞ  Ο f x = Ο x (f x)

NatΞ -is-embedding : hfunext π€ π₯
β hfunext π€ π¦
β {X : π€ Μ } {A : X β π₯ Μ } {B : X β π¦ Μ }
β (Ο : Nat A B)
β ((x : X) β is-embedding (Ο x))
β is-embedding (NatΞ  Ο)

NatΞ -is-embedding v w {X} {A} Ο i = embedding-criterion (NatΞ  Ο) Ξ³
where
Ξ³ : (f g : Ξ  A) β (NatΞ  Ο f οΌ NatΞ  Ο g) β (f οΌ g)
Ξ³ f g = (NatΞ  Ο f οΌ NatΞ  Ο g) ββ¨ hfunext-β w (NatΞ  Ο f) (NatΞ  Ο g) β©
(NatΞ  Ο f βΌ NatΞ  Ο g) ββ¨ b β©
(f βΌ g)               ββ¨ β-sym (hfunext-β v f g) β©
(f οΌ g)               β

where
a : (x : X) β (NatΞ  Ο f x οΌ NatΞ  Ο g x) β (f x οΌ g x)
a x = embedding-criterion-converse (Ο x) (i x) (f x) (g x)

b : (NatΞ  Ο f βΌ NatΞ  Ο g) β (f βΌ g)
b = Ξ -cong (hfunext-gives-dfunext w) (hfunext-gives-dfunext v) a

_βͺ_ : π€ Μ β π₯ Μ β π€ β π₯ Μ
X βͺ Y = Ξ£ f κ (X β Y), is-embedding f

Embβfun : {X : π€ Μ } {Y : π₯ Μ } β X βͺ Y β X β Y
Embβfun (f , i) = f

\end{code}