Martin Escardo

\begin{code}

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

module UF-Embeddings where

open import SpartanMLTT

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

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

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)

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')

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

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

Subtypes : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
Subtypes {𝓀} Y = Ξ£ X κž‰ 𝓀 Μ‡ , X β†ͺ 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 ⁻¹)))

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

embedding-embedding' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                     β†’ is-embedding f
                     β†’ is-embedding' f
embedding-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)))

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-embedding' f e x' x)

embedding'-embedding : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                     β†’ is-embedding' f
                     β†’ is-embedding f
embedding'-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'')

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}
    isp : is-prop (fiber e x)
    isp = 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)) isp

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') = to-Ξ£-Id (r , q)
 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'

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)

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 = subtype-of-prop-is-prop 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 = subtype-of-prop-is-prop
         (Ο† z)
         (sections-are-lc (Ο† z) (Ξ³ z , (Ξ³Ο† z)))
         (T-is-prop z)

\end{code}

TODO. Redo the above proof using the technique of the following proof.

\begin{code}

embedding-factor : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (f : X β†’ Y) (g : Y β†’ Z)
                 β†’ is-embedding (g ∘ f)
                 β†’ is-embedding g
                 β†’ is-embedding f
embedding-factor {𝓀} {π“₯} {𝓦} {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-embedding' (g ∘ f) i x x'

  b : (y y' : Y) β†’ (y ≑ y') ≃ (g y ≑ g y')
  b y y' = ap g {y} {y'} , embedding-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

embedding-exponential : FunExt
                      β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ } (f : X β†’ Y)
                      β†’ is-embedding f
                      β†’ is-embedding (Ξ» (Ο† : A β†’ X) β†’ f ∘ Ο†)
embedding-exponential {𝓀} {π“₯} {𝓦} 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-embedding' f i (Ο† a) (Ο†' a)

  h : (Ο† Ο†' : A β†’ X) β†’ Ο† ∼ Ο†' ≃ f ∘ Ο† ∼ f ∘ Ο†'
  h Ο† Ο†' = Ξ -cong (fe 𝓦 𝓀) (fe 𝓦 π“₯) A
            (Ξ» a β†’ Ο† a ≑ Ο†' a) (Ξ» a β†’ f (Ο† a) ≑ f (Ο†' a)) (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}

is-dense : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
is-dense f = is-empty (Ξ£ y κž‰ codomain f , Β¬ fiber f y)

id-is-dense : {X : 𝓀 Μ‡ } β†’ is-dense (id {𝓀} {X})
id-is-dense (y , n) = n (y , refl)

comp-dense : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
             {f : X β†’ Y} {g : Y β†’ Z}
           β†’ is-dense f
           β†’ is-dense g
           β†’ is-dense (g ∘ f)
comp-dense {𝓀} {π“₯} {𝓦} {X} {Y} {Z} {f} {g} e d = h
 where
  h : Β¬ (Ξ£ z κž‰ Z , Β¬ fiber (g ∘ f) z)
  h (z , n) = d (z , k)
   where
    k : Β¬ fiber g z
    k (y , refl) = e (y , l)
     where
      l : Β¬ fiber f y
      l (x , refl) = n (x , refl)

\end{code}

We should find a better home for the above definition, which says that
the complement of the image of f is empty. Perhaps a better
terminology would be ¬¬-dense.

\begin{code}

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

module _ {𝓀 π“₯} {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } where

 retraction-is-dense : (r : X β†’ Y) β†’ has-section r β†’ is-dense r
 retraction-is-dense r (s , rs) (y , n) = n (s y , rs y)

 is-equiv-is-dense : (f : X β†’ Y) β†’ is-equiv f β†’ is-dense f
 is-equiv-is-dense f e = retraction-is-dense f (equivs-have-sections f e)

 equiv-dense-embedding : X ≃ Y β†’ X β†ͺᡈ Y
 equiv-dense-embedding e = ⌜ e ⌝ ,
                           equivs-are-embeddings ⌜ e ⌝ (⌜⌝-is-equiv e),
                           is-equiv-is-dense     ⌜ e ⌝ (⌜⌝-is-equiv e)

 detofun : (X β†ͺᡈ Y) β†’ X β†’ Y
 detofun = pr₁

 is-embedding-detofun : (e : X β†ͺᡈ Y) β†’ is-embedding (detofun e)
 is-embedding-detofun e = pr₁ (prβ‚‚ e)

 is-dense-detofun : (e : X β†ͺᡈ Y) β†’ is-dense (detofun e)
 is-dense-detofun e = prβ‚‚ (prβ‚‚ e)


module _ {𝓀 π“₯ 𝓦 𝓣}
         {X : 𝓀 Μ‡ }
         {A : X β†’ π“₯ Μ‡ }
         {Y : 𝓦 Μ‡ }
         {B : Y β†’ 𝓣 Μ‡ }
         (f : X β†’ Y)
         (g : (x : X) β†’ A x β†’ B (f x))
       where

 pair-fun : Ξ£ A β†’ Ξ£ B
 pair-fun (x , a) = (f x , g x a)

 pair-fun-is-embedding : is-embedding f
                    β†’ ((x : X) β†’ is-embedding (g x))
                    β†’ is-embedding pair-fun
 pair-fun-is-embedding e d (y , b) = h
  where
   Z : 𝓀 βŠ” π“₯ βŠ” 𝓦 βŠ” 𝓣 Μ‡
   Z = Ξ£ w κž‰ fiber f y , fiber (g (pr₁ w)) (back-transport B (prβ‚‚ w) b)

   Z-is-prop : is-prop Z
   Z-is-prop = subtype-of-prop-is-prop
                pr₁
                (pr₁-lc (Ξ» {w} β†’ d (pr₁ w) (back-transport B (prβ‚‚ w) b)))
                (e y)

   Ο† : fiber pair-fun (y , b) β†’ Z
   Ο† ((x , a) , refl) = (x , refl) , (a , refl)

   Ξ³ : Z β†’ fiber pair-fun (y , b)
   Ξ³ ((x , refl) , (a , refl)) = (x , a) , refl

   Ξ³Ο† : (t : fiber pair-fun (y , b)) β†’ Ξ³ (Ο† t) ≑ t
   Ξ³Ο† ((x , a) , refl) = refl

   h : is-prop (fiber pair-fun (y , b))
   h = subtype-of-prop-is-prop Ο† (sections-are-lc Ο† (Ξ³ , Ξ³Ο†)) Z-is-prop

 pair-fun-dense : is-dense f
               β†’ ((x : X) β†’ is-dense (g x))
               β†’ is-dense pair-fun
 pair-fun-dense i j = contrapositive Ξ³ i
  where
   Ξ³ : (Ξ£ w κž‰ Ξ£ B , Β¬ fiber pair-fun w) β†’ Ξ£ y κž‰ Y , Β¬ fiber f y
   Ξ³ ((y , b) , n) = y , m
    where
     m : Β¬ fiber f y
     m (x , refl) = j x (b , l)
      where
       l : Β¬ fiber (g x) b
       l (a , refl) = n ((x , a) , refl)

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)

Γ—-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))
Γ—-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Ξ£-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}

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

Added by Tom de Jong.

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

\begin{code}

embedding-into-prop : {X : 𝓀 Μ‡ } {P : π“₯ Μ‡ } β†’ is-prop P β†’ X β†ͺ P β†’ is-prop X
embedding-into-prop i (f , e) x y = d
 where
   a : x ≑ y β†’ f x ≑ f y
   a = ap f {x} {y}

   b : is-equiv a
   b = embedding-embedding' f e x y

   c : f x ≑ f y
   c = i (f x) (f y)

   d : x ≑ y
   d = inverse a b c

\end{code}

\begin{code}

infix  0 _β†ͺ_

\end{code}