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 --without-K --exact-split --safe #-}

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}