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

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

module UF.IdEmbedding where

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

\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}

\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}