Agda UALib ↑

MartΓ­n EscardΓ³ 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes, which are available online from the following links.

html lecture notes

Source code repository


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

module MGS-Quotient where

open import MGS-Unique-Existence        public
open import MGS-Subsingleton-Truncation public

is-subsingleton-valued
 reflexive
 symmetric
 transitive
 is-equivalence-relation :

 {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡

is-subsingleton-valued  _β‰ˆ_ = βˆ€ x y β†’ is-subsingleton (x β‰ˆ y)
reflexive               _β‰ˆ_ = βˆ€ x β†’ x β‰ˆ x
symmetric               _β‰ˆ_ = βˆ€ x y β†’ x β‰ˆ y β†’ y β‰ˆ x
transitive              _β‰ˆ_ = βˆ€ x y z β†’ x β‰ˆ y β†’ y β‰ˆ z β†’ x β‰ˆ z

is-equivalence-relation _β‰ˆ_ = is-subsingleton-valued _β‰ˆ_
                            Γ— reflexive _β‰ˆ_
                            Γ— symmetric _β‰ˆ_
                            Γ— transitive _β‰ˆ_

module quotient
       {𝓀 π“₯ : Universe}
       (pt  : subsingleton-truncations-exist)
       (hfe : global-hfunext)
       (pe  : propext π“₯)
       (X   : 𝓀 Μ‡ )
       (_β‰ˆ_ : X β†’ X β†’ π“₯ Μ‡ )
       (β‰ˆp  : is-subsingleton-valued _β‰ˆ_)
       (β‰ˆr  : reflexive _β‰ˆ_)
       (β‰ˆs  : symmetric _β‰ˆ_)
       (β‰ˆt  : transitive _β‰ˆ_)
      where

 open basic-truncation-development pt hfe

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

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

 X/β‰ˆ-is-set : is-set X/β‰ˆ
 X/β‰ˆ-is-set = subsets-of-sets-are-sets (X β†’ Ξ© π“₯) _
               (powersets-are-sets (dfunext-gives-hfunext hunapply) hunapply pe)
               (Ξ» _ β†’ βˆƒ-is-subsingleton)

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

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

 Ξ·-induction : (P : X/β‰ˆ β†’ 𝓦 Μ‡ )
             β†’ ((x' : X/β‰ˆ) β†’ is-subsingleton (P x'))
             β†’ ((x : X) β†’ P (Ξ· x))
             β†’ (x' : X/β‰ˆ) β†’ P x'

 Ξ·-induction = surjection-induction Ξ· Ξ·-surjection

 Ξ·-equiv-equal : {x y : X} β†’ x β‰ˆ y β†’ Ξ· x ≑ Ξ· y
 Ξ·-equiv-equal {x} {y} e =
  to-subtype-≑
    (Ξ» _ β†’ βˆƒ-is-subsingleton)
    (hunapply (Ξ» z β†’ to-subtype-≑
                        (Ξ» _ β†’ being-subsingleton-is-subsingleton hunapply)
                        (pe (β‰ˆp x z) (β‰ˆp y z) (β‰ˆt y x z (β‰ˆs x y e)) (β‰ˆt x y z e))))

 Ξ·-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 = Id→fun a

 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 i f Ο„ = e
  where
   G : X/β‰ˆ β†’ π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓦 Μ‡
   G x' = Ξ£ a κž‰ A , βˆƒ x κž‰ X , (Ξ· x ≑ x') Γ— (f x ≑ a)

   Ο† : (x' : X/β‰ˆ) β†’ is-subsingleton (G x')
   Ο† = Ξ·-induction _ Ξ³ induction-step
    where
     induction-step : (y : X) β†’ is-subsingleton (G (Ξ· y))
     induction-step x (a , d) (b , e) = to-subtype-≑ (Ξ» _ β†’ βˆƒ-is-subsingleton) p
      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) = a    β‰‘βŸ¨ s ⁻¹                         ⟩
                                     f x' β‰‘βŸ¨ Ο„ (Ξ·-equal-equiv (r βˆ™ t ⁻¹)) ⟩
                                     f y' β‰‘βŸ¨ u                            ⟩
                                     b    ∎

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

     Ξ³ : (x' : X/β‰ˆ) β†’ is-subsingleton (is-subsingleton (G x'))
     Ξ³ x' = being-subsingleton-is-subsingleton hunapply

   k : (x' : X/β‰ˆ) β†’ G x'
   k = Ξ·-induction _ Ο† induction-step
    where
     induction-step : (y : X) β†’ G (Ξ· y)
     induction-step x = f x , ∣ x , refl (η x) , refl (f x) ∣

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

   r : f' ∘ Ξ· ≑ f
   r = hunapply 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) = f' (Ξ· y) β‰‘βŸ¨ q ⁻¹                ⟩
                       f x      β‰‘βŸ¨ Ο„ (Ξ·-equal-equiv p) ⟩
                       f y      ∎

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

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

     t : f' ≑ f''
     t = hunapply (Ξ·-induction _ (Ξ» x' β†’ i (f' x') (f'' x')) w)

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