Tom de Jong, 4 & 5 April 2022.

Assuming set quotients, we
(1) derive propositional truncations in the presence of function extensionality;
(2) prove Set Replacement as defined in UF-Size.lagda.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

module UF-Quotient where

open import SpartanMLTT

open import UF-Base hiding (_β‰ˆ_)
open import UF-Equiv
open import UF-FunExt
open import UF-ImageAndSurjection
open import UF-PropTrunc
open import UF-Subsingletons
open import UF-Subsingletons-FunExt
open import UF-Size

is-prop-valued is-equiv-relation : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡
is-prop-valued    _β‰ˆ_ = βˆ€ x y β†’ is-prop (x β‰ˆ y)
is-equiv-relation _β‰ˆ_ = is-prop-valued _β‰ˆ_ Γ— reflexive  _β‰ˆ_
                      Γ— symmetric      _β‰ˆ_ Γ— transitive _β‰ˆ_

EqRel : {𝓀 π“₯ : Universe} β†’ 𝓀 Μ‡ β†’ 𝓀 βŠ” (π“₯ ⁺) Μ‡
EqRel {𝓀} {π“₯} X = Ξ£ R κž‰ (X β†’ X β†’ π“₯ Μ‡ ) , is-equiv-relation R

_β‰ˆ[_]_ : {X : 𝓀 Μ‡ } β†’ X β†’ EqRel X β†’ X β†’ π“₯ Μ‡
x β‰ˆ[ _β‰ˆ_ , _ ] y = x β‰ˆ y

identifies-related-points : {X : 𝓀 Μ‡  } (β‰ˆ : EqRel {𝓀} {π“₯} X) {Y : 𝓦 Μ‡  }
                          β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
identifies-related-points (_β‰ˆ_ , _) f = βˆ€ {x x'} β†’ x β‰ˆ x' β†’ f x ≑ f x'

record set-quotients-exist : 𝓀ω where
 field
  _/_ : {𝓀 π“₯ : Universe} (X : 𝓀 Μ‡  ) β†’ EqRel {𝓀} {π“₯} X β†’ 𝓀 βŠ” π“₯ Μ‡
  Ξ·/ : {𝓀 π“₯ : Universe} {X : 𝓀 Μ‡  } (≋ : EqRel {𝓀} {π“₯} X) β†’ X β†’ X / ≋
  Ξ·/-identifies-related-points : {𝓀 π“₯ : Universe}
                                 {X : 𝓀 Μ‡  } (≋ : EqRel {𝓀} {π“₯} X)
                               β†’ identifies-related-points ≋ (Ξ·/ ≋)
  /-is-set : {𝓀 π“₯ : Universe} {X : 𝓀 Μ‡  } (≋ : EqRel {𝓀} {π“₯} X) β†’ is-set (X / ≋)
  /-induction : {𝓀 π“₯ : Universe} {X : 𝓀 Μ‡  } (≋ : EqRel {𝓀} {π“₯} X)
                {𝓦 : Universe} {P : X / ≋ β†’ 𝓦 Μ‡  }
              β†’ ((x' : X / ≋) β†’ is-prop (P x'))
              β†’ ((x : X) β†’ P (Ξ·/ ≋ x)) β†’ (y : X / ≋) β†’ P y
  /-universality : {𝓀 π“₯ : Universe} {X : 𝓀 Μ‡  } (≋ : EqRel {𝓀} {π“₯} X)
                   {𝓦 : Universe} {Y : 𝓦 Μ‡  }
                 β†’ is-set Y β†’ (f : X β†’ Y)
                 β†’ identifies-related-points ≋ f
                 β†’ βˆƒ! fΜ… κž‰ (X / ≋ β†’ Y) , fΜ… ∘ Ξ·/ ≋ ∼ f

\end{code}

Paying attention to universe levels, it is important to note that the quotient
of X : 𝓀 by a π“₯-valued equivalence relation is assumed to live in 𝓀 βŠ” π“₯. In
particular, the quotient of type in 𝓀 by a 𝓀-valued equivalence relation lives
in 𝓀 again.

The following is boilerplate and duplicates some of the material in
UF-Quotient.lagda, where large set quotients are constructed using propositional
truncations, function extensionality and propositional extensionality.

We need the boilerplate in OrdinalOfOrdinalsSuprema.lagda, where we use set
quotients to construct small suprema of small ordinals.


A quotient is said to be effective if for every x, y : X, we have x β‰ˆ y whenever
Ξ·/ x ≑ β€ŒΞ·/ y. Notice that we did not include effectivity as a requirement in
'set-quotients-exist'. But actually it follows from the other properties, at
least in the presence of function extensionality and propositonal
extensionality, as MartΓ­n observed. The proof is as follows:

(1) First construct propositional truncations using assumed set quotients.
(2) Construct another (large) quotient as described in UF-Large-Quotients.lagda.
(3) This large quotient is effective, but has to be isomorphic to the assumed
    set quotient, hence this quotient has to be effective as well.

TODO: Implement this in Agda.

\begin{code}

 module _
         {X : 𝓀 Μ‡  }
         (≋@(_β‰ˆ_ , β‰ˆp , β‰ˆr , β‰ˆs , β‰ˆt) : EqRel {𝓀} {π“₯} X)
        where

  module _
          {A : 𝓦 Μ‡  }
          (A-is-set : is-set A)
         where

   mediating-map/ : (f : X β†’ A)
                  β†’ identifies-related-points ≋ f
                  β†’ X / ≋ β†’ A
   mediating-map/ f p = βˆƒ!-witness (/-universality ≋ A-is-set f p)

   universality-triangle/ : (f : X β†’ A)
                            (p : identifies-related-points ≋ f)
                          β†’ mediating-map/ f p ∘ Ξ·/ ≋ ∼ f
   universality-triangle/ f p = βˆƒ!-is-witness (/-universality ≋ A-is-set f p)

\end{code}

We extend unary and binary prop-valued relations to the quotient.

\begin{code}

 module extending-relations-to-quotient (fe : Fun-Ext) (pe : Prop-Ext) where

  module _
          {X : 𝓀 Μ‡  }
          (≋@(_β‰ˆ_ , β‰ˆp , β‰ˆr , β‰ˆs , β‰ˆt) : EqRel {𝓀} {π“₯} X)
         where

   module _
           (r : X β†’ Ξ© 𝓣)
           (p : {x y : X} β†’ x β‰ˆ y β†’ r x ≑ r y)
          where

    extension-rel₁ : X / ≋ β†’ Ξ© 𝓣
    extension-rel₁ = mediating-map/ ≋ (Ξ©-is-set fe pe) r p

    extension-rel-triangle₁ : extension-rel₁ ∘ Ξ·/ ≋ ∼ r
    extension-rel-triangle₁ = universality-triangle/ ≋ (Ξ©-is-set fe pe) r p

   module _ (r : X β†’ X β†’ Ξ© 𝓣)
            (p : {x y x' y' : X} β†’ x β‰ˆ x' β†’ y β‰ˆ y' β†’ r x y ≑ r x' y')
          where

    abstract
     private
      p' : (x : X) {y y' : X} β†’ y β‰ˆ y' β†’ r x y ≑ r x y'
      p' x {y} {y'} = p (β‰ˆr x)

      r₁ : X β†’ X / ≋ β†’ Ξ© 𝓣
      r₁ x = extension-rel₁ (r x) (p' x)

      Ξ΄ : {x x' : X} β†’ x β‰ˆ x' β†’ (y : X) β†’ r₁ x (Ξ·/ ≋ y) ≑ r₁ x' (Ξ·/ ≋ y)
      Ξ΄ {x} {x'} e y =
        r₁ x  (Ξ·/ ≋ y)  β‰‘βŸ¨ extension-rel-triangle₁ (r x) (p (β‰ˆr x)) y        ⟩
        r  x     y      β‰‘βŸ¨ p e (β‰ˆr y)                                        ⟩
        r  x'    y      β‰‘βŸ¨ (extension-rel-triangle₁ (r x') (p (β‰ˆr x')) y) ⁻¹ ⟩
        r₁ x' (Ξ·/ ≋ y)  ∎

      ρ : (q : X / ≋) {x x' : X} β†’ x β‰ˆ x' β†’ r₁ x q ≑ r₁ x' q
      ρ q {x} {x'} e = /-induction ≋ (Ξ» q β†’ Ξ©-is-set fe pe) (Ξ΄ e) q

      rβ‚‚ : X / ≋ β†’ X / ≋ β†’ Ξ© 𝓣
      rβ‚‚ = mediating-map/ ≋ (Ξ -is-set fe (Ξ» _ β†’ Ξ©-is-set fe pe)) r₁
                            (Ξ» {x} {x'} e β†’ dfunext fe (Ξ» q β†’ ρ q e))

      Οƒ : (x : X) β†’ rβ‚‚ (Ξ·/ ≋ x) ≑ r₁ x
      Οƒ = universality-triangle/ ≋ (Ξ -is-set fe (Ξ» _ β†’ Ξ©-is-set fe pe)) r₁
                                   (Ξ» {x} {x'} e β†’ dfunext fe (Ξ» q β†’ ρ q e))

      Ο„ : (x y : X) β†’ rβ‚‚ (Ξ·/ ≋ x) (Ξ·/ ≋ y) ≑ r x y
      Ο„ x y = rβ‚‚ (Ξ·/ ≋ x) (Ξ·/ ≋ y) β‰‘βŸ¨ happly (Οƒ x) (Ξ·/ ≋ y) ⟩
              r₁ x        (Ξ·/ ≋ y) β‰‘βŸ¨ extension-rel-triangle₁ (r x) (p' x) y ⟩
              r  x            y    ∎

     extension-relβ‚‚ : X / ≋ β†’ X / ≋ β†’ Ξ© 𝓣
     extension-relβ‚‚ = rβ‚‚

     extension-rel-triangleβ‚‚ : (x y : X)
                             β†’ extension-relβ‚‚ (Ξ·/ ≋ x) (Ξ·/ ≋ y) ≑ r x y
     extension-rel-triangleβ‚‚ = Ο„

\end{code}

For proving properties of an extended binary relation, it is useful to have a
binary and ternary versions of quotient induction.

\begin{code}

 module _
         (fe : Fun-Ext)
         {X : 𝓀 Μ‡  }
         (≋ : EqRel {𝓀 } {π“₯} X)
        where

  /-inductionβ‚‚ : βˆ€ {𝓦} {P : X / ≋ β†’ X / ≋ β†’ 𝓦 Μ‡ }
               β†’ ((x' y' : X / ≋) β†’ is-prop (P x' y'))
               β†’ ((x y : X) β†’ P (Ξ·/ ≋ x) (Ξ·/ ≋ y))
               β†’ (x' y' : X / ≋) β†’ P x' y'
  /-inductionβ‚‚ p h =
   /-induction ≋ (Ξ» x' β†’ Ξ -is-prop fe (p x'))
                 (Ξ» x β†’ /-induction ≋ (p (Ξ·/ ≋ x)) (h x))

  /-induction₃ : βˆ€ {𝓦} β†’ {P : X / ≋ β†’ X / ≋ β†’ X / ≋ β†’ 𝓦 Μ‡ }
               β†’ ((x' y' z' : X / ≋) β†’ is-prop (P x' y' z'))
               β†’ ((x y z : X) β†’ P (Ξ·/ ≋ x) (Ξ·/ ≋ y) (Ξ·/ ≋ z))
               β†’ (x' y' z' : X / ≋) β†’ P x' y' z'
  /-induction₃ p h =
   /-inductionβ‚‚ (Ξ» x' y' β†’ Ξ -is-prop fe (p x' y'))
                (Ξ» x y β†’ /-induction ≋ (p (Ξ·/ ≋ x) (Ξ·/ ≋ y)) (h x y))


 quotients-equivalent : (X : 𝓀 Μ‡ ) (R : EqRel {𝓀} {π“₯} X) (R' : EqRel {𝓀} {𝓦} X)
                      β†’ ({x y : X} β†’ x β‰ˆ[ R ] y ⇔ x β‰ˆ[ R' ] y)
                      β†’ (X / R) ≃ (X / R')
 quotients-equivalent X (_β‰ˆ_  , β‰ˆp ,  β‰ˆr  , β‰ˆs  , β‰ˆt )
                        (_β‰ˆ'_ , β‰ˆp' , β‰ˆr' , β‰ˆs' , β‰ˆt') Ξ΅ = Ξ³
  where
   ≋  = (_β‰ˆ_  , β‰ˆp ,  β‰ˆr  , β‰ˆs  , β‰ˆt )
   ≋' = (_β‰ˆ'_ , β‰ˆp' , β‰ˆr' , β‰ˆs' , β‰ˆt')
   i : {x y : X} β†’ x β‰ˆ y β†’ Ξ·/ ≋' x ≑ Ξ·/ ≋' y
   i e = Ξ·/-identifies-related-points ≋' (lr-implication Ξ΅ e)
   i' : {x y : X} β†’ x β‰ˆ' y β†’ Ξ·/ ≋ x ≑ Ξ·/ ≋ y
   i' e = Ξ·/-identifies-related-points ≋ (rl-implication Ξ΅ e)
   f : X / ≋ β†’ X / ≋'
   f = mediating-map/ ≋ (/-is-set ≋') (Ξ·/ ≋') i
   f' : X / ≋' β†’ X / ≋
   f' = mediating-map/ ≋' (/-is-set ≋) (Ξ·/ ≋) i'
   a : (x : X) β†’ f (f' (Ξ·/ ≋' x)) ≑ Ξ·/ ≋' x
   a x = f (f' (Ξ·/ ≋' x)) β‰‘βŸ¨ I ⟩
         f (Ξ·/ ≋ x)       β‰‘βŸ¨ II ⟩
         Ξ·/ ≋' x          ∎
    where
     I  = ap f (universality-triangle/ ≋' (/-is-set ≋) (Ξ·/ ≋) i' x)
     II = universality-triangle/ ≋ (/-is-set ≋') (Ξ·/ ≋') i x
   α : f ∘ f' ∼ id
   Ξ± = /-induction ≋' (Ξ» _ β†’ /-is-set ≋') a
   a' : (x : X) β†’ f' (f (Ξ·/ ≋ x)) ≑ Ξ·/ ≋ x
   a' x = f' (f (Ξ·/ ≋ x)) β‰‘βŸ¨ I ⟩
         f' (Ξ·/ ≋' x)     β‰‘βŸ¨ II ⟩
         Ξ·/ ≋ x           ∎
    where
     I  = ap f' (universality-triangle/ ≋ (/-is-set ≋') (Ξ·/ ≋') i x)
     II = universality-triangle/ ≋' (/-is-set ≋) (Ξ·/ ≋) i' x
   α' : f' ∘ f ∼ id
   Ξ±' = /-induction ≋ (Ξ» _ β†’ /-is-set ≋) a'
   Ξ³ : (X / ≋) ≃ (X / ≋')
   Ξ³ = qinveq f (f' , Ξ±' , Ξ±)

\end{code}

We now construct propositional truncations using set quotients. Notice that
function extensionality is (only) needed to prove that the quotient is a
proposition.

\begin{code}

 private
  module _ {X : 𝓀 Μ‡  } where
   _β‰ˆ_ : X β†’ X β†’ 𝓀₀ Μ‡
   x β‰ˆ y = πŸ™
   ≋ : EqRel X
   ≋ = _β‰ˆ_ , (Ξ» x y β†’ πŸ™-is-prop) , (Ξ» x β†’ ⋆) , (Ξ» x y _ β†’ ⋆) , (Ξ» x y z _ _ β†’ ⋆)

  βˆ₯_βˆ₯ : 𝓀 Μ‡  β†’ 𝓀 Μ‡
  βˆ₯_βˆ₯ X = X / ≋

  ∣_∣ : {X : 𝓀 Μ‡  } β†’ X β†’ βˆ₯ X βˆ₯
  ∣_∣ = Ξ·/ ≋

  βˆ₯βˆ₯-is-prop : {X : 𝓀 Μ‡  } β†’ funext 𝓀 𝓀 β†’ is-prop βˆ₯ X βˆ₯
  βˆ₯βˆ₯-is-prop {𝓀} {X} fe = /-induction ≋ (Ξ» x' β†’ Ξ -is-prop fe (Ξ» y' β†’ /-is-set ≋))
                           (Ξ» x β†’ /-induction ≋ (Ξ» y' β†’ /-is-set ≋)
                                  (Ξ» y β†’ Ξ·/-identifies-related-points ≋ ⋆))

  βˆ₯βˆ₯-rec : {X : 𝓀 Μ‡  } {P : π“₯ Μ‡  } β†’ is-prop P β†’ (X β†’ P) β†’ βˆ₯ X βˆ₯ β†’ P
  βˆ₯βˆ₯-rec {𝓀} {π“₯} {X} {P} i f =
   βˆƒ!-witness (/-universality ≋ (props-are-sets i) f
                              (Ξ» {x} {x'}_ β†’ i (f x) (f x')))


 propositional-truncations-from-set-quotients :
  Fun-Ext β†’ propositional-truncations-exist
 propositional-truncations-from-set-quotients fe = record
  { βˆ₯_βˆ₯        = βˆ₯_βˆ₯
  ; βˆ₯βˆ₯-is-prop = βˆ₯βˆ₯-is-prop fe
  ; ∣_∣        = ∣_∣
  ; βˆ₯βˆ₯-rec     = βˆ₯βˆ₯-rec
  }

\end{code}

Finally, we show that Set Replacement is derivable when we have set quotients as
defined above.

Notice how we could replace propositional-truncations-exist assumption by
function extensionality (funext) as we can use funext to construct truncations,
as shown above.

\begin{code}

module _
        (sq : set-quotients-exist)
        (pt : propositional-truncations-exist)
       where
 open set-quotients-exist sq

 open ImageAndSurjection pt
 open PropositionalTruncation pt

 module set-replacement-construction
         {X : 𝓀 Μ‡  }
         {Y : 𝓦 Μ‡  }
         (f : X β†’ Y)
         (Y-is-loc-small : Y is-locally π“₯ small)
         (Y-is-set : is-set Y)
        where

  _β‰ˆ_ : X β†’ X β†’ 𝓦 Μ‡
  x β‰ˆ x' = f x ≑ f x'

  β‰ˆ-is-prop-valued : is-prop-valued _β‰ˆ_
  β‰ˆ-is-prop-valued x x' = Y-is-set

  β‰ˆ-is-reflexive : reflexive _β‰ˆ_
  β‰ˆ-is-reflexive x = refl

  β‰ˆ-is-symmetric : symmetric _β‰ˆ_
  β‰ˆ-is-symmetric x x' p = p ⁻¹

  β‰ˆ-is-transitive : transitive _β‰ˆ_
  β‰ˆ-is-transitive _ _ _ p q = p βˆ™ q

  β‰ˆ-is-equiv-rel : is-equiv-relation _β‰ˆ_
  β‰ˆ-is-equiv-rel = β‰ˆ-is-prop-valued , β‰ˆ-is-reflexive  ,
                   β‰ˆ-is-symmetric   , β‰ˆ-is-transitive

 \end{code}

 Using that Y is locally π“₯ small, we resize _β‰ˆ_ to a π“₯-valued equivalence
 relation.

 \begin{code}

  _β‰ˆβ»_ : X β†’ X β†’ π“₯ Μ‡
  x β‰ˆβ» x' = pr₁ (Y-is-loc-small (f x) (f x'))

  β‰ˆβ»-≃-β‰ˆ : {x x' : X} β†’ x β‰ˆβ» x' ≃ x β‰ˆ x'
  β‰ˆβ»-≃-β‰ˆ {x} {x'} = prβ‚‚ (Y-is-loc-small (f x) (f x'))

  β‰ˆβ»-is-prop-valued : is-prop-valued _β‰ˆβ»_
  β‰ˆβ»-is-prop-valued x x' = equiv-to-prop β‰ˆβ»-≃-β‰ˆ (β‰ˆ-is-prop-valued x x')

  β‰ˆβ»-is-reflexive : reflexive _β‰ˆβ»_
  β‰ˆβ»-is-reflexive x = ⌜ β‰ˆβ»-≃-β‰ˆ ⌝⁻¹ (β‰ˆ-is-reflexive x)

  β‰ˆβ»-is-symmetric : symmetric _β‰ˆβ»_
  β‰ˆβ»-is-symmetric x x' p = ⌜ β‰ˆβ»-≃-β‰ˆ ⌝⁻¹ (β‰ˆ-is-symmetric x x' (⌜ β‰ˆβ»-≃-β‰ˆ ⌝ p))

  β‰ˆβ»-is-transitive : transitive _β‰ˆβ»_
  β‰ˆβ»-is-transitive x x' x'' p q =
   ⌜ β‰ˆβ»-≃-β‰ˆ ⌝⁻¹ (β‰ˆ-is-transitive x x' x'' (⌜ β‰ˆβ»-≃-β‰ˆ ⌝ p) (⌜ β‰ˆβ»-≃-β‰ˆ ⌝ q))

  β‰ˆβ»-is-equiv-rel : is-equiv-relation _β‰ˆβ»_
  β‰ˆβ»-is-equiv-rel = β‰ˆβ»-is-prop-valued , β‰ˆβ»-is-reflexive  ,
                    β‰ˆβ»-is-symmetric   , β‰ˆβ»-is-transitive

  ≋ : EqRel X
  ≋ = _β‰ˆ_ , β‰ˆ-is-equiv-rel

  X/β‰ˆ : 𝓀 βŠ” 𝓦 Μ‡
  X/β‰ˆ = (X / ≋)

  X/β‰ˆβ» : 𝓀 βŠ” π“₯ Μ‡
  X/β‰ˆβ» = (X / (_β‰ˆβ»_ , β‰ˆβ»-is-equiv-rel))

  [_] : X β†’ X/β‰ˆ
  [_] = Ξ·/ ≋

  X/β‰ˆ-≃-X/β‰ˆβ» : X/β‰ˆ ≃ X/β‰ˆβ»
  X/β‰ˆ-≃-X/β‰ˆβ» = quotients-equivalent X ≋ (_β‰ˆβ»_ , β‰ˆβ»-is-equiv-rel)
                                        (⌜ β‰ˆβ»-≃-β‰ˆ ⌝⁻¹ , ⌜ β‰ˆβ»-≃-β‰ˆ ⌝)

 \end{code}

 We now proceed to show that X/β‰ˆ and image f are equivalent types.

 \begin{code}

  corestriction-respects-β‰ˆ : {x x' : X}
                           β†’ x β‰ˆ x'
                           β†’ corestriction f x ≑ corestriction f x'
  corestriction-respects-β‰ˆ =
   to-subtype-≑ (Ξ» y β†’ being-in-the-image-is-prop y f)

  quotient-to-image : X/β‰ˆ β†’ image f
  quotient-to-image = mediating-map/ ≋ (image-is-set f Y-is-set)
                       (corestriction f) (corestriction-respects-β‰ˆ)

  image-to-quotient' : (y : image f)
                     β†’ Ξ£ q κž‰ X/β‰ˆ , βˆƒ x κž‰ X , ([ x ] ≑ q) Γ— (f x ≑ pr₁ y)
  image-to-quotient' (y , p) = βˆ₯βˆ₯-rec prp r p
   where
    r : (Ξ£ x κž‰ X , f x ≑ y)
      β†’ (Ξ£ q κž‰ X/β‰ˆ , βˆƒ x κž‰ X , ([ x ] ≑ q) Γ— (f x ≑ y))
    r (x , e) = [ x ] , ∣ x , refl , e ∣
    prp : is-prop (Ξ£ q κž‰ X/β‰ˆ , βˆƒ x κž‰ X , ([ x ] ≑ q) Γ— (f x ≑ y))
    prp (q , u) (q' , u') = to-subtype-≑ (Ξ» _ β†’ βˆƒ-is-prop)
                                         (βˆ₯βˆ₯-recβ‚‚ (/-is-set ≋) Ξ³ u u')
     where
      Ξ³ : (Ξ£ x  κž‰ X , ([ x  ] ≑ q ) Γ— (f x  ≑ y))
        β†’ (Ξ£ x' κž‰ X , ([ x' ] ≑ q') Γ— (f x' ≑ y))
        β†’ q ≑ q'
      Ξ³ (x , refl , e) (x' , refl , refl) = Ξ·/-identifies-related-points ≋ e

  image-to-quotient : image f β†’ X/β‰ˆ
  image-to-quotient y = pr₁ (image-to-quotient' y)

  image-to-quotient-lemma : (x : X)
                          β†’ image-to-quotient (corestriction f x) ≑ [ x ]
  image-to-quotient-lemma x = βˆ₯βˆ₯-rec (/-is-set ≋) Ξ³ t
   where
    q : X/β‰ˆ
    q = image-to-quotient (corestriction f x)
    t : βˆƒ x' κž‰ X , ([ x' ] ≑ q) Γ— (f x' ≑ f x)
    t = prβ‚‚ (image-to-quotient' (corestriction f x))
    Ξ³ : (Ξ£ x' κž‰ X , ([ x' ] ≑ q) Γ— (f x' ≑ f x))
      β†’ q ≑ [ x ]
    Ξ³ (x' , u , v) =   q    β‰‘βŸ¨ u ⁻¹ ⟩
                     [ x' ] β‰‘βŸ¨ Ξ·/-identifies-related-points ≋ v ⟩
                     [ x  ] ∎

  image-≃-quotient : image f ≃ X/β‰ˆ
  image-≃-quotient = qinveq Ο• (ψ , ρ , Οƒ)
   where
    Ο• : image f β†’ X/β‰ˆ
    Ο• = image-to-quotient
    ψ : X/β‰ˆ β†’ image f
    ψ = quotient-to-image
    Ο„ : (x : X) β†’ ψ [ x ] ≑ corestriction f x
    Ο„ = universality-triangle/ ≋ (image-is-set f Y-is-set)
                               (corestriction f)
                               corestriction-respects-β‰ˆ
    Οƒ : Ο• ∘ ψ ∼ id
    Οƒ = /-induction ≋ (Ξ» x' β†’ /-is-set ≋) Ξ³
     where
      Ξ³ : (x : X) β†’ Ο• (ψ [ x ]) ≑ [ x ]
      Ξ³ x = Ο• (ψ [ x ])            β‰‘βŸ¨ ap Ο• (Ο„ x)                ⟩
            Ο• (corestriction f x ) β‰‘βŸ¨ image-to-quotient-lemma x ⟩
            [ x ]                  ∎
    ρ : ψ ∘ Ο• ∼ id
    ρ (y , p) = βˆ₯βˆ₯-rec (image-is-set f Y-is-set) Ξ³ p
     where
      Ξ³ : (Ξ£ x κž‰ X , f x ≑ y) β†’ ψ (Ο• (y , p)) ≑ (y , p)
      Ξ³ (x , refl) = ψ (Ο• (f x , p))           β‰‘βŸ¨ β¦…1⦆ ⟩
                     ψ (Ο• (corestriction f x)) β‰‘βŸ¨ β¦…2⦆ ⟩
                     ψ [ x ]                   β‰‘βŸ¨ β¦…3⦆ ⟩
                     corestriction f x         β‰‘βŸ¨ β¦…4⦆ ⟩
                     (f x , p)                 ∎
       where
        β¦…4⦆ = to-subtype-≑ (Ξ» yΒ β†’ being-in-the-image-is-prop y f) refl
        β¦…1⦆ = ap (ψ ∘ Ο•) (β¦…4⦆ ⁻¹)
        β¦…2⦆ = ap ψ (image-to-quotient-lemma x)
        β¦…3⦆ = Ο„ x

 set-replacement-from-set-quotients : Set-Replacement pt
 set-replacement-from-set-quotients
  {𝓦} {𝓣} {𝓀} {π“₯} {X} {Y} f X-is-small Y-is-loc-small Y-is-set = X/β‰ˆβ» , ≃-sym e
  where
   X' : 𝓀 Μ‡
   X' = pr₁ X-is-small
   Ο† : X' ≃ X
   Ο† = prβ‚‚ X-is-small
   f' : X' β†’ Y
   f' = f ∘ ⌜ Ο† ⌝
   open set-replacement-construction f' Y-is-loc-small Y-is-set
   open import UF-EquivalenceExamples
   e = image f  β‰ƒβŸ¨ Ξ£-cong (Ξ» y β†’ βˆ₯βˆ₯-cong pt (h y)) ⟩
       image f' β‰ƒβŸ¨ image-≃-quotient ⟩
       X/β‰ˆ      β‰ƒβŸ¨ X/β‰ˆ-≃-X/β‰ˆβ»       ⟩
       X/β‰ˆβ»     β– 
    where
     h : (y : Y) β†’ (Ξ£ x κž‰ X , f x ≑ y) ≃ (Ξ£ x' κž‰ X' , f' x' ≑ y)
     h y = ≃-sym (Ξ£-change-of-variable (Ξ» x β†’ f x ≑ y) ⌜ Ο† ⌝ (⌜⌝-is-equiv Ο†))

\end{code}