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

module UF-IdEmbedding where

open import SpartanMLTT
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}