Martin Escardo. \begin{code} {-# OPTIONS --safe --without-K #-} open import UF.PropTrunc module UF.ImageAndSurjection (pt : propositional-truncations-exist) where open import MLTT.Spartan open import UF.Base open import UF.Embeddings open import UF.Equiv open import UF.EquivalenceExamples open import UF.FunExt open import UF.Hedberg 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 \end{code} A main application of propositional truncations is to be able to define images and surjections: \begin{code} open PropositionalTruncation pt _βimage_ : {X : π€ Μ } {Y : π₯ Μ } β Y β (X β Y) β π€ β π₯ Μ y βimage f = β x κ domain f , f x οΌ y being-in-the-image-is-prop : {X : π€ Μ } {Y : π₯ Μ } (y : Y) (f : X β Y) β is-prop (y βimage f) being-in-the-image-is-prop y f = β-is-prop image : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ Μ image f = Ξ£ y κ codomain f , y βimage f restriction : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β image f β Y restriction f (y , _) = y corestriction : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β X β image f corestriction f x = f x , β£ x , refl β£ image-factorization : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β f βΌ restriction f β corestriction f image-factorization f x = refl restrictions-are-embeddings : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-embedding (restriction f) restrictions-are-embeddings f = prβ-is-embedding (Ξ» y β β₯β₯-is-prop) is-surjection : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ Μ is-surjection f = β y β y βimage f being-surjection-is-prop : FunExt β {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-prop (is-surjection f) being-surjection-is-prop fe f = Ξ -is-prop (fe _ _) (Ξ» y β being-in-the-image-is-prop y f) corestrictions-are-surjections : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-surjection (corestriction f) corestrictions-are-surjections f (y , s) = β₯β₯-functor g s where g : (Ξ£ x κ domain f , f x οΌ y) β Ξ£ x κ domain f , corestriction f x οΌ (y , s) g (x , p) = x , to-Ξ£-οΌ (p , β₯β₯-is-prop _ _) id-is-surjection : {X : π€ Μ } β is-surjection (ππ X) id-is-surjection = Ξ» y β β£ y , refl β£ _β _ : π€ Μ β π₯ Μ β π€ β π₯ Μ X β Y = Ξ£ f κ (X β Y) , is-surjection f β_β : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β (X β Y) β (f , i) β = f ββ-is-surjection : {X : π€ Μ } {Y : π₯ Μ } (π― : X β Y) β is-surjection β π― β ββ-is-surjection (f , i) = i _is-image-of_ : π€ Μ β π₯ Μ β π€ β π₯ Μ Y is-image-of X = X β Y image-is-set : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-set Y β is-set (image f) image-is-set f i = subsets-of-sets-are-sets _ (Ξ» y β y βimage f) i (being-in-the-image-is-prop _ f) vv-equivs-are-surjections : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-vv-equiv f β is-surjection f vv-equivs-are-surjections f i y = prβ (lr-implication the-singletons-are-the-inhabited-propositions (i y)) surjective-embeddings-are-vv-equivs : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-embedding f β is-surjection f β is-vv-equiv f surjective-embeddings-are-vv-equivs f e s y = rl-implication the-singletons-are-the-inhabited-propositions (e y , s y) surjective-embeddings-are-equivs : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-embedding f β is-surjection f β is-equiv f surjective-embeddings-are-equivs f e s = vv-equivs-are-equivs f (surjective-embeddings-are-vv-equivs f e s) vv-equiv-iff-embedding-and-surjection : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-vv-equiv f β is-embedding f Γ is-surjection f vv-equiv-iff-embedding-and-surjection f = (Ξ» i β vv-equivs-are-embeddings f i , vv-equivs-are-surjections f i) , (Ξ» (e , s) β surjective-embeddings-are-vv-equivs f e s) pt-is-surjection : {X : π€ Μ } β is-surjection (Ξ» (x : X) β β£ x β£) pt-is-surjection t = β₯β₯-rec β₯β₯-is-prop (Ξ» x β β£ x , β₯β₯-is-prop (β£ x β£) t β£) t NatΞ£-is-surjection : {X : π€ Μ } (A : X β π₯ Μ ) (B : X β π¦ Μ ) (ΞΆ : Nat A B) β ((x : X) β is-surjection (ΞΆ x)) β is-surjection (NatΞ£ ΞΆ) NatΞ£-is-surjection A B ΞΆ i (x , b) = Ξ³ where Ξ΄ : (Ξ£ a κ A x , ΞΆ x a οΌ b) β Ξ£ (x' , a) κ Ξ£ A , (x' , ΞΆ x' a) οΌ (x , b) Ξ΄ (a , p) = (x , a) , (ap (x ,_) p) Ξ³ : β (x' , a) κ Ξ£ A , (x' , ΞΆ x' a) οΌ (x , b) Ξ³ = β₯β₯-functor Ξ΄ (i x b) \end{code} TODO. The converse of the above holds. Surjections can be characterized as follows, modulo size: \begin{code} Surjection-Induction : β {π¦ π€ π₯} {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ β π¦ βΊ Μ Surjection-Induction {π¦} {π€} {π₯} {X} {Y} f = (P : Y β π¦ Μ ) β ((y : Y) β is-prop (P y)) β ((x : X) β P (f x)) β (y : Y) β P y surjection-induction : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-surjection f β Surjection-Induction {π¦} f surjection-induction f is P P-is-prop a y = β₯β₯-rec (P-is-prop y) (Ξ» Ο β transport P (prβ Ο) (a (prβ Ο))) (is y) surjection-induction-converse : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β Surjection-Induction f β is-surjection f surjection-induction-converse f is' = is' (Ξ» y β β₯ Ξ£ (Ξ» x β f x οΌ y) β₯) (Ξ» y β β₯β₯-is-prop) (Ξ» x β β£ x , refl β£) image-induction : β {π¦} {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) (P : image f β π¦ Μ ) β (β y' β is-prop (P y')) β (β x β P (corestriction f x)) β β y' β P y' image-induction f = surjection-induction (corestriction f) (corestrictions-are-surjections f) set-right-cancellable : {X : π€ Μ } {A : π₯ Μ } β (X β A) β π€Ο set-right-cancellable f = {π¦ : Universe} β (B : π¦ Μ ) β is-set B β (g h : codomain f β B) β g β f βΌ h β f β g βΌ h surjections-are-set-rc : {X : π€ Μ } {A : π₯ Μ } (f : X β A) β is-surjection f β set-right-cancellable f surjections-are-set-rc f f-is-surjection B B-is-set g h H = surjection-induction f f-is-surjection (Ξ» a β g a οΌ h a) (Ξ» a β B-is-set) (Ξ» x β g (f x) οΌβ¨ (H x) β© h (f x) β) retractions-are-surjections : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β has-section f β is-surjection f retractions-are-surjections {π€} {π₯} {X} f Ο y = β£ prβ Ο y , prβ Ο y β£ prβ-is-surjection : {X : π€ Μ } (A : X β π₯ Μ ) β ((x : X) β β₯ A x β₯) β is-surjection (Ξ» (Ο : Ξ£ A) β prβ Ο) prβ-is-surjection A s x = Ξ³ where Ξ΄ : A x β Ξ£ Ο κ Ξ£ A , prβ Ο οΌ x Ξ΄ a = (x , a) , refl Ξ³ : β Ο κ Ξ£ A , prβ Ο οΌ x Ξ³ = β₯β₯-functor Ξ΄ (s x) prβ-is-surjection-converse : {X : π€ Μ } (A : X β π₯ Μ ) β is-surjection (Ξ» (Ο : Ξ£ A) β prβ Ο) β ((x : X) β β₯ A x β₯) prβ-is-surjection-converse A s x = Ξ³ where Ξ΄ : (Ξ£ Ο κ Ξ£ A , prβ Ο οΌ x) β A x Ξ΄ ((.x , a) , refl) = a Ξ³ : β₯ A x β₯ Ξ³ = β₯β₯-functor Ξ΄ (s x) wconstant-maps-to-sets-have-propositional-images : {X : π€ Μ } {Y : π₯ Μ } β is-set Y β (f : X β Y) β wconstant f β is-prop (image f) wconstant-maps-to-sets-have-propositional-images {π€} {π₯} {X} {Y} s f c (y , p) (y' , p') = to-subtype-οΌ (Ξ» _ β β₯β₯-is-prop) (β₯β₯-rec s q p) where q : (Ξ£ x κ X , f x οΌ y) β y οΌ y' q u = β₯β₯-rec s (h u) p' where h : (Ξ£ x κ X , f x οΌ y) β (Ξ£ x' κ X , f x' οΌ y') β y οΌ y' h (x , e) (x' , e') = y οΌβ¨ e β»ΒΉ β© f x οΌβ¨ c x x' β© f x' οΌβ¨ e' β© y' β wconstant-map-to-set-factors-through-truncation-of-domain : {X : π€ Μ } {Y : π₯ Μ } β is-set Y β (f : X β Y) β wconstant f β Ξ£ f' κ (β₯ X β₯ β Y) , f βΌ f' β β£_β£ wconstant-map-to-set-factors-through-truncation-of-domain {π€} {π₯} {X} {Y} Y-is-set f f-is-wconstant = f' , h where i : is-prop (image f) i = wconstant-maps-to-sets-have-propositional-images Y-is-set f f-is-wconstant f'' : β₯ X β₯ β image f f'' = β₯β₯-rec i (corestriction f) f' : β₯ X β₯ β Y f' = restriction f β f'' h : f βΌ f' β β£_β£ h x = f x οΌβ¨ refl β© restriction f (corestriction f x) οΌβ¨ Ο β© restriction f (f'' β£ x β£) οΌβ¨ refl β© f' β£ x β£ β where Ο = ap (restriction f) (i (corestriction f x) (f'' β£ x β£)) factor-through-surjection : {X : π€ Μ } {A : π₯ Μ } β (f : X β A) β is-surjection f β {B : π¦ Μ } β is-set B β (g : X β B) β ((x y : X) β f x οΌ f y β g x οΌ g y) β Ξ£ h κ (A β B) , h β f βΌ g factor-through-surjection {π€} {π₯} {π¦} {X} {A} f f-is-surjection {B} B-is-set g g-respects-f = Ξ³ where Ο : (a : A) β fiber f a β B Ο _ (x , _) = g x Ο-is-wconstant : (a : A) (u v : fiber f a) β Ο a u οΌ Ο a v Ο-is-wconstant a (x , p) (y , q) = g-respects-f x y (f x οΌβ¨ p β© a οΌβ¨ q β»ΒΉ β© f y β) Ο : (a : A) β Ξ£ Ο κ (β₯ fiber f a β₯ β B) , Ο a βΌ Ο β β£_β£ Ο a = wconstant-map-to-set-factors-through-truncation-of-domain B-is-set (Ο a) (Ο-is-wconstant a) h : A β B h a = prβ (Ο a) (f-is-surjection a) H : h β f βΌ g H x = h (f x) οΌβ¨ refl β© prβ (Ο (f x)) (f-is-surjection (f x)) οΌβ¨ i β© prβ (Ο (f x)) β£ x , refl β£ οΌβ¨ ii β© Ο (f x) (x , refl) οΌβ¨ refl β© g x β where i = ap (prβ (Ο (f x))) (β₯β₯-is-prop (f-is-surjection (f x)) β£ x , refl β£) ii = (prβ (Ο (f x)) (x , refl))β»ΒΉ Ξ³ : Ξ£ h κ (A β B) , h β f βΌ g Ξ³ = (h , H) factor-through-surjection! : Fun-Ext β {X : π€ Μ } {A : π₯ Μ } β (f : X β A) β is-surjection f β {B : π¦ Μ } β is-set B β (g : X β B) β ((x y : X) β f x οΌ f y β g x οΌ g y) β β! h κ (A β B) , h β f βΌ g factor-through-surjection! fe {X} {A} f f-is-surjection {B} B-is-set g g-respects-f = IV where I : (Ξ£ h κ (A β B) , h β f βΌ g) β β! h κ (A β B) , h β f βΌ g I (h , H) = III where II : (k : A β B) β k β f βΌ g β h βΌ k II k K = surjections-are-set-rc f f-is-surjection B B-is-set h k (Ξ» x β h (f x) οΌβ¨ H x β© g x οΌβ¨ (K x)β»ΒΉ β© k (f x) β) III : β! h κ (A β B) , h β f βΌ g III = (h , H) , (Ξ» (k , K) β to-subtype-οΌ (Ξ» - β Ξ -is-prop fe (Ξ» x β B-is-set)) (dfunext fe (II k K))) IV : β! h κ (A β B) , h β f βΌ g IV = I (factor-through-surjection f f-is-surjection B-is-set g g-respects-f) factor-through-image : Fun-Ext β {X : π€ Μ } {A : π₯ Μ } β (f : X β A) β {B : π¦ Μ } β is-set B β (g : X β B) β ((x y : X) β f x οΌ f y β g x οΌ g y) β β! h κ (image f β B) , h β corestriction f βΌ g factor-through-image fe f B-is-set g g-respects-f = factor-through-surjection! fe (corestriction f) (corestrictions-are-surjections f) B-is-set g r where r : β x y β f x , β£ x , refl β£ οΌ f y , β£ y , refl β£ β g x οΌ g y r x y p = g-respects-f x y (ap prβ p) \end{code} Added by Tom de Jong on 4 December 2020. \begin{code} corestriction-of-embedding-is-equivalence : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-embedding f β is-equiv (corestriction f) corestriction-of-embedding-is-equivalence f e = surjective-embeddings-are-equivs f' e' s' where f' : domain f β image f f' = corestriction f s' : is-surjection f' s' = corestrictions-are-surjections f e' : is-embedding f' e' (y , p) = retract-of-prop Ξ³ (e y) where Ξ³ : fiber f' (y , p) β fiber f y Ξ³ = Ξ£-retract (Ξ» x β f' x οΌ y , p) (Ξ» x β f x οΌ y) Ο where Ο : (x : domain f) β (f' x οΌ (y , p)) β (f x οΌ y) Ο x = Ο , Ο , Ξ· where Ο : f x οΌ y β f' x οΌ (y , p) Ο q = to-subtype-οΌ (Ξ» y' β β₯β₯-is-prop) q Ο : f' x οΌ (y , p) β f x οΌ y Ο q' = ap prβ q' Ξ· : Ο β Ο βΌ id Ξ· refl = to-Ξ£-οΌ (refl , q) οΌβ¨ ap (Ξ» - β to-Ξ£-οΌ (refl , -)) h β© to-Ξ£-οΌ (refl , refl) οΌβ¨ refl β© refl β where q : β£ x , refl β£ οΌ β£ x , refl β£ q = β₯β₯-is-prop β£ x , refl β£ β£ x , refl β£ h : q οΌ refl h = props-are-sets β₯β₯-is-prop q refl embedding-if-corestriction-is-equivalence : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-equiv (corestriction f) β is-embedding f embedding-if-corestriction-is-equivalence f i = embedding-closed-under-βΌ f' f (β-is-embedding eβ eβ) H where f' : domain f β codomain f f' = prβ β corestriction f H : f βΌ prβ β corestriction f H x = refl eβ : is-embedding (corestriction f) eβ = equivs-are-embeddings (corestriction f) i eβ : is-embedding prβ eβ = prβ-is-embedding (Ξ» y β β₯β₯-is-prop) \end{code} Added 13 February 2020 by Tom de Jong. \begin{code} surjection-β-image : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-surjection f β image f β Y surjection-β-image {π€} {π₯} {X} {Y} f s = image f ββ¨ β-refl _ β© (Ξ£ y κ Y , β x κ X , f x οΌ y) ββ¨ Ξ£-cong Ξ³ β© (Ξ£ y κ Y , π) ββ¨ β-refl _ β© Y Γ π ββ¨ π-rneutral {π₯} {π₯} β© Y β where Ξ³ : (y : Y) β (β x κ X , f x οΌ y) β π Ξ³ y = singleton-β-π (pointed-props-are-singletons (s y) β₯β₯-is-prop) \end{code} Added 18 December 2020 by Tom de Jong. \begin{code} β-is-surjection : {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ } {f : X β Y} {g : Y β Z} β is-surjection f β is-surjection g β is-surjection (g β f) β-is-surjection {π€} {π₯} {π¦} {X} {Y} {Z} {f} {g} Ο Ο z = β₯β₯-rec β₯β₯-is-prop Ξ³β (Ο z) where Ξ³β : (Ξ£ y κ Y , g y οΌ z) β β x κ X , (g β f) x οΌ z Ξ³β (y , q) = β₯β₯-functor Ξ³β (Ο y) where Ξ³β : (Ξ£ x κ X , f x οΌ y) β Ξ£ x κ X , (g β f) x οΌ z Ξ³β (x , p) = (x , (g (f x) οΌβ¨ ap g p β© g y οΌβ¨ q β© z β)) equivs-are-surjections : {X : π€ Μ } {Y : π₯ Μ } {f : X β Y} β is-equiv f β is-surjection f equivs-are-surjections ((Ο , Ξ·) , (Ο , Ξ΅)) y = β£ Ο y , Ξ· y β£ \end{code}