Martin Escardo

\begin{code}

{-# OPTIONS --safe --without-K #-}

module UF.Embeddings where

open import MLTT.Spartan
open import MLTT.Plus-Properties
open import UF.Base
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.LeftCancellable
open import UF.Lower-FunExt
open import UF.Retracts
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties
open import UF.UA-FunExt
open import UF.Univalence
open import UF.Yoneda

is-embedding : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
is-embedding f = each-fiber-of f is-prop

being-embedding-is-prop : funext (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯)
                        β†’ {X : 𝓀 Μ‡ }
                          {Y : π“₯ Μ‡ }
                          (f : X β†’ Y)
                        β†’ is-prop (is-embedding f)
being-embedding-is-prop {𝓀} {π“₯} fe f =
 Ξ -is-prop (lower-funext 𝓀 𝓀 fe) (Ξ» x β†’ being-prop-is-prop fe)

id-is-embedding : {X : 𝓀 Μ‡ } β†’ is-embedding (id {𝓀} {X})
id-is-embedding = singleton-types'-are-props

∘-is-embedding : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
                 {f : X β†’ Y} {g : Y β†’ Z}
               β†’ is-embedding f
               β†’ is-embedding g
               β†’ is-embedding (g ∘ f)
∘-is-embedding {𝓀} {π“₯} {𝓦} {X} {Y} {Z} {f} {g} e d = h
 where
  T : (z : Z) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
  T z = Ξ£ (y , _) κž‰ fiber g z , fiber f y

  T-is-prop : (z : Z) β†’ is-prop (T z)
  T-is-prop z = subtypes-of-props-are-props'
                 pr₁
                 (pr₁-lc (Ξ» {t} β†’ e (pr₁ t)))
                 (d z)

  Ο† : (z : Z) β†’ fiber (g ∘ f) z β†’ T z
  Ο† z (x , p) = (f x , p) , x , refl

  Ξ³ : (z : Z) β†’ T z β†’ fiber (g ∘ f) z
  Ξ³ z ((.(f x) , p) , x , refl) = x , p

  Ξ³Ο† : (z : Z) (t : fiber (g ∘ f) z) β†’ Ξ³ z (Ο† z t) ＝ t
  Ξ³Ο† .(g (f x)) (x , refl) = refl

  h : (z : Z) β†’ is-prop (fiber (g ∘ f) z)
  h z = subtypes-of-props-are-props'
         (Ο† z)
         (sections-are-lc (Ο† z) (Ξ³ z , (Ξ³Ο† z)))
         (T-is-prop z)

_β†ͺ_ : 𝓀 Μ‡ β†’ π“₯ Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡
X β†ͺ Y = Ξ£ f κž‰ (X β†’ Y) , is-embedding f

β†ͺ-refl : (X : 𝓀 Μ‡ ) β†’ X β†ͺ X
β†ͺ-refl X = id , id-is-embedding

_∘β†ͺ_ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
     β†’ Y β†ͺ Z
     β†’ X β†ͺ Y
     β†’ X β†ͺ Z
(g , j) ∘β†ͺ (f , i) = g ∘ f , ∘-is-embedding i j

⌊_βŒ‹ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X β†ͺ Y β†’ X β†’ Y
⌊ f , _ βŒ‹     = f

⌊_βŒ‹-is-embedding : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (e : X β†ͺ Y)
                 β†’ is-embedding ⌊ e βŒ‹
⌊ _ , i βŒ‹-is-embedding = i

_β†ͺ⟨_⟩_ : (X : 𝓀 Μ‡ ) {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } β†’ X β†ͺ Y β†’ Y β†ͺ Z β†’ X β†ͺ Z
_ β†ͺ⟨ f , i ⟩ (g , j) = (g ∘ f) , (∘-is-embedding i j)

_β–‘ : (X : 𝓀 Μ‡ ) β†’ X β†ͺ X
_β–‘ X = id , id-is-embedding

embedding-criterion : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                    β†’ ((x : X) β†’ is-prop (fiber f (f x)))
                    β†’ is-embedding f
embedding-criterion f Ο† .(f x) (x , refl) = Ο† x (x , refl)

embedding-criterion' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                    β†’ ((x x' : X) β†’ (f x ＝ f x') ≃ (x ＝ x'))
                    β†’ is-embedding f
embedding-criterion' {𝓀} {π“₯} {X} {Y} f e =
 embedding-criterion f
  (Ξ» x' β†’ equiv-to-prop (a x')
  (singleton-types'-are-props x'))
 where
  a : (x' : X) β†’ fiber f (f x') ≃ (Ξ£ x κž‰ X , x ＝ x')
  a x' = Ξ£-cong (Ξ» x β†’ e x x')

vv-equivs-are-embeddings : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                         β†’ is-vv-equiv f
                         β†’ is-embedding f
vv-equivs-are-embeddings f e y = singletons-are-props (e y)

equivs-are-embeddings : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                      β†’ is-equiv f
                      β†’ is-embedding f
equivs-are-embeddings f e = vv-equivs-are-embeddings f
                             (equivs-are-vv-equivs f e)

equivs-are-embeddings' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (𝕗 : X ≃ Y)
                      β†’ is-embedding ⌜ 𝕗 ⌝
equivs-are-embeddings' (f , e) = equivs-are-embeddings f e

≃-gives-β†ͺ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X ≃ Y β†’ X β†ͺ Y
≃-gives-β†ͺ (f , i) = (f , equivs-are-embeddings f i)

embeddings-with-sections-are-vv-equivs : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                                       β†’ is-embedding f
                                       β†’ has-section f
                                       β†’ is-vv-equiv f
embeddings-with-sections-are-vv-equivs f i (g , Ξ·) y =
 pointed-props-are-singletons (g y , Ξ· y) (i y)

embeddings-with-sections-are-equivs : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                                    β†’ is-embedding f
                                    β†’ has-section f
                                    β†’ is-equiv f
embeddings-with-sections-are-equivs f i h =
 vv-equivs-are-equivs f (embeddings-with-sections-are-vv-equivs f i h)

Subtype' : (𝓀 {π“₯} : Universe) β†’ π“₯ Μ‡ β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
Subtype' 𝓀 {π“₯} Y = Ξ£ X κž‰ 𝓀 Μ‡ , X β†ͺ Y

Subtype : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
Subtype {𝓀} Y = Subtype' 𝓀 Y

etofun : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†ͺ Y) β†’ (X β†’ Y)
etofun = pr₁

is-embedding-etofun : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                    β†’ (e : X β†ͺ Y)
                    β†’ is-embedding (etofun e)
is-embedding-etofun = prβ‚‚

equivs-embedding : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X ≃ Y β†’ X β†ͺ Y
equivs-embedding e = ⌜ e ⌝ , equivs-are-embeddings ⌜ e ⌝ (⌜⌝-is-equiv e)

embeddings-are-lc : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                  β†’ is-embedding f
                  β†’ left-cancellable f
embeddings-are-lc f e {x} {x'} p = ap pr₁ (e (f x) (x , refl) (x' , (p ⁻¹)))

subtypes-of-props-are-props : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (e : X β†’ Y)
                             β†’ is-embedding e
                             β†’ is-prop Y
                             β†’ is-prop X
subtypes-of-props-are-props e i =
 subtypes-of-props-are-props' e (embeddings-are-lc e i)

subtypes-of-sets-are-sets : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (e : X β†’ Y)
                          β†’ is-embedding e
                          β†’ is-set Y
                          β†’ is-set X
subtypes-of-sets-are-sets e i =
 subtypes-of-sets-are-sets' e (embeddings-are-lc e i)

is-embedding' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
is-embedding' f = βˆ€ x x' β†’ is-equiv (ap f {x} {x'})

embedding-gives-embedding' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                           β†’ is-embedding f
                           β†’ is-embedding' f
embedding-gives-embedding' {𝓀} {π“₯} {X} {Y} f ise = g
 where
  b : (x : X) β†’ is-singleton (fiber f (f x))
  b x = (x , refl) , ise (f x) (x , refl)

  c : (x : X) β†’ is-singleton (fiber' f (f x))
  c x = retract-of-singleton
         (≃-gives-β–· (fiber-lemma f (f x)))
         (b x)

  g : (x x' : X) β†’ is-equiv (ap f {x} {x'})
  g x = universality-equiv x refl
         (central-point-is-universal
         (Ξ» x' β†’ f x ＝ f x')
         (center (c x))
         (centrality (c x)))

\end{code}

Added 27 June 2024.  It follows that if f is an equivalence, then so
is ap f.  It is added here, rather than in UF.EquivalenceExamples, to
avoid cyclic module dependencies.

\begin{code}

ap-is-equiv : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
            β†’ is-equiv f
            β†’ {x x' : X} β†’ is-equiv (ap f {x} {x'})
ap-is-equiv f e {x} {x'} =
 embedding-gives-embedding' f (equivs-are-embeddings f e) x x'

embedding-criterion-converse' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                             β†’ is-embedding f
                             β†’ (x' x : X)
                             β†’ (x' ＝ x) ≃ (f x' ＝ f x)
embedding-criterion-converse' f e x' x = ap f {x'} {x} ,
                                         embedding-gives-embedding' f e x' 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 (embedding-criterion-converse' f e x' x)

embedding'-gives-embedding : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                             (f : X β†’ Y)
                           β†’ is-embedding' f
                           β†’ is-embedding f
embedding'-gives-embedding {𝓀} {π“₯} {X} {Y} f ise = g
 where
  e : (x : X) β†’ is-central (Ξ£ x' κž‰ X , f x ＝ f x') (x , refl)
  e x = universal-element-is-central
         (x , refl)
         (equiv-universality x refl (ise x))

  h : (x : X) β†’ is-prop (fiber' f (f x))
  h x Οƒ Ο„ = Οƒ          ＝⟨ (e x Οƒ)⁻¹ ⟩
            (x , refl) ＝⟨ e x Ο„ ⟩
            Ο„          ∎

  g' : (y : Y) β†’ is-prop (fiber' f y)
  g' y (x , p) = transport
                  (Ξ» - β†’ is-prop (Ξ£ x' κž‰ X , - ＝ f x'))
                  (p ⁻¹)
                  (h x)
                  (x , p)

  g : (y : Y) β†’ is-prop (fiber f y)
  g y = left-cancellable-reflects-is-prop
         ⌜ fiber-lemma f y ⌝
         (section-lc _
           (equivs-are-sections _ (⌜⌝-is-equiv (fiber-lemma f y ))))
         (g' y)

pr₁-is-embedding : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ }
                 β†’ ((x : X) β†’ is-prop (Y x))
                 β†’ is-embedding (pr₁ {𝓀} {π“₯} {X} {Y})
pr₁-is-embedding f x ((x , y') , refl) ((x , y'') , refl) = g
 where
  g : (x , y') , refl ＝ (x , y'') , refl
  g = ap (Ξ» - β†’ (x , -) , refl) (f x y' y'')


to-subtype-＝-≃ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
                β†’ ((x : X) β†’ is-prop (A x))
                β†’ {x y : X} {a : A x} {b : A y}
                β†’ (x ＝ y) ≃ ((x , a) ＝ (y , b))
to-subtype-＝-≃ A-is-prop-valued {x} {y} {a} {b} =
 embedding-criterion-converse
  pr₁
  (pr₁-is-embedding A-is-prop-valued)
  (x , a)
  (y , b)

pr₁-lc-bis : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ }
           β†’ ({x : X} β†’ is-prop (Y x))
           β†’ left-cancellable pr₁
pr₁-lc-bis f {u} {v} r = embeddings-are-lc pr₁ (pr₁-is-embedding (Ξ» x β†’ f {x})) r

pr₁-is-embedding-converse : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ }
                          β†’ is-embedding (pr₁ {𝓀} {π“₯} {X} {Y})
                          β†’ (x : X) β†’ is-prop (Y x)
pr₁-is-embedding-converse {𝓀} {π“₯} {X} {Y} ie x = h
  where
    e : Ξ£ Y β†’ X
    e = pr₁ {𝓀} {π“₯} {X} {Y}

    i : is-prop (fiber e x)
    i = ie x

    s : Y x β†’ fiber e x
    s y = (x , y) , refl

    r : fiber e x β†’ Y x
    r ((x , y) , refl) = y

    rs : (y : Y x) β†’ r (s y) ＝ y
    rs y = refl

    h : is-prop (Y x)
    h = left-cancellable-reflects-is-prop s (section-lc s (r , rs)) i

embedding-closed-under-∼ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f g : X β†’ Y)
                         β†’ is-embedding f
                         β†’ g ∼ f
                         β†’ is-embedding g
embedding-closed-under-∼ f g e H y = equiv-to-prop (∼-fiber-≃ H y) (e y)

K-idtofun-lc : K-axiom (𝓀 ⁺)
             β†’ {X : 𝓀 Μ‡ } (x y : X) (A : X β†’ 𝓀 Μ‡ )
             β†’ left-cancellable (idtofun (Id x y) (A y))
K-idtofun-lc {𝓀} k {X} x y A {p} {q} r = k (𝓀 Μ‡ ) p q

lc-maps-into-sets-are-embeddings : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                                 β†’ left-cancellable f
                                 β†’ is-set Y
                                 β†’ is-embedding f
lc-maps-into-sets-are-embeddings
 {𝓀} {π“₯} {X} {Y} f f-lc iss y (x , p) (x' , p') = Ξ³
 where
   r : x ＝ x'
   r = f-lc (p βˆ™ (p' ⁻¹))

   q : yoneda-nat x (Ξ» x β†’ f x ＝ y) p x' r ＝ p'
   q = iss (yoneda-nat x (Ξ» x β†’ f x ＝ y) p x' r) p'

   γ : x , p ＝ x' , p'
   Ξ³ = to-Ξ£-Id (r , q)

sections-into-sets-are-embeddings : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                                  β†’ is-section f
                                  β†’ is-set Y
                                  β†’ is-embedding f
sections-into-sets-are-embeddings f f-is-section Y-is-set =
 lc-maps-into-sets-are-embeddings f (sections-are-lc f f-is-section) Y-is-set

lc-maps-are-embeddings-with-K : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                              β†’ left-cancellable f
                              β†’ K-axiom π“₯
                              β†’ is-embedding f
lc-maps-are-embeddings-with-K {𝓀} {π“₯} {X} {Y} f f-lc k =
 lc-maps-into-sets-are-embeddings f f-lc (k Y)

factor-is-lc : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
               (f : X β†’ Y)
               (g : Y β†’ Z)
             β†’ left-cancellable (g ∘ f)
             β†’ left-cancellable f
factor-is-lc f g gf-lc {x} {x'} p = gf-lc (ap g p)

factor-is-embedding : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
                      (f : X β†’ Y)
                      (g : Y β†’ Z)
                    β†’ is-embedding (g ∘ f)
                    β†’ is-embedding g
                    β†’ is-embedding f
factor-is-embedding {𝓀} {π“₯} {𝓦} {X} {Y} {Z} f g i j = Ξ³
 where
  a : (x x' : X) β†’ (x ＝ x') ≃ (g (f x) ＝ g (f x'))
  a x x' = ap (g ∘ f) {x} {x'} , embedding-gives-embedding' (g ∘ f) i x x'

  b : (y y' : Y) β†’ (y ＝ y') ≃ (g y ＝ g y')
  b y y' = ap g {y} {y'} , embedding-gives-embedding' g j y y'

  c : (x x' : X) β†’ (f x ＝ f x') ≃ (x ＝ x')
  c x x' = (f x ＝ f x')         β‰ƒβŸ¨ b (f x) (f x') ⟩
           (g (f x) ＝ g (f x')) β‰ƒβŸ¨ ≃-sym (a x x') ⟩
           (x ＝ x')             β– 

  Ξ³ : is-embedding f
  Ξ³ = embedding-criterion' f c

is-essential : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ (𝓦 : Universe) β†’ 𝓀 βŠ” π“₯ βŠ” (𝓦 ⁺) Μ‡
is-essential f 𝓦 = (Z : 𝓦 Μ‡) (g : codomain f β†’ Z)
                 β†’ is-embedding (g ∘ f)
                 β†’ is-embedding g

is-essential-embedding
 : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ (𝓦 : Universe) β†’ 𝓀 βŠ” π“₯ βŠ” (𝓦 ⁺) Μ‡
is-essential-embedding f 𝓦 = is-essential f 𝓦 Γ— is-embedding f

postcomp-is-embedding : FunExt
                      β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ } (f : X β†’ Y)
                      β†’ is-embedding f
                      β†’ is-embedding (Ξ» (Ο† : A β†’ X) β†’ f ∘ Ο†)
postcomp-is-embedding {𝓀} {π“₯} {𝓦} fe {X} {Y} {A} f i = Ξ³
 where
  g : (Ο† Ο†' : A β†’ X) (a : A) β†’ (Ο† a ＝ Ο†' a) ≃ (f (Ο† a) ＝ f (Ο†' a))
  g Ο† Ο†' a = ap f {Ο† a} {Ο†' a} , embedding-gives-embedding' f i (Ο† a) (Ο†' a)

  h : (Ο† Ο†' : A β†’ X) β†’ Ο† ∼ Ο†' ≃ f ∘ Ο† ∼ f ∘ Ο†'
  h Ο† Ο†' = Ξ -cong (fe 𝓦 𝓀) (fe 𝓦 π“₯) (g Ο† Ο†')

  k : (Ο† Ο†' : A β†’ X) β†’ (f ∘ Ο† ＝ f ∘ Ο†') ≃ (Ο† ＝ Ο†')
  k Ο† Ο†' = (f ∘ Ο† ＝ f ∘ Ο†') β‰ƒβŸ¨ ≃-funext (fe 𝓦 π“₯) (f ∘ Ο†) (f ∘ Ο†') ⟩
           (f ∘ Ο† ∼ f ∘ Ο†') β‰ƒβŸ¨ ≃-sym (h Ο† Ο†') ⟩
           (Ο† ∼ Ο†')         β‰ƒβŸ¨ ≃-sym (≃-funext (fe 𝓦 𝓀) Ο† Ο†') ⟩
           (Ο† ＝ Ο†')         β– 

  γ : is-embedding (f ∘_)
  γ = embedding-criterion' (f ∘_) k

disjoint-images : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ }
                β†’ (X β†’ A)
                β†’ (Y β†’ A)
                β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
disjoint-images f g = βˆ€ x y β†’ f x β‰  g y

disjoint-cases-embedding : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ }
                           (f : X β†’ A) (g : Y β†’ A)
                         β†’ is-embedding f
                         β†’ is-embedding g
                         β†’ disjoint-images f g
                         β†’ is-embedding (cases f g)
disjoint-cases-embedding {𝓀} {π“₯} {𝓦} {X} {Y} {A} f g ef eg d = Ξ³
  where
   Ξ³ : (a : A) (Οƒ Ο„ : Ξ£ z κž‰ X + Y , cases f g z ＝ a) β†’ Οƒ ＝ Ο„
   Ξ³ a (inl x , p) (inl x' , p') = r
     where
       q : x , p ＝ x' , p'
       q = ef a (x , p) (x' , p')

       h : fiber f a β†’ fiber (cases f g) a
       h (x , p) = inl x , p

       r : inl x , p ＝ inl x' , p'
       r = ap h q

   Ξ³ a (inl x , p) (inr y  , q) = 𝟘-elim (d x y (p βˆ™ q ⁻¹))

   Ξ³ a (inr y , q) (inl x  , p) = 𝟘-elim (d x y (p βˆ™ q ⁻¹))

   Ξ³ a (inr y , q) (inr y' , q') = r
     where
       p : y , q ＝ y' , q'
       p = eg a (y , q) (y' , q')

       h : fiber g a β†’ fiber (cases f g) a
       h (y , q) = inr y , q

       r : inr y , q ＝ inr y' , q'
       r = ap h p

\end{code}

TODO.
  (1) f : X β†’ Y is an embedding iff fiber f (f x) is a singleton for every x : X.
  (2) f : X β†’ Y is an embedding iff its corestriction to its image is an
      equivalence.

This can be deduced directly from Yoneda.

\begin{code}

inl-is-embedding : (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ )
                 β†’ is-embedding (inl {𝓀} {π“₯} {X} {Y})
inl-is-embedding {𝓀} {π“₯} X Y (inl a) (a , refl) (a , refl) = refl
inl-is-embedding {𝓀} {π“₯} X Y (inr b) (x , p) (x' , p') = 𝟘-elim (+disjoint p)

inr-is-embedding : (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ )
                 β†’ is-embedding (inr {𝓀} {π“₯} {X} {Y})
inr-is-embedding {𝓀} {π“₯} X Y (inl b) (x , p) (x' , p') = 𝟘-elim (+disjoint' p)
inr-is-embedding {𝓀} {π“₯} X Y (inr a) (a , refl) (a , refl) = refl

maps-of-props-into-sets-are-embeddings : {P : 𝓀 Μ‡ } {X : π“₯ Μ‡ } (f : P β†’ X)
                                       β†’ is-prop P
                                       β†’ is-set X
                                       β†’ is-embedding f
maps-of-props-into-sets-are-embeddings f i j q (p , s) (p' , s') =
 to-Σ-＝ (i p p' , j _ s')

maps-of-props-are-embeddings : {P : 𝓀 Μ‡ } {Q : π“₯ Μ‡ } (f : P β†’ Q)
                             β†’ is-prop P
                             β†’ is-prop Q
                             β†’ is-embedding f
maps-of-props-are-embeddings f i j =
 maps-of-props-into-sets-are-embeddings f i (props-are-sets j)

Γ—-is-embedding : {X : 𝓀 Μ‡ } {Y : π“₯Β Μ‡ } {A : 𝓦 Μ‡ } {B : 𝓣 Μ‡ }
                 (f : X β†’ A ) (g : Y β†’ B)
               β†’ is-embedding f
               β†’ is-embedding g
               β†’ is-embedding (Ξ» ((x , y) : X Γ— Y) β†’ (f x , g y))
Γ—-is-embedding f g i j (a , b) = retract-of-prop
                               (r , (s , rs))
                               (Γ—-is-prop (i a) (j b))
 where
  r : fiber f a Γ— fiber g b β†’ fiber (Ξ» (x , y) β†’ f x , g y) (a , b)
  r ((x , s) , (y , t)) = (x , y) , to-Γ—-＝ s t

  s : fiber (Ξ» (x , y) β†’ f x , g y) (a , b) β†’ fiber f a Γ— fiber g b
  s ((x , y) , p) = (x , ap pr₁ p) , (y , ap prβ‚‚ p)

  rs : (Ο† : fiber (Ξ» (x , y) β†’ f x , g y) (a , b)) β†’ r (s Ο†) ＝ Ο†
  rs ((x , y) , refl) = refl

NatΞ£-is-embedding : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ )
                    (ΞΆ : Nat A B)
                  β†’ ((x : X) β†’ is-embedding (ΞΆ x))
                  β†’ is-embedding (NatΞ£ ΞΆ)
NatΞ£-is-embedding A B ΞΆ i (x , b) = equiv-to-prop
                                     (≃-sym (NatΞ£-fiber-equiv A B ΞΆ x b))
                                     (i x b)

NatΞ£-embedding : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ }
               β†’ ((x : X) β†’ A x β†ͺ B x)
               β†’ Ξ£ A β†ͺ Ξ£ B
NatΞ£-embedding f = NatΞ£ (Ξ» x β†’ ⌊ f x βŒ‹) ,
                   NatΞ£-is-embedding _ _
                    (Ξ» x β†’ ⌊ f x βŒ‹)
                    (Ξ» x β†’ ⌊ f x βŒ‹-is-embedding)

NatΞ£-is-embedding-converse : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ )
                             (ΞΆ : Nat A B)
                           β†’ is-embedding (NatΞ£ ΞΆ)
                           β†’ ((x : X) β†’ is-embedding (ΞΆ x))
NatΞ£-is-embedding-converse A B ΞΆ e x b = equiv-to-prop
                                          (NatΞ£-fiber-equiv A B ΞΆ x b)
                                          (e (x , b))

NatΞ -is-embedding : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ )
                    (ΞΆ : Nat A B)
                  β†’ funext 𝓀 (π“₯ βŠ” 𝓦)
                  β†’ ((x : X) β†’ is-embedding (ΞΆ x))
                  β†’ is-embedding (NatΞ  ΞΆ)
NatΞ -is-embedding {𝓀} {π“₯} {𝓦} A B ΞΆ fe i g =
 equiv-to-prop
   (≃-sym (NatΞ -fiber-equiv A B ΞΆ (lower-funext 𝓀 π“₯ fe) g))
   (Ξ -is-prop fe (Ξ» x β†’ i x (g x)))

\end{code}

For any proposition P, the unique map P β†’ πŸ™ is an embedding:

\begin{code}

unique-to-πŸ™-is-embedding : (P : 𝓀 Μ‡ )
                         β†’ is-prop P
                         β†’ βˆ€ π“₯ β†’ is-embedding (unique-to-πŸ™ {𝓀} {π“₯})
unique-to-πŸ™-is-embedding P i π“₯ * (p , r) (p' , r') =
 to-Γ—-＝ (i p p') (props-are-sets πŸ™-is-prop r r')

embedding-into-πŸ™ : (P : 𝓀 Μ‡ )
                 β†’ is-prop P
                 β†’ P β†ͺ πŸ™ {π“₯}
embedding-into-πŸ™ {𝓀} {π“₯} P P-is-prop =
 unique-to-πŸ™ ,
 unique-to-πŸ™-is-embedding P P-is-prop π“₯

\end{code}

Added by Tom de Jong.

If a type X embeds into a proposition, then X is itself a proposition.

\begin{code}

subtypes-of-props-are-props'' : {X : 𝓀 Μ‡ } {P : π“₯ Μ‡ }
                              β†’ is-prop P
                              β†’ X β†ͺ P
                              β†’ is-prop X
subtypes-of-props-are-props'' P-is-prop (f , f-emb) =
 subtypes-of-props-are-props f f-emb P-is-prop

\end{code}

Added by Martin Escardo 12th July 2023.

Assuming univalence, the canonical map of X = Y into X β†’ Y is an
embedding.

\begin{code}

idtofun-is-embedding : is-univalent 𝓀
                     β†’ {X Y : 𝓀 Μ‡ } β†’ is-embedding (idtofun X Y)
idtofun-is-embedding ua {X} {Y} =
 ∘-is-embedding
  (equivs-are-embeddings (idtoeq X Y) (ua X Y))
  (pr₁-is-embedding (being-equiv-is-prop'' (univalence-gives-funext ua)))
 where
  remark : pr₁ ∘ idtoeq X Y ＝ idtofun X Y
  remark = refl

Idtofun-is-embedding : is-univalent 𝓀
                     β†’ funext (𝓀 ⁺) 𝓀
                     β†’ {X Y : 𝓀 Μ‡ } β†’ is-embedding (Idtofun {𝓀} {X} {Y})
Idtofun-is-embedding ua fe {X} {Y} =
 transport
  is-embedding
  (dfunext fe (idtofun-agreement X Y))
  (idtofun-is-embedding ua)

unique-from-𝟘-is-embedding : {X : 𝓀 Μ‡ }
                           β†’ is-embedding (unique-from-𝟘 {𝓀} {π“₯} {X})
unique-from-𝟘-is-embedding x (y , p) = 𝟘-elim y

\end{code}

Added by Martin Escardo and Tom de Jong 10th October 2023.

\begin{code}

id-is-essential : {X : 𝓀 Μ‡ } β†’ is-essential (id {𝓀} {X}) π“₯
id-is-essential {𝓀} {X} Z g = id

∘-is-essential : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
                 {f : X β†’ Y} {g : Y β†’ Z}
               β†’ is-essential f 𝓣
               β†’ is-essential g 𝓣
               β†’ is-essential (g ∘ f) 𝓣
∘-is-essential {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} {Z} {f} {g} f-ess g-ess W h ghf-emb = II
 where
  I : is-embedding (h ∘ g)
  I = f-ess W (h ∘ g) ghf-emb

  II : is-embedding h
  II = g-ess W h I

\end{code}

We originally hoped to prove that Idtofun was essential, but it's not:
while the composite

           Idtofun            evaluate at 0
  (𝟚 ≃ 𝟚) ---------β†’ (𝟚 β†’ 𝟚) ---------------> 𝟚

is an embedding, the evaluation map isn't.

Added by Ian Ray 22nd August 2024

\begin{code}

equiv-embeds-into-function : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                           β†’ FunExt
                           β†’ (X ≃ Y) β†ͺ (X β†’ Y)
equiv-embeds-into-function fe =
 (⌜_⌝ , pr₁-is-embedding (Ξ» f β†’ being-equiv-is-prop fe f))

\end{code}

End of addition.

Fixities:

\begin{code}

infix  0 _β†ͺ_
infix  1 _β–‘
infixr 0 _β†ͺ⟨_⟩_

\end{code}