Embeddings
Martin Escardo{-# OPTIONS --safe --without-K #-} module UF.Embeddings where open import MLTT.Spartan open import MLTT.Plus-Properties open import UF.Base open import UF.Equiv open import UF.Equiv-FunExt open import UF.EquivalenceExamples open import UF.FunExt open import UF.LeftCancellable open import UF.Lower-FunExt open import UF.Retracts open import UF.Sets open import UF.Sets-Properties open import UF.Subsingletons open import UF.Subsingletons-FunExt open import UF.Subsingletons-Properties open import UF.UA-FunExt open import UF.Univalence open import UF.Yoneda open import UF.SubtypeClassifier is-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇ is-embedding f = each-fiber-of f is-prop being-embedding-is-prop : funext (𝓤 ⊔ 𝓥) (𝓤 ⊔ 𝓥) → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-prop (is-embedding f) being-embedding-is-prop {𝓤} {𝓥} fe f = Π-is-prop (lower-funext 𝓤 𝓤 fe) (λ x → being-prop-is-prop fe) id-is-embedding : {X : 𝓤 ̇ } → is-embedding (id {𝓤} {X}) id-is-embedding = singleton-types'-are-props ∘-is-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } {f : X → Y} {g : Y → Z} → is-embedding f → is-embedding g → is-embedding (g ∘ f) ∘-is-embedding {𝓤} {𝓥} {𝓦} {X} {Y} {Z} {f} {g} e d = h where T : (z : Z) → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ̇ T z = Σ (y , _) ꞉ fiber g z , fiber f y T-is-prop : (z : Z) → is-prop (T z) T-is-prop z = subtypes-of-props-are-props' pr₁ (pr₁-lc (λ {t} → e (pr₁ t))) (d z) φ : (z : Z) → fiber (g ∘ f) z → T z φ z (x , p) = (f x , p) , x , refl γ : (z : Z) → T z → fiber (g ∘ f) z γ z ((.(f x) , p) , x , refl) = x , p γφ : (z : Z) (t : fiber (g ∘ f) z) → γ z (φ z t) ＝ t γφ .(g (f x)) (x , refl) = refl h : (z : Z) → is-prop (fiber (g ∘ f) z) h z = subtypes-of-props-are-props' (φ z) (sections-are-lc (φ z) (γ z , (γφ z))) (T-is-prop z) _↪_ : 𝓤 ̇ → 𝓥 ̇ → 𝓤 ⊔ 𝓥 ̇ X ↪ Y = Σ f ꞉ (X → Y) , is-embedding f ↪-refl : (X : 𝓤 ̇ ) → X ↪ X ↪-refl X = id , id-is-embedding _∘↪_ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } → Y ↪ Z → X ↪ Y → X ↪ Z (g , j) ∘↪ (f , i) = g ∘ f , ∘-is-embedding i j ⌊_⌋ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → X ↪ Y → X → Y ⌊ f , _ ⌋ = f ⌊_⌋-is-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (e : X ↪ Y) → is-embedding ⌊ e ⌋ ⌊ _ , i ⌋-is-embedding = i _↪⟨_⟩_ : (X : 𝓤 ̇ ) {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } → X ↪ Y → Y ↪ Z → X ↪ Z _ ↪⟨ f , i ⟩ (g , j) = (g ∘ f) , (∘-is-embedding i j) _□ : (X : 𝓤 ̇ ) → X ↪ X _□ X = id , id-is-embedding embedding-criterion : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → ((x : X) → is-prop (fiber f (f x))) → is-embedding f embedding-criterion f φ .(f x) (x , refl) = φ x (x , refl) embedding-criterion' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → ((x x' : X) → (f x ＝ f x') ≃ (x ＝ x')) → is-embedding f embedding-criterion' {𝓤} {𝓥} {X} {Y} f e = embedding-criterion f (λ x' → equiv-to-prop (a x') (singleton-types'-are-props x')) where a : (x' : X) → fiber f (f x') ≃ (Σ x ꞉ X , x ＝ x') a x' = Σ-cong (λ x → e x x') vv-equivs-are-embeddings : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-vv-equiv f → is-embedding f vv-equivs-are-embeddings f e y = singletons-are-props (e y) equivs-are-embeddings : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-equiv f → is-embedding f equivs-are-embeddings f e = vv-equivs-are-embeddings f (equivs-are-vv-equivs f e) equivs-are-embeddings' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (𝕗 : X ≃ Y) → is-embedding ⌜ 𝕗 ⌝ equivs-are-embeddings' (f , e) = equivs-are-embeddings f e ≃-gives-↪ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → X ≃ Y → X ↪ Y ≃-gives-↪ (f , i) = (f , equivs-are-embeddings f i) embeddings-with-sections-are-vv-equivs : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-embedding f → has-section f → is-vv-equiv f embeddings-with-sections-are-vv-equivs f i (g , η) y = pointed-props-are-singletons (g y , η y) (i y) embeddings-with-sections-are-equivs : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-embedding f → has-section f → is-equiv f embeddings-with-sections-are-equivs f i h = vv-equivs-are-equivs f (embeddings-with-sections-are-vv-equivs f i h) Subtype' : (𝓤 {𝓥} : Universe) → 𝓥 ̇ → 𝓤 ⁺ ⊔ 𝓥 ̇ Subtype' 𝓤 {𝓥} Y = Σ X ꞉ 𝓤 ̇ , X ↪ Y Subtype : 𝓤 ̇ → 𝓤 ⁺ ̇ Subtype {𝓤} Y = Subtype' 𝓤 Y etofun : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X ↪ Y) → (X → Y) etofun = pr₁ is-embedding-etofun : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (e : X ↪ Y) → is-embedding (etofun e) is-embedding-etofun = pr₂ equivs-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → X ≃ Y → X ↪ Y equivs-embedding e = ⌜ e ⌝ , equivs-are-embeddings ⌜ e ⌝ (⌜⌝-is-equiv e) embeddings-are-lc : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-embedding f → left-cancellable f embeddings-are-lc f e {x} {x'} p = ap pr₁ (e (f x) (x , refl) (x' , (p ⁻¹))) subtypes-of-props-are-props : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (e : X → Y) → is-embedding e → is-prop Y → is-prop X subtypes-of-props-are-props e i = subtypes-of-props-are-props' e (embeddings-are-lc e i) subtypes-of-sets-are-sets : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (e : X → Y) → is-embedding e → is-set Y → is-set X subtypes-of-sets-are-sets e i = subtypes-of-sets-are-sets' e (embeddings-are-lc e i) is-embedding' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇ is-embedding' f = ∀ x x' → is-equiv (ap f {x} {x'}) embedding-gives-embedding' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-embedding f → is-embedding' f embedding-gives-embedding' {𝓤} {𝓥} {X} {Y} f ise = g where b : (x : X) → is-singleton (fiber f (f x)) b x = (x , refl) , ise (f x) (x , refl) c : (x : X) → is-singleton (fiber' f (f x)) c x = retract-of-singleton (≃-gives-▷ (fiber-lemma f (f x))) (b x) g : (x x' : X) → is-equiv (ap f {x} {x'}) g x = universality-equiv x refl (central-point-is-universal (λ x' → f x ＝ f x') (center (c x)) (centrality (c x)))Added 27 June 2024. It follows that if f is an equivalence, then so is ap f. It is added here, rather than in UF.EquivalenceExamples, to avoid cyclic module dependencies.ap-is-equiv : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-equiv f → {x x' : X} → is-equiv (ap f {x} {x'}) ap-is-equiv f e {x} {x'} = embedding-gives-embedding' f (equivs-are-embeddings f e) x x' embedding-criterion-converse' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-embedding f → (x' x : X) → (x' ＝ x) ≃ (f x' ＝ f x) embedding-criterion-converse' f e x' x = ap f {x'} {x} , embedding-gives-embedding' f e x' x embedding-criterion-converse : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-embedding f → (x' x : X) → (f x' ＝ f x) ≃ (x' ＝ x) embedding-criterion-converse f e x' x = ≃-sym (embedding-criterion-converse' f e x' x) embedding'-gives-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-embedding' f → is-embedding f embedding'-gives-embedding {𝓤} {𝓥} {X} {Y} f ise = g where e : (x : X) → is-central (Σ x' ꞉ X , f x ＝ f x') (x , refl) e x = universal-element-is-central (x , refl) (equiv-universality x refl (ise x)) h : (x : X) → is-prop (fiber' f (f x)) h x σ τ = σ ＝⟨ (e x σ)⁻¹ ⟩ (x , refl) ＝⟨ e x τ ⟩ τ ∎ g' : (y : Y) → is-prop (fiber' f y) g' y (x , p) = transport (λ - → is-prop (Σ x' ꞉ X , - ＝ f x')) (p ⁻¹) (h x) (x , p) g : (y : Y) → is-prop (fiber f y) g y = left-cancellable-reflects-is-prop ⌜ fiber-lemma f y ⌝ (section-lc _ (equivs-are-sections _ (⌜⌝-is-equiv (fiber-lemma f y)))) (g' y) pr₁-is-embedding : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } → ((x : X) → is-prop (Y x)) → is-embedding (pr₁ {𝓤} {𝓥} {X} {Y}) pr₁-is-embedding f x ((x , y') , refl) ((x , y'') , refl) = g where g : (x , y') , refl ＝ (x , y'') , refl g = ap (λ - → (x , -) , refl) (f x y' y'') 𝕡𝕣₁ : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } → ((x : X) → is-prop (Y x)) → (Σ Y ↪ X) 𝕡𝕣₁ i = pr₁ , pr₁-is-embedding i to-subtype-＝-≃ : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } → ((x : X) → is-prop (A x)) → {x y : X} {a : A x} {b : A y} → (x ＝ y) ≃ ((x , a) ＝ (y , b)) to-subtype-＝-≃ A-is-prop-valued {x} {y} {a} {b} = embedding-criterion-converse pr₁ (pr₁-is-embedding A-is-prop-valued) (x , a) (y , b) pr₁-lc-bis : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } → ({x : X} → is-prop (Y x)) → left-cancellable pr₁ pr₁-lc-bis f {u} {v} r = embeddings-are-lc pr₁ (pr₁-is-embedding (λ x → f {x})) r pr₁-is-embedding-converse : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } → is-embedding (pr₁ {𝓤} {𝓥} {X} {Y}) → (x : X) → is-prop (Y x) pr₁-is-embedding-converse {𝓤} {𝓥} {X} {Y} ie x = h where e : Σ Y → X e = pr₁ {𝓤} {𝓥} {X} {Y} i : is-prop (fiber e x) i = ie x s : Y x → fiber e x s y = (x , y) , refl r : fiber e x → Y x r ((x , y) , refl) = y rs : (y : Y x) → r (s y) ＝ y rs y = refl h : is-prop (Y x) h = left-cancellable-reflects-is-prop s (section-lc s (r , rs)) i embedding-closed-under-∼ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f g : X → Y) → is-embedding f → g ∼ f → is-embedding g embedding-closed-under-∼ f g e H y = equiv-to-prop (∼-fiber-≃ H y) (e y) K-idtofun-lc : K-axiom (𝓤 ⁺) → {X : 𝓤 ̇ } (x y : X) (A : X → 𝓤 ̇ ) → left-cancellable (idtofun (Id x y) (A y)) K-idtofun-lc {𝓤} k {X} x y A {p} {q} r = k (𝓤 ̇ ) p q lc-maps-into-sets-are-embeddings : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → left-cancellable f → is-set Y → is-embedding f lc-maps-into-sets-are-embeddings {𝓤} {𝓥} {X} {Y} f f-lc iss y (x , p) (x' , p') = γ where r : x ＝ x' r = f-lc (p ∙ (p' ⁻¹)) q : yoneda-nat x (λ x → f x ＝ y) p x' r ＝ p' q = iss (yoneda-nat x (λ x → f x ＝ y) p x' r) p' γ : x , p ＝ x' , p' γ = to-Σ-Id (r , q) sections-into-sets-are-embeddings : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-section f → is-set Y → is-embedding f sections-into-sets-are-embeddings f f-is-section Y-is-set = lc-maps-into-sets-are-embeddings f (sections-are-lc f f-is-section) Y-is-set lc-maps-are-embeddings-with-K : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → left-cancellable f → K-axiom 𝓥 → is-embedding f lc-maps-are-embeddings-with-K {𝓤} {𝓥} {X} {Y} f f-lc k = lc-maps-into-sets-are-embeddings f f-lc (k Y) factor-is-lc : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } (f : X → Y) (g : Y → Z) → left-cancellable (g ∘ f) → left-cancellable f factor-is-lc f g gf-lc {x} {x'} p = gf-lc (ap g p) factor-is-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } (f : X → Y) (g : Y → Z) → is-embedding (g ∘ f) → is-embedding g → is-embedding f factor-is-embedding {𝓤} {𝓥} {𝓦} {X} {Y} {Z} f g i j = γ where a : (x x' : X) → (x ＝ x') ≃ (g (f x) ＝ g (f x')) a x x' = ap (g ∘ f) {x} {x'} , embedding-gives-embedding' (g ∘ f) i x x' b : (y y' : Y) → (y ＝ y') ≃ (g y ＝ g y') b y y' = ap g {y} {y'} , embedding-gives-embedding' g j y y' c : (x x' : X) → (f x ＝ f x') ≃ (x ＝ x') c x x' = (f x ＝ f x') ≃⟨ b (f x) (f x') ⟩ (g (f x) ＝ g (f x')) ≃⟨ ≃-sym (a x x') ⟩ (x ＝ x') ■ γ : is-embedding f γ = embedding-criterion' f c is-essential : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → (𝓦 : Universe) → 𝓤 ⊔ 𝓥 ⊔ (𝓦 ⁺) ̇ is-essential f 𝓦 = (Z : 𝓦 ̇ ) (g : codomain f → Z) → is-embedding (g ∘ f) → is-embedding g is-essential-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → (𝓦 : Universe) → 𝓤 ⊔ 𝓥 ⊔ (𝓦 ⁺) ̇ is-essential-embedding f 𝓦 = is-essential f 𝓦 × is-embedding f postcomp-is-embedding : FunExt → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ } (f : X → Y) → is-embedding f → is-embedding (λ (φ : A → X) → f ∘ φ) postcomp-is-embedding {𝓤} {𝓥} {𝓦} fe {X} {Y} {A} f i = γ where g : (φ φ' : A → X) (a : A) → (φ a ＝ φ' a) ≃ (f (φ a) ＝ f (φ' a)) g φ φ' a = ap f {φ a} {φ' a} , embedding-gives-embedding' f i (φ a) (φ' a) h : (φ φ' : A → X) → φ ∼ φ' ≃ f ∘ φ ∼ f ∘ φ' h φ φ' = Π-cong (fe 𝓦 𝓤) (fe 𝓦 𝓥) (g φ φ') k : (φ φ' : A → X) → (f ∘ φ ＝ f ∘ φ') ≃ (φ ＝ φ') k φ φ' = (f ∘ φ ＝ f ∘ φ') ≃⟨ ≃-funext (fe 𝓦 𝓥) (f ∘ φ) (f ∘ φ') ⟩ (f ∘ φ ∼ f ∘ φ') ≃⟨ ≃-sym (h φ φ') ⟩ (φ ∼ φ') ≃⟨ ≃-sym (≃-funext (fe 𝓦 𝓤) φ φ') ⟩ (φ ＝ φ') ■ γ : is-embedding (f ∘_) γ = embedding-criterion' (f ∘_) k disjoint-images : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ } → (X → A) → (Y → A) → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ̇ disjoint-images f g = ∀ x y → f x ≠ g y disjoint-cases-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ } (f : X → A) (g : Y → A) → is-embedding f → is-embedding g → disjoint-images f g → is-embedding (cases f g) disjoint-cases-embedding {𝓤} {𝓥} {𝓦} {X} {Y} {A} f g ef eg d = γ where γ : (a : A) (σ τ : Σ z ꞉ X + Y , cases f g z ＝ a) → σ ＝ τ γ a (inl x , p) (inl x' , p') = r where q : x , p ＝ x' , p' q = ef a (x , p) (x' , p') h : fiber f a → fiber (cases f g) a h (x , p) = inl x , p r : inl x , p ＝ inl x' , p' r = ap h q γ a (inl x , p) (inr y , q) = 𝟘-elim (d x y (p ∙ q ⁻¹)) γ a (inr y , q) (inl x , p) = 𝟘-elim (d x y (p ∙ q ⁻¹)) γ a (inr y , q) (inr y' , q') = r where p : y , q ＝ y' , q' p = eg a (y , q) (y' , q') h : fiber g a → fiber (cases f g) a h (y , q) = inr y , q r : inr y , q ＝ inr y' , q' r = ap h pTODO. (1) f : X → Y is an embedding iff fiber f (f x) is a singleton for every x : X. (2) f : X → Y is an embedding iff its corestriction to its image is an equivalence. This can be deduced directly from Yoneda.inl-is-embedding : (X : 𝓤 ̇ ) (Y : 𝓥 ̇ ) → is-embedding (inl {𝓤} {𝓥} {X} {Y}) inl-is-embedding {𝓤} {𝓥} X Y (inl a) (a , refl) (a , refl) = refl inl-is-embedding {𝓤} {𝓥} X Y (inr b) (x , p) (x' , p') = 𝟘-elim (+disjoint p) inr-is-embedding : (X : 𝓤 ̇ ) (Y : 𝓥 ̇ ) → is-embedding (inr {𝓤} {𝓥} {X} {Y}) inr-is-embedding {𝓤} {𝓥} X Y (inl b) (x , p) (x' , p') = 𝟘-elim (+disjoint' p) inr-is-embedding {𝓤} {𝓥} X Y (inr a) (a , refl) (a , refl) = refl maps-of-props-into-sets-are-embeddings : {P : 𝓤 ̇ } {X : 𝓥 ̇ } (f : P → X) → is-prop P → is-set X → is-embedding f maps-of-props-into-sets-are-embeddings f i j q (p , s) (p' , s') = to-Σ-＝ (i p p' , j _ s') maps-of-props-are-embeddings : {P : 𝓤 ̇ } {Q : 𝓥 ̇ } (f : P → Q) → is-prop P → is-prop Q → is-embedding f maps-of-props-are-embeddings f i j = maps-of-props-into-sets-are-embeddings f i (props-are-sets j) ×-is-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ } {B : 𝓣 ̇ } (f : X → A) (g : Y → B) → is-embedding f → is-embedding g → is-embedding (λ ((x , y) : X × Y) → (f x , g y)) ×-is-embedding f g i j (a , b) = retract-of-prop (r , (s , rs)) (×-is-prop (i a) (j b)) where r : fiber f a × fiber g b → fiber (λ (x , y) → f x , g y) (a , b) r ((x , s) , (y , t)) = (x , y) , to-×-＝ s t s : fiber (λ (x , y) → f x , g y) (a , b) → fiber f a × fiber g b s ((x , y) , p) = (x , ap pr₁ p) , (y , ap pr₂ p) rs : (φ : fiber (λ (x , y) → f x , g y) (a , b)) → r (s φ) ＝ φ rs ((x , y) , refl) = refl NatΣ-is-embedding : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (ζ : Nat A B) → ((x : X) → is-embedding (ζ x)) → is-embedding (NatΣ ζ) NatΣ-is-embedding A B ζ i (x , b) = equiv-to-prop (≃-sym (NatΣ-fiber-equiv A B ζ x b)) (i x b) NatΣ-embedding : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } {B : X → 𝓦 ̇ } → ((x : X) → A x ↪ B x) → Σ A ↪ Σ B NatΣ-embedding f = NatΣ (λ x → ⌊ f x ⌋) , NatΣ-is-embedding _ _ (λ x → ⌊ f x ⌋) (λ x → ⌊ f x ⌋-is-embedding) NatΣ-is-embedding-converse : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (ζ : Nat A B) → is-embedding (NatΣ ζ) → ((x : X) → is-embedding (ζ x)) NatΣ-is-embedding-converse A B ζ e x b = equiv-to-prop (NatΣ-fiber-equiv A B ζ x b) (e (x , b)) NatΠ-is-embedding : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (ζ : Nat A B) → funext 𝓤 (𝓥 ⊔ 𝓦) → ((x : X) → is-embedding (ζ x)) → is-embedding (NatΠ ζ) NatΠ-is-embedding {𝓤} {𝓥} {𝓦} A B ζ fe i g = equiv-to-prop (≃-sym (NatΠ-fiber-equiv A B ζ (lower-funext 𝓤 𝓥 fe) g)) (Π-is-prop fe (λ x → i x (g x)))For any proposition P, the unique map P → 𝟙 is an embedding:unique-to-𝟙-is-embedding : (P : 𝓤 ̇ ) → is-prop P → ∀ 𝓥 → is-embedding (unique-to-𝟙 {𝓤} {𝓥}) unique-to-𝟙-is-embedding P i 𝓥 * (p , r) (p' , r') = to-×-＝ (i p p') (props-are-sets 𝟙-is-prop r r') embedding-into-𝟙 : (P : 𝓤 ̇ ) → is-prop P → P ↪ 𝟙 {𝓥} embedding-into-𝟙 {𝓤} {𝓥} P P-is-prop = unique-to-𝟙 , unique-to-𝟙-is-embedding P P-is-prop 𝓥Added by Tom de Jong. If a type X embeds into a proposition, then X is itself a proposition.subtypes-of-props-are-props'' : {X : 𝓤 ̇ } {P : 𝓥 ̇ } → is-prop P → X ↪ P → is-prop X subtypes-of-props-are-props'' P-is-prop (f , f-emb) = subtypes-of-props-are-props f f-emb P-is-propAdded by Martin Escardo 12th July 2023. Assuming univalence, the canonical map of X = Y into X → Y is an embedding.idtofun-is-embedding : is-univalent 𝓤 → {X Y : 𝓤 ̇ } → is-embedding (idtofun X Y) idtofun-is-embedding ua {X} {Y} = ∘-is-embedding (equivs-are-embeddings (idtoeq X Y) (ua X Y)) (pr₁-is-embedding (being-equiv-is-prop'' (univalence-gives-funext ua))) where remark : pr₁ ∘ idtoeq X Y ＝ idtofun X Y remark = refl Idtofun-is-embedding : is-univalent 𝓤 → funext (𝓤 ⁺) 𝓤 → {X Y : 𝓤 ̇ } → is-embedding (Idtofun {𝓤} {X} {Y}) Idtofun-is-embedding ua fe {X} {Y} = transport is-embedding (dfunext fe (idtofun-agreement X Y)) (idtofun-is-embedding ua) unique-from-𝟘-is-embedding : {X : 𝓤 ̇ } → is-embedding (unique-from-𝟘 {𝓤} {𝓥} {X}) unique-from-𝟘-is-embedding x (y , p) = 𝟘-elim yAdded by Martin Escardo and Tom de Jong 10th October 2023.id-is-essential : {X : 𝓤 ̇ } → is-essential (id {𝓤} {X}) 𝓥 id-is-essential {𝓤} {X} Z g = id ∘-is-essential : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } {f : X → Y} {g : Y → Z} → is-essential f 𝓣 → is-essential g 𝓣 → is-essential (g ∘ f) 𝓣 ∘-is-essential {𝓤} {𝓥} {𝓦} {𝓣} {X} {Y} {Z} {f} {g} f-ess g-ess W h ghf-emb = II where I : is-embedding (h ∘ g) I = f-ess W (h ∘ g) ghf-emb II : is-embedding h II = g-ess W h IWe originally hoped to prove that Idtofun was essential, but it's not: while the composite Idtofun evaluate at 0 (𝟚 ≃ 𝟚) ---------→ (𝟚 → 𝟚) ---------------> 𝟚 is an embedding, the evaluation map isn't. Added by Ian Ray 22nd August 2024equiv-embeds-into-function : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → FunExt → (X ≃ Y) ↪ (X → Y) equiv-embeds-into-function fe = (⌜_⌝ , pr₁-is-embedding (λ f → being-equiv-is-prop fe f))End of addition. Added by Martin Escardo 13th June 2025.Fiber : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X ↪ Y) → Y → Ω (𝓤 ⊔ 𝓥) Fiber 𝕛 y = fiber ⌊ 𝕛 ⌋ y , ⌊ 𝕛 ⌋-is-embedding y embedding-to-𝟙 : {P : Ω 𝓤} → P holds ↪ 𝟙 {𝓥} embedding-to-𝟙 {𝓤} {𝓥} {P} = embedding-into-𝟙 (P holds) (holds-is-prop P) fiber-to-𝟙 : {𝓦 : Universe} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (𝕛 : X ↪ Y) (y : Y) → fiber ⌊ 𝕛 ⌋ y ↪ 𝟙 {𝓦} fiber-to-𝟙 𝕛 y = embedding-to-𝟙 {_} {_} {Fiber 𝕛 y}Fixities:infix 0 _↪_ infix 1 _□ infixr 0 _↪⟨_⟩_