Martin Escardo, 2015, formalized December 2017.

Id : X β†’ (X β†’ U) is an embedding assuming functional extensionality,
and either univalence or K, in fact the Yoneda Embedding.

The Id-fiber of A:X→𝓀 Μ‡ says that A is representable, which is
equivalent to the contractibility of Ξ£A, which is a
proposition. (Hence the injective types are the retracts of the
exponential powers of the universe.)

This works as follows in outline:

If A : X β†’ 𝓀 Μ‡ then the Id-fiber of A is Ξ£ x κž‰ X , Id x ＝ A.

If the pair (x,p) is in the fiber for x : X and p : Id x = A, then

   ap Ξ£ p : Ξ£ (Id x) = Ξ£ A,

and hence, being equal to a contractible type, the type Ξ£ A is
contractible.

Next we have (*)

 A x ≃ Nat (Id x) A             (yoneda)
     = (y : X) β†’ Id x y β†’ A y   (definition)
     ≃ (y : X) β†’ Id x y ≃ A y   (because Ξ£ A is contractible (Yoneda corollary))
     ≃ (y : X) β†’ Id x y ＝ A y   (by univalence)
     ≃ Id x ＝ A                 (by function extensionality)

Applying Ξ£ to both sides, Ξ£ A ≃ (Ξ£ x κž‰ X , Id x ＝ A), and because
the type Ξ£ A is contractible so is Ξ£ x κž‰ X , Id x ＝ A, which shows
that the map Id : X β†’ (X β†’ U) is an embedding.

2017:

This relies on univalence. But less than that suffices
(https://groups.google.com/forum/#!topic/homotopytypetheory/bKti7krHM-c)

First, Evan Cavallo showed that it is enough to assume funext and that
the canonical map X ＝ Y β†’ X ≃ Y is an embedding. Then, using this idea
and the above proof outline, we further generalized this to assume
that the canonical map X ＝ Y β†’ (X β†’ Y) is left-cancellable (which is
much weaker than assuming that it is an embedding).

This is what we record next (9th December 2017), using the original
idea (*) in the weakened form discussed above.

\begin{code}

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

module UF.IdEmbedding where

open import MLTT.Spartan
open import UF.Base
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.FunExt
open import UF.Lower-FunExt
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.Embeddings
open import UF.Yoneda
open import UF.LeftCancellable
open import UF.Univalence
open import UF.EquivalenceExamples

\end{code}

The Id Embedding Lemma. The idea is to show that the type
T := Ξ£ x κž‰ X , Id x ＝ A is a proposition by showing that there is a
left-cancellable map from it to a proposition, namely the contractible
type Ξ£ A.

\begin{code}

Id-Embedding-Lemma : FunExt
                   β†’ {X : 𝓀 Μ‡ }
                   β†’ ((x y : X) (A : X β†’ 𝓀 Μ‡ )
                   β†’ left-cancellable (idtofun (Id x y) (A y)))
                   β†’ is-embedding(Id {𝓀} {X})
Id-Embedding-Lemma {𝓀} fe {X} iflc A (xβ‚€ , pβ‚€) = h (xβ‚€ , pβ‚€)
 where
  T = Ξ£ x κž‰ X , Id x ＝ A
  q : Ξ£ (Id xβ‚€) ＝ Ξ£ A
  q = ap Ξ£ pβ‚€
  c : βˆƒ! A
  c = yoneda-nat (singleton-type xβ‚€) is-singleton (singleton-types-are-singletons xβ‚€) (Ξ£ A) q
  fβ‚€ : (x : X) β†’ Id x ＝ A β†’ (y : X) β†’ Id x y ＝ A y
  fβ‚€ x = happly
  f₁ : (x : X) β†’ ((y : X) β†’ Id x y ＝ A y) β†’ Nat (Id x) A
  f₁ x = NatΞ  (Ξ» y β†’ idtofun (Id x y) (A y))
  fβ‚‚ : (x : X) β†’ Nat (Id x) A β†’ A x
  fβ‚‚ x = yoneda-elem x A
  f : (x : X) β†’ Id x ＝ A β†’ A x
  f x = fβ‚‚ x ∘ f₁ x ∘ fβ‚€ x
  fβ‚€-lc : (x : X) β†’ left-cancellable(fβ‚€ x)
  fβ‚€-lc x = happly-lc (fe 𝓀 (𝓀 ⁺)) (Id x) A
  f₁-lc : (x : X) β†’ left-cancellable(f₁ x)
  f₁-lc x = g
    where
      l : βˆ€ {Ο† Ο†'} β†’ f₁ x Ο† ＝ f₁ x Ο†' β†’ (x : X) β†’ Ο† x ＝ Ο†' x
      l {Ο†} {Ο†'} = NatΞ -lc (Ξ» y β†’ idtofun (Id x y) (A y)) (Ξ» y β†’ iflc x y A)
      g : βˆ€ {Ο† Ο†'} β†’ f₁ x Ο† ＝ f₁ x Ο†' β†’ Ο† ＝ Ο†'
      g p = dfunext (fe 𝓀 (𝓀 ⁺)) (l p)
  fβ‚‚-lc : (x : X) β†’ left-cancellable(fβ‚‚ x)
  fβ‚‚-lc x {Ξ·} {Ξ·'} p = dfunext (fe 𝓀 𝓀) (Ξ» y β†’ dfunext (fe 𝓀 𝓀) (l y))
    where
      l : Ξ· β‰ˆ Ξ·'
      l = yoneda-elem-lc Ξ· Ξ·' p
  f-lc : (x : X) β†’ left-cancellable(f x)
  f-lc x = left-cancellable-closed-under-∘
               (fβ‚€ x)
               (fβ‚‚ x ∘ f₁ x)
               (fβ‚€-lc x)
               (left-cancellable-closed-under-∘ (f₁ x) (fβ‚‚ x) (f₁-lc x) (fβ‚‚-lc x))
  g : T β†’ Ξ£ A
  g = NatΞ£ f
  g-lc : left-cancellable g
  g-lc = NatΞ£-lc f f-lc
  h : is-prop T
  h = left-cancellable-reflects-is-prop g g-lc (singletons-are-props c)

\end{code}

univalence implies that the function Id {𝓀} {X} : X β†’ (X β†’ 𝓀 Μ‡ ) is an embedding.

The map eqtofun is left-cancellable assuming univalence (and function
extensionality, which is a consequence of univalence, but we don't
bother):

\begin{code}

eqtofun-lc : is-univalent 𝓀
           β†’ FunExt
           β†’ (X Y : 𝓀 Μ‡ ) β†’ left-cancellable(Eqtofun X Y)
eqtofun-lc ua fe X Y {f , jef} {g , jeg} p = Ξ³
 where
  q : yoneda-nat f is-equiv jef g p ＝ jeg
  q = being-equiv-is-prop fe g _ _
  γ : f , jef ＝ g , jeg
  Ξ³ = to-Ξ£-Id (p , q)

\end{code}

The map idtofun is left-cancellable assuming univalence (and funext):

\begin{code}

is-univalent-idtofun-lc : is-univalent 𝓀
                        β†’ FunExt
                        β†’ (X Y : 𝓀 Μ‡ ) β†’ left-cancellable(idtofun X Y)
is-univalent-idtofun-lc  ua fe X Y = left-cancellable-closed-under-∘
                                        (idtoeq X Y)
                                        (Eqtofun X Y)
                                        (is-univalent-idtoeq-lc ua X Y) (eqtofun-lc ua fe X Y)

UA-Id-embedding : is-univalent 𝓀
                β†’ FunExt
                β†’ {X : 𝓀 Μ‡ } β†’ is-embedding(Id {𝓀} {X})
UA-Id-embedding {𝓀} ua fe {X} = Id-Embedding-Lemma fe
                                            (Ξ» x y a β†’ is-univalent-idtofun-lc ua fe (Id x y) (a y))

\end{code}

The K axiom and function extensionality together imply that the
function Id : X β†’ (X β†’ U) is an embedding.

\begin{code}

K-Id-embedding' : K-axiom (𝓀 ⁺)
                β†’ FunExt
                β†’ {X : 𝓀 Μ‡ } β†’ is-embedding(Id {𝓀} {X})
K-Id-embedding' {𝓀} k fe {X} = Id-Embedding-Lemma fe (K-idtofun-lc k)

\end{code}

But actually function extensionality is not needed for this: K alone suffices.

\begin{code}

Id-lc : {X : 𝓀 Μ‡ } β†’ left-cancellable (Id {𝓀} {X})
Id-lc {𝓀} {X} {x} {y} p = idtofun (Id y y) (Id x y) (happly (p ⁻¹) y) refl

K-Id-embedding : K-axiom (𝓀 ⁺) β†’ {X : 𝓀 Μ‡ } β†’ is-embedding(Id {𝓀} {X})
K-Id-embedding {𝓀} k {X} = lc-maps-are-embeddings-with-K Id Id-lc k

\end{code}

Added 7th Feb 2019.

\begin{code}

Id-set : {X : 𝓀 Μ‡ } β†’ is-set X β†’ X β†’ (X β†’ Ξ© 𝓀)
Id-set i x y = (x ＝ y) , i

Id-set-lc : funext  𝓀 (𝓀 ⁺)
          β†’ {X : 𝓀 Μ‡ } (i : is-set X)
          β†’ left-cancellable (Id-set i)
Id-set-lc fe {X} i {x} {y} e = Id-lc d
 where
  d : Id x ＝ Id y
  d = dfunext fe (Ξ» z β†’ ap pr₁ (happly e z))

Id-set-is-embedding : funext  𝓀 (𝓀 ⁺)
                    β†’ propext 𝓀
                    β†’ {X : 𝓀 Μ‡ } (i : is-set X) β†’ is-embedding (Id-set i)
Id-set-is-embedding {𝓀} fe pe {X} i = lc-maps-into-sets-are-embeddings
                                        (Id-set i)
                                        (Id-set-lc (lower-funext 𝓀 (𝓀 ⁺) fe) i)
                                        (Ξ -is-set fe (Ξ» x β†’ Ξ©-is-set (lower-funext 𝓀 (𝓀 ⁺) fe) pe))
\end{code}