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                       โโจ โ-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)

โ-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}