Martin Escardo, 2015, formalized December 2017. My MGS'2019 have a better development of this. 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 --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} 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}