Martin Escardo and Tom de Jong, October 2021

Modified from UF.ImageAndSurjection.lagda to add the parameter F.

We use F to control the universe where propositional truncations live.
For more comments and explanations, see the original files.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan

module UF.ImageAndSurjection-Variation (F : Universe β†’ Universe) where

open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Hedberg
open import UF.PropTrunc-Variation F
open import UF.Retracts
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.Subsingletons-Properties

module ImageAndSurjection (pt : propositional-truncations-exist) where

 open PropositionalTruncation pt

 _∈image_ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ Y β†’ (X β†’ Y) β†’ F (𝓀 βŠ” π“₯) Μ‡
 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) β†’ F (𝓀 βŠ” π“₯) βŠ” π“₯ Μ‡
 image f = Ξ£ y κž‰ codomain f , y ∈image f

 restriction : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
             β†’ image f β†’ Y
 restriction f (y , _) = y

 restriction-embedding : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                       β†’ is-embedding (restriction f)
 restriction-embedding f = pr₁-is-embedding (Ξ» y β†’ βˆ₯βˆ₯-is-prop)

 corestriction : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
               β†’ X β†’ image f
 corestriction f x = f x , ∣ x , refl ∣

 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 s f c (y , p) (y' , p') =
  to-Ξ£-＝ (βˆ₯βˆ₯-rec s (Ξ» u β†’ βˆ₯βˆ₯-rec s (Ξ» v β†’ h u v) p') p ,
          βˆ₯βˆ₯-is-prop _ 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-truncation-of-domain-map' : (X : 𝓀 Μ‡ ) {Y : π“₯ Μ‡ }
                                                β†’ is-set Y
                                                 β†’ (f : X β†’ Y)
                                                β†’ wconstant f
                                                β†’ βˆ₯ X βˆ₯ β†’ image f
 wconstant-map-to-set-truncation-of-domain-map' X s f c =
  βˆ₯βˆ₯-rec
  (wconstant-maps-to-sets-have-propositional-images X s f c)
  (corestriction f)

 wconstant-map-to-set-truncation-of-domain-map : (X : 𝓀 Μ‡ ) {Y : π“₯ Μ‡ }
                                               β†’ is-set Y
                                               β†’ (f : X β†’ Y)
                                               β†’ wconstant f
                                                 β†’ βˆ₯ X βˆ₯ β†’ Y
 wconstant-map-to-set-truncation-of-domain-map X s f c =
  restriction f ∘ wconstant-map-to-set-truncation-of-domain-map' X s f c

 wconstant-map-to-set-factors-through-truncation-of-domain : (X : 𝓀 Μ‡ ) {Y : π“₯ Μ‡ }
                                                             (s : is-set Y)
                                                             (f : X β†’ Y)
                                                             (c : wconstant f)
                                                           β†’ f ∼ (wconstant-map-to-set-truncation-of-domain-map X s f c) ∘ ∣_∣
 wconstant-map-to-set-factors-through-truncation-of-domain X s f c = Ξ³
  where
   g : βˆ₯ X βˆ₯ β†’ image f
   g = wconstant-map-to-set-truncation-of-domain-map' X s f c
   p : is-prop (image f)
   p = wconstant-maps-to-sets-have-propositional-images X s f c
   Ξ³ : (x : X) β†’ f x ＝ restriction f (g ∣ x ∣)
   γ x = f x                               ＝⟨refl⟩
         restriction f (corestriction f x) ＝⟨ ap (restriction f)
                                              (p (corestriction f x) (g ∣ x ∣)) ⟩
         restriction f (g ∣ x ∣)           ∎

 is-surjection : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ F (𝓀 βŠ” π“₯) βŠ” π“₯ Μ‡
 is-surjection f = βˆ€ y β†’ βˆƒ x κž‰ domain f , f x ＝ y

 _β† _ : 𝓀 Μ‡ β†’ π“₯ Μ‡ β†’ F (𝓀 βŠ” π“₯) βŠ” 𝓀 βŠ” π“₯ Μ‡
 X β†  Y = Ξ£ f κž‰ (X β†’ Y) , is-surjection f

 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-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 = g , h
  where
   g : is-vv-equiv f β†’ is-embedding f Γ— is-surjection f
   g i = (Ξ» y β†’ pr₁ (pr₁ the-singletons-are-the-inhabited-propositions (i y))) ,
         (Ξ» y β†’ prβ‚‚ (pr₁ the-singletons-are-the-inhabited-propositions (i y)))

   h : is-embedding f Γ— is-surjection f β†’ is-vv-equiv f
   h (e , s) = Ξ» y β†’ prβ‚‚ the-singletons-are-the-inhabited-propositions (e y , s 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 = prβ‚‚ (vv-equiv-iff-embedding-and-surjection f) (e , s)

 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)

 corestriction-is-surjection : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                             β†’ is-surjection (corestriction f)
 corestriction-is-surjection 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 _ _)

 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)

 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' = corestriction-is-surjection 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)

 imageInduction : βˆ€ {𝓦 𝓀 π“₯} {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦  ⁺ Μ‡
 imageInduction {𝓦} {𝓀} {π“₯} {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 β†’ imageInduction {𝓦} f
 surjection-induction f is P isp a y = βˆ₯βˆ₯-rec (isp y)
                                             (Ξ» Οƒ β†’ transport P (prβ‚‚ Οƒ) (a (pr₁ Οƒ)))
                                             (is y)

 image-surjection-converse : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                           β†’ imageInduction f β†’ is-surjection f
 image-surjection-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)
                                          (corestriction-is-surjection f)

 retraction-surjection : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                       β†’ has-section f β†’ is-surjection f
 retraction-surjection {𝓀} {π“₯} {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)

 surjection-≃-image : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                    β†’ is-surjection f
                    β†’ image f ≃ Y
 surjection-≃-image {𝓀} {π“₯} {X} {Y} f s =
  image f                       β‰ƒβŸ¨by-definition⟩
  (Ξ£ y κž‰ Y , βˆƒ x κž‰ X , f x ＝ y) β‰ƒβŸ¨ Ξ£-cong Ξ³ ⟩
  (Ξ£ y κž‰ Y , πŸ™)                 β‰ƒβŸ¨by-definition⟩
  Y Γ— πŸ™                         β‰ƒβŸ¨ πŸ™-rneutral {π“₯} {π“₯} ⟩
  Y                             β– 
   where
    Ξ³ : (y : Y) β†’ (βˆƒ x κž‰ X , f x ＝ y) ≃ πŸ™
    Ξ³ y = singleton-≃-πŸ™ (pointed-props-are-singletons (s y) βˆ₯βˆ₯-is-prop)

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