module 1Lab.Equiv.Embedding where
Embeddingsπ
One of the most important observations leading to the development of categorical set theory is that injective maps into a set correspond to maps from into a universe of propositions, normally denoted . Classically, this object is , but there are other settings in which this idea makes sense (elementary topoi) where the subobject classifier is not a coproduct .
To develop this correspondence, we note that, if a map is injective and its codomain is a set, then all the fibres
of
are propositions.
injective : (A β B) β Type _ injective f = β {x y} β f x β‘ f y β x β‘ y injectiveβis-embedding : is-set B β (f : A β B) β injective f β β x β is-prop (fibre f x) injectiveβis-embedding bset f inj x (f*x , p) (f*xβ² , q) = Ξ£-prop-path (Ξ» x β bset _ _) (inj (p β sym q))
In fact, this condition is not only necessary, it is also sufficient. Thus, we conclude that, for maps between sets, these notions are equivalent, and we could take either as the definition of βsubset inclusionβ.
has-prop-fibresβinjective : (f : A β B) β (β x β is-prop (fibre f x)) β injective f has-prop-fibresβinjective _ prop p = ap fst (prop _ (_ , p) (_ , refl)) between-sets-injectiveβhas-prop-fibres : is-set A β is-set B β (f : A β B) β injective f β (β x β is-prop (fibre f x)) between-sets-injectiveβhas-prop-fibres aset bset f = prop-ext (Ξ» p q i x β aset _ _ (p x) (q x) i) (Ξ -is-hlevel 1 Ξ» _ β is-prop-is-prop) (injectiveβis-embedding bset f) (has-prop-fibresβinjective f)
Since we want βis a subtype inclusionβ to be a property β that is, we really want to not care about how a function is a subtype inclusion, only that it is, we define embeddings as those functions which have propositional fibres:
is-embedding : (A β B) β Type _ is-embedding f = β x β is-prop (fibre f x) _βͺ_ : Type β β Type ββ β Type _ A βͺ B = Ξ£[ f β (A β B) ] is-embedding f
Univalence β specifically, the existence of classifying objects for maps with -fibres β tells us that the embeddings into correspond to the families of propositional types over .
subtype-classifier : β {β} {B : Type β} β (Ξ£[ A β Type β ] (A βͺ B)) β (B β Ξ£[ T β Type β ] (is-prop T)) subtype-classifier {β} = Map-classifier {β = β} is-prop module subtype-classifier {β} {B : Type β} = Equiv (subtype-classifier {B = B})
A canonical source of embedding, then, are the first projections from total spaces of propositional families. This is because, as Fibre-equiv tells us, the fibre of over is equivalent to βthe space of possible second coordinatesβ, i.e., . Since was assumed to be a prop., then so are the fibres of fst.
Subset-proj-embedding : β {B : A β Type β} β (β x β is-prop (B x)) β is-embedding {A = Ξ£ A B} fst Subset-proj-embedding {B = B} Bprop x = is-hlevelβ 1 (Fibre-equiv B x) (Bprop _)
embeddingβmonic : β {β ββ² ββ²β²} {A : Type β} {B : Type ββ²} {f : A β B} β is-embedding f β β {C : Type ββ²β²} (g h : C β A) β f β g β‘ f β h β g β‘ h embeddingβmonic {f = f} emb g h p = funext Ξ» x β ap fst (emb _ (g x , refl) (h x , happly (sym p) x)) monicβis-embedding : β {β ββ² ββ²β²} {A : Type β} {B : Type ββ²} {f : A β B} β is-set B β (β {C : Set ββ²β²} (g h : β£ C β£ β A) β f β g β‘ f β h β g β‘ h) β is-embedding f monicβis-embedding {f = f} bset monic = injectiveβis-embedding bset _ Ξ» {x} {y} p β happly (monic {C = el (Lift _ β€) (Ξ» _ _ _ _ i j β lift tt)} (Ξ» _ β x) (Ξ» _ β y) (funext (Ξ» _ β p))) _
As ff morphismsπ
A fully faithful functor is a functor whose action on morphisms is an isomorphism everywhere. By the βtypes are higher groupoidsβ analogy, functors are functions, so weβre left to consider: what is a fully faithful function? The answer turns out to be precisely βan embeddingβ, as long as we interpret βfully faithfulβ to mean βaction on morphisms is an equivalenceβ everywhere.
module _ {β ββ²} {A : Type β} {B : Type ββ²} {f : A β B} where embedding-lemma : (β x β is-contr (fibre f (f x))) β is-embedding f embedding-lemma cffx y (x , p) q = is-contrβis-prop (subst is-contr (ap (fibre f) p) (cffx x)) (x , p) q cancellableβembedding : (β {x y} β (f x β‘ f y) β (x β‘ y)) β is-embedding f cancellableβembedding eqv = embedding-lemma Ξ» x β is-hlevelβ 0 (Ξ£-ap-snd (Ξ» _ β eqv)) $ contr (x , refl) Ξ» (y , p) i β p (~ i) , Ξ» j β p (~ i β¨ j) embeddingβcancellable : is-embedding f β β {x y} β is-equiv {B = f x β‘ f y} (ap f) embeddingβcancellable emb = totalβequiv {f = Ξ» y p β ap f {y = y} p} (is-contrβis-equiv (contr (_ , refl) Ξ» (y , p) i β p i , Ξ» j β p (i β§ j)) (contr (_ , refl) (is-hlevelβ 1 (Ξ£-ap-snd Ξ» _ β sym-equiv) (emb _) _)))