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

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}