Martin Escardo, August 2018.

Set quotients in univalent mathematics in Agda notation.

This took place during the Dagstuhl meeting "Formalization of
Mathematics in Type Theory", because Dan Grayson wanted to see how
universe levels work in Agda and I thought that this would be a nice
example to illustrate that.

We assume, in addition to Spartan Martin-LΓΆf type theory,

 * function extensionality
   (any two pointwise equal functions are equal),

 * propositional extensionality
   (any two logically equivalent propositions are equal),

 * propositional truncation
   (any type can be universally mapped into a prop in the same
   universe),

and no resizing axioms.

The K axiom is not used (the without-K option below). We also make
sure pattern matching corresponds to Martin-LΓΆf eliminators, using the
option exact-split. With the option safe we make sure that nothing
is postulated - any non-MLTT axiom has to be an explicit assumption
(argument to a function or a module).

\begin{code}

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

open import SpartanMLTT

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

module UF-Quotient
        (pt  : propositional-truncations-exist)
        (fe  : Fun-Ext)
        (pe  : Prop-Ext)
       where

\end{code}

We define when a relation is subsingleton (or proposition) valued,
reflexive, transitive or an equivalence.

What is noteworthy, for the purpose of explaining universes in Agda to
Dan, is that X is in a universe 𝓀, and the value of the relation is in
a universe π“₯, where 𝓀 and π“₯ are arbitrary.

(NB. The Agda library uses the word "Level" for universes, and then
what we write "𝓀 Μ‡" here is written "Set 𝓀". This is not good for
univalent mathematics, because the types in 𝓀 Μ‡ need not be sets, and
also because it places emphasis on levels rather than universes
themselves.)

Then, for example, the function is-prop-valued defined below takes
values in the least upper bound of 𝓀 and π“₯, which is denoted by 𝓀 βŠ” π“₯.

We first define the type of five functions and then define them, where
_β‰ˆ_ is a variable:

\begin{code}

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 _β‰ˆ_

\end{code}

Now, using an anonymous module with parameters (corresponding to a
section in Coq), we assume propositional truncations that stay in the
same universe, function extensionality for all universes, two
universes 𝓀 and π“₯, propositional truncation for the universe π“₯, a type
X : 𝓀 Μ‡, and an equivalence relation _β‰ˆ_ with values in π“₯ Μ‡.

\begin{code}

module quotient
       {𝓀 π“₯ : Universe}
       (X   : 𝓀 Μ‡ )
       (_β‰ˆ_ : X β†’ X β†’ π“₯ Μ‡ )
       (β‰ˆp  : is-prop-valued _β‰ˆ_)
       (β‰ˆr  : reflexive _β‰ˆ_)
       (β‰ˆs  : symmetric _β‰ˆ_)
       (β‰ˆt  : transitive _β‰ˆ_)
      where

 open PropositionalTruncation pt
 open ImageAndSurjection pt

\end{code}

Now, Ξ© π“₯ is the type of subsingletons, or (univalent) propositions, or
h-propositions, or mere propositions, in the universe π“₯, which lives
in the next universe π“₯ ⁺.

From the relation _β‰ˆ_ : X β†’ (X β†’ π“₯ Μ‡ ) we define a relation
X β†’ (X β†’ Ξ© π“₯), which of course is formally a function. We then take
the quotient X/β‰ˆ to be the image of this function.

Of course, it is for constructing the image that we need propositional
truncations.

\begin{code}

 equiv-rel : X β†’ (X β†’ Ξ© π“₯)
 equiv-rel x y = x β‰ˆ y , β‰ˆp x y

\end{code}

Then the quotient lives in the least upper bound of 𝓀 and π“₯ ⁺, where π“₯ ⁺
is the successor of the universe π“₯:

\begin{code}

 X/β‰ˆ : 𝓀 βŠ” (π“₯ ⁺) Μ‡
 X/β‰ˆ = image equiv-rel

 X/β‰ˆ-is-set : is-set X/β‰ˆ
 X/β‰ˆ-is-set = subsets-of-sets-are-sets (X β†’ Ξ© π“₯) _
                (powersets-are-sets'' fe fe pe)
                βˆ₯βˆ₯-is-prop

 Ξ· : X β†’ X/β‰ˆ
 Ξ· = corestriction equiv-rel

\end{code}

Then Ξ· is the universal solution to the problem of transforming
equivalence _β‰ˆ_ into equality _≑_ (in Agda the notation for the
identity type is _≑_ - we can't use _=_ because this is a reserved
symbol for definitional equality).

By construction, Ξ· is a surjection, of course:

\begin{code}

 Ξ·-surjection : is-surjection Ξ·
 Ξ·-surjection = corestriction-is-surjection equiv-rel

\end{code}

It is convenient to use the following induction principle for
reasoning about the image. Notice that the property we consider has
values in any universe 𝓦 we please:

\begin{code}

 quotient-induction : βˆ€ {𝓦} (P : X/β‰ˆ β†’ 𝓦 Μ‡ )
                    β†’ ((x' : X/β‰ˆ) β†’ is-prop (P x'))
                    β†’ ((x : X) β†’ P (Ξ· x))
                    β†’ (x' : X/β‰ˆ) β†’ P x'
 quotient-induction = surjection-induction Ξ· Ξ·-surjection

\end{code}

The first part of the universal property of Ξ· says that equivalent
points are mapped to equal points:

\begin{code}

 Ξ·-equiv-equal : {x y : X} β†’ x β‰ˆ y β†’ Ξ· x ≑ Ξ· y
 Ξ·-equiv-equal {x} {y} e =
   to-Ξ£-≑ (dfunext fe
          (Ξ» z β†’ to-Ξ£-≑ (pe (β‰ˆp x z) (β‰ˆp y z) (β‰ˆt y x z (β‰ˆs x y e)) (β‰ˆt x y z e) ,
                         being-prop-is-prop fe _ _)) ,
       βˆ₯βˆ₯-is-prop _ _)

\end{code}

We also need the fact that Ξ· reflects equality into equivalence:

\begin{code}

 Ξ·-equal-equiv : {x y : X} β†’ Ξ· x ≑ Ξ· y β†’ x β‰ˆ y
 Ξ·-equal-equiv {x} {y} p = equiv-rel-reflect (ap pr₁ p)
  where
   equiv-rel-reflect : equiv-rel x ≑ equiv-rel y β†’ x β‰ˆ y
   equiv-rel-reflect q = b (β‰ˆr y)
    where
     a : (y β‰ˆ y) ≑ (x β‰ˆ y)
     a = ap (Ξ» - β†’ pr₁(- y)) (q ⁻¹)
     b : (y β‰ˆ y) β†’ (x β‰ˆ y)
     b = Idtofun a

\end{code}

We are now ready to formulate and prove the universal property of the
quotient. What is noteworthy here, regarding universes, is that the
universal property says that we can eliminate into any set A of any
universe 𝓦.

                   Ξ·
              X ------> X/β‰ˆ
               \       .
                \     .
               f \   . f'
                  \ .
                   v
                   A

\begin{code}

 universal-property : βˆ€ {𝓦} (A : 𝓦 Μ‡ )
                    β†’ is-set A
                    β†’ (f : X β†’ A)
                    β†’ ({x x' : X} β†’ x β‰ˆ x' β†’ f x ≑ f x')
                    β†’ βˆƒ! f' κž‰( X/β‰ˆ β†’ A), f' ∘ Ξ· ≑ f
 universal-property {𝓦} A iss f pr = ic
  where
   Ο† : (x' : X/β‰ˆ) β†’ is-prop (Ξ£ a κž‰ A , βˆƒ x κž‰ X ,  (Ξ· x ≑ x') Γ— (f x ≑ a))
   Ο† = quotient-induction _ Ξ³ induction-step
     where
      induction-step : (y : X) β†’ is-prop (Ξ£ a κž‰ A , βˆƒ x κž‰ X ,  (Ξ· x ≑ Ξ· y) Γ— (f x ≑ a))
      induction-step x (a , d) (b , e) = to-Ξ£-≑ (p , βˆ₯βˆ₯-is-prop _ _)
       where
        h : (Ξ£ x' κž‰ X , (Ξ· x' ≑ Ξ· x) Γ— (f x' ≑ a))
          β†’ (Ξ£ y' κž‰ X , (Ξ· y' ≑ Ξ· x) Γ— (f y' ≑ b))
          β†’ a ≑ b
        h (x' , r , s) (y' , t , u) = s ⁻¹ βˆ™ pr (Ξ·-equal-equiv (r βˆ™ t ⁻¹)) βˆ™ u

        p : a ≑ b
        p = βˆ₯βˆ₯-rec iss (Ξ» Οƒ β†’ βˆ₯βˆ₯-rec iss (h Οƒ) e) d

      Ξ³ : (x' : X/β‰ˆ) β†’ is-prop (is-prop (Ξ£ a κž‰ A , βˆƒ x κž‰ X , (Ξ· x ≑ x') Γ— (f x ≑ a)))
      Ξ³ x' = being-prop-is-prop fe

   k : (x' : X/β‰ˆ) β†’ Ξ£ a κž‰ A , βˆƒ x κž‰ X , (Ξ· x ≑ x') Γ— (f x ≑ a)
   k = quotient-induction _ Ο† induction-step
    where
     induction-step : (y : X) β†’ Ξ£ a κž‰ A , βˆƒ x κž‰ X , (Ξ· x ≑ Ξ· y) Γ— (f x ≑ a)
     induction-step x = f x , ∣ x , refl , refl ∣

   f' : X/β‰ˆ β†’ A
   f' x' = pr₁(k x')

   r : f' ∘ Ξ· ≑ f
   r = dfunext fe h
    where
     g : (y : X) β†’ βˆƒ x κž‰ X , (Ξ· x ≑ Ξ· y) Γ— (f x ≑ f' (Ξ· y))
     g y = prβ‚‚(k(Ξ· y))

     j : (y : X) β†’ (Ξ£ x κž‰ X , (Ξ· x ≑ Ξ· y) Γ— (f x ≑ f' (Ξ· y))) β†’ f'(Ξ· y) ≑ f y
     j y (x , p , q) = q ⁻¹ βˆ™ pr (Ξ·-equal-equiv p)

     h : (y : X) β†’ f'(Ξ· y) ≑ f y
     h y = βˆ₯βˆ₯-rec iss (j y) (g y)

   c : (Οƒ : Ξ£ f'' κž‰ (X/β‰ˆ β†’ A), f'' ∘ Ξ· ≑ f) β†’ (f' , r) ≑ Οƒ
   c (f'' , s) = to-Ξ£-≑ (t , v)
    where
     w : βˆ€ x β†’ f'(Ξ· x) ≑ f''(Ξ· x)
     w = happly (r βˆ™ s ⁻¹)

     t : f' ≑ f''
     t = dfunext fe (quotient-induction _ (Ξ» _ β†’ iss) w)

     u : f'' ∘ Ξ· ≑ f
     u = transport (Ξ» - β†’ - ∘ Ξ· ≑ f) t r

     v : u ≑ s
     v = Ξ -is-set fe (Ξ» _ β†’ iss) u s

   ic : βˆƒ! f' κž‰ (X/β‰ˆ β†’ A), f' ∘ Ξ· ≑ f
   ic = (f' , r) , c

\end{code}

Added 11th February 2021. We now repackage the above for convenient
use:

\begin{code}

module _ {𝓀 π“₯ : Universe} where

 open quotient
 open ImageAndSurjection pt

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

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

 _/_ : (X : 𝓀 Μ‡ ) β†’ EqRel X β†’ 𝓀 βŠ” (π“₯ ⁺) Μ‡
 X / (_β‰ˆ_ , p , r , s , t) = X/β‰ˆ X _β‰ˆ_ p r s t

 module _ {X : 𝓀 Μ‡ }
          ((_β‰ˆ_ , β‰ˆp , β‰ˆr , β‰ˆs , β‰ˆt) : EqRel X)
        where

  private
   ≋ : EqRel X
   ≋ = (_β‰ˆ_ , β‰ˆp , β‰ˆr , β‰ˆs , β‰ˆt)

  quotient-is-set : is-set (X / ≋)
  quotient-is-set = X/β‰ˆ-is-set _ _β‰ˆ_ β‰ˆp β‰ˆr β‰ˆs β‰ˆt

  Ξ·/ : X β†’ X / ≋
  Ξ·/ = Ξ· X _β‰ˆ_ β‰ˆp β‰ˆr β‰ˆs β‰ˆt

  Ξ·/-is-surjection : is-surjection Ξ·/
  Ξ·/-is-surjection = Ξ·-surjection X _β‰ˆ_ β‰ˆp β‰ˆr β‰ˆs β‰ˆt

  /-induction : βˆ€ {𝓦} (P : X / ≋ β†’ 𝓦 Μ‡ )
              β†’ ((x' : X / ≋) β†’ is-prop (P x'))
              β†’ ((x : X) β†’ P (Ξ·/ x))
              β†’ (x' : X / ≋) β†’ P x'
  /-induction = surjection-induction Ξ·/ Ξ·/-is-surjection

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

  Ξ·/-identifies-related-points : identifies-related-points Ξ·/
  Ξ·/-identifies-related-points = Ξ·-equiv-equal X _β‰ˆ_ β‰ˆp β‰ˆr β‰ˆs β‰ˆt

  Ξ·/-relates-identified-points : {x y : X}
                               β†’ Ξ·/ x ≑ Ξ·/ y
                               β†’ x β‰ˆ y
  Ξ·/-relates-identified-points = Ξ·-equal-equiv X _β‰ˆ_ β‰ˆp β‰ˆr β‰ˆs β‰ˆt

  module _ {𝓦 : Universe}
           {A : 𝓦 Μ‡ }
         where

   abstract
    universal-property/ : is-set A
                        β†’ (f : X β†’ A)
                        β†’ identifies-related-points f
                        β†’ βˆƒ! f' κž‰ (X / ≋ β†’ A), f' ∘ Ξ·/ ≑ f
    universal-property/ = universal-property X _β‰ˆ_ β‰ˆp β‰ˆr β‰ˆs β‰ˆt A

    mediating-map/ : is-set A
                   β†’ (f : X β†’ A)
                   β†’ identifies-related-points f
                   β†’ X / ≋ β†’ A
    mediating-map/ i f p = pr₁ (center (universal-property/ i f p))

    universality-triangle/≑ : (i : is-set A) (f : X β†’ A)
                              (p : identifies-related-points f)
                            β†’ mediating-map/ i f p ∘ Ξ·/ ≑ f
    universality-triangle/≑ i f p = prβ‚‚ (center (universal-property/ i f p))


    universality-triangle/ : (i : is-set A) (f : X β†’ A)
                             (p : identifies-related-points f)
                           β†’ mediating-map/ i f p ∘ Ξ·/ ∼ f
    universality-triangle/ i f p = happly (universality-triangle/≑ i f p)


    at-most-one-mediating-map/≑ : is-set A
                               β†’ (g h : X / ≋ β†’ A)
                               β†’ g ∘ Ξ·/ ≑ h ∘ Ξ·/
                               β†’ g ≑ h
    at-most-one-mediating-map/≑ i g h p = q ⁻¹ βˆ™ r
     where
      f : X β†’ A
      f = g ∘ η/

      j : identifies-related-points f
      j e = ap g (Ξ·/-identifies-related-points e)

      q : mediating-map/ i f j ≑ g
      q = witness-uniqueness (Ξ» f' β†’ f' ∘ Ξ·/ ≑ f)
           (universal-property/ i f j)
           (mediating-map/ i f j) g (universality-triangle/≑ i f j)
           refl

      r : mediating-map/ i f j ≑ h
      r = witness-uniqueness (Ξ» f' β†’ f' ∘ Ξ·/ ≑ f)
           (universal-property/ i f j)
           (mediating-map/ i f j) h (universality-triangle/≑ i f j)
           (p ⁻¹)

    at-most-one-mediating-map/ : is-set A
                               β†’ (g h : X / ≋ β†’ A)
                               β†’ g ∘ Ξ·/ ∼ h ∘ Ξ·/
                               β†’ g ∼ h
    at-most-one-mediating-map/ i g h p = happly (at-most-one-mediating-map/≑ i g h
                                                   (dfunext fe p))
\end{code}

Extending unary and binary operations to the quotient:

\begin{code}

  extension/ : (f : X β†’ X / ≋)
             β†’ identifies-related-points f
             β†’ (X / ≋ β†’ X / ≋)
  extension/ = mediating-map/ quotient-is-set

  extension-triangle/ : (f : X β†’ X / ≋)
                        (i : identifies-related-points f)
                      β†’ extension/ f i ∘ Ξ·/ ∼ f
  extension-triangle/ = universality-triangle/ quotient-is-set

  module _ (f : X β†’ X)
           (p : {x y : X} β†’ x β‰ˆ y β†’ f x β‰ˆ f y)
         where

   abstract
    private
      Ο€ : identifies-related-points (Ξ·/ ∘ f)
      Ο€ e = Ξ·/-identifies-related-points (p e)

   extension₁/ : X / ≋ β†’ X / ≋
   extension₁/ = extension/ (Ξ·/ ∘ f) Ο€

   naturality/ : extension₁/ ∘ Ξ·/ ∼ Ξ·/ ∘ f
   naturality/ = universality-triangle/ quotient-is-set (Ξ·/ ∘ f) Ο€

  module _ (f : X β†’ X β†’ X)
           (p : {x y x' y' : X} β†’ x β‰ˆ x' β†’ y β‰ˆ y' β†’ f x y β‰ˆ f x' y')
         where

   abstract
    private
     Ο€ : (x : X) β†’ identifies-related-points (Ξ·/ ∘ f x)
     Ο€ x {y} {y'} e = Ξ·/-identifies-related-points (p {x} {y} {x} {y'} (β‰ˆr x) e)

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

     f₁ : X β†’ X / ≋ β†’ X / ≋
     f₁ x = extension₁/ (f x) (p' x)

     n/ : (x : X) β†’ f₁ x ∘ Ξ·/ ∼ Ξ·/ ∘ f x
     n/ x = naturality/ (f x) (p' x)

     Ξ΄ : {x x' : X} β†’ x β‰ˆ x' β†’ (y : X) β†’ f₁ x (Ξ·/ y) ≑ f₁ x' (Ξ·/ y)
     Ξ΄ {x} {x'} e y =
       f₁ x (Ξ·/ y)   β‰‘βŸ¨ naturality/ (f x) (p' x) y ⟩
       Ξ·/ (f x y)    β‰‘βŸ¨ Ξ·/-identifies-related-points (p e (β‰ˆr y)) ⟩
       Ξ·/ (f x' y)   β‰‘βŸ¨ (naturality/ (f x') (p' x') y)⁻¹ ⟩
       f₁ x' (Ξ·/ y)  ∎

     ρ : (b : X / ≋) {x x' : X} β†’ x β‰ˆ x' β†’ f₁ x b ≑ f₁ x' b
     ρ b {x} {x'} e = /-induction (Ξ» b β†’ f₁ x b ≑ f₁ x' b)
                        (Ξ» y β†’ quotient-is-set) (Ξ΄ e) b

     fβ‚‚ : X / ≋ β†’ X / ≋ β†’ X / ≋
     fβ‚‚ d e = extension/ (Ξ» x β†’ f₁ x e) (ρ e) d

   extensionβ‚‚/ : X / ≋ β†’ X / ≋ β†’ X / ≋
   extensionβ‚‚/ = fβ‚‚

   abstract
    naturalityβ‚‚/ : (x y : X) β†’ fβ‚‚ (Ξ·/ x) (Ξ·/ y) ≑ Ξ·/ (f x y)
    naturalityβ‚‚/ x y =
     fβ‚‚ (Ξ·/ x) (Ξ·/ y) β‰‘βŸ¨ extension-triangle/ (Ξ» x β†’ f₁ x (Ξ·/ y)) (ρ (Ξ·/ y)) x ⟩
     f₁ x (Ξ·/ y)      β‰‘βŸ¨ naturality/ (f x) (p (β‰ˆr x)) y ⟩
     η/ (f x y)       ∎

\end{code}

Without the above abstract declarations, the use of naturalityβ‚‚/ takes
for ever in the module FreeGroup.lagda.

\begin{code}

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/ ≋ (quotient-is-set ≋') (Ξ·/ ≋') i

  f' : X / ≋' β†’ X / ≋
  f' = mediating-map/ ≋' (quotient-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/ ≋' (quotient-is-set ≋) (Ξ·/ ≋) i' x)
    II = universality-triangle/ ≋ (quotient-is-set ≋') (Ξ·/ ≋') i x

  α : f ∘ f' ∼ id
  Ξ± = /-induction ≋' (Ξ» u β†’ f (f' u) ≑ u) (Ξ» u β†’ quotient-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/ ≋ (quotient-is-set ≋') (Ξ·/ ≋') i x)
    II = universality-triangle/ ≋' (quotient-is-set ≋) (Ξ·/ ≋) i' x

  α' : f' ∘ f ∼ id
  Ξ±' = /-induction ≋ (Ξ» u β†’ f' (f u) ≑ u) (Ξ» u β†’ quotient-is-set ≋) a'


  Ξ³ : (X / ≋) ≃ (X / ≋')
  Ξ³ = qinveq f (f' , Ξ±' , Ξ±)

\end{code}