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}