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' β©
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 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}

The following was marked as a TODO by Martin:
A map is an embedding iff its corestriction is an equivalence.
It was done 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 β©