The uniqueness of set quotients

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Daniel Gratzer, Elisabeth Stenholm, Julian KG, fernabnor and louismntnu.

Created on 2022-02-17.
Last modified on 2024-02-06.

module foundation.uniqueness-set-quotients where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.reflecting-maps-equivalence-relations
open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.universal-property-equivalences
open import foundation.universal-property-set-quotients
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.contractible-types
open import foundation-core.equivalence-relations
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.precomposition-functions

Idea

The universal property of set quotients implies that set quotients are uniquely unique.

Properties

Uniqueness of set quotients

precomp-comp-Set-Quotient :
  {l1 l2 l3 l4 l5 : Level} {A : UU l1} (R : equivalence-relation l2 A)
  (B : Set l3) (f : reflecting-map-equivalence-relation R (type-Set B))
  (C : Set l4) (g : hom-Set B C)
  (D : Set l5) (h : hom-Set C D) →
  ( precomp-Set-Quotient R B f D (h ∘ g)) ＝
  ( precomp-Set-Quotient R C (precomp-Set-Quotient R B f C g) D h)
precomp-comp-Set-Quotient R B f C g D h =
  eq-htpy-reflecting-map-equivalence-relation R D
    ( precomp-Set-Quotient R B f D (h ∘ g))
    ( precomp-Set-Quotient R C (precomp-Set-Quotient R B f C g) D h)
    ( refl-htpy)

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} (R : equivalence-relation l2 A)
  (B : Set l3) (f : reflecting-map-equivalence-relation R (type-Set B))
  (C : Set l4) (g : reflecting-map-equivalence-relation R (type-Set C))
  {h : type-Set B → type-Set C}
  (H :
    (h ∘ map-reflecting-map-equivalence-relation R f) ~
    map-reflecting-map-equivalence-relation R g)
  where

  map-inv-is-equiv-is-set-quotient-is-set-quotient :
    is-set-quotient R B f →
    is-set-quotient R C g →
    type-Set C → type-Set B
  map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug =
    map-universal-property-set-quotient-is-set-quotient R C g Ug B f

  is-section-map-inv-is-equiv-is-set-quotient-is-set-quotient :
    ( Uf : is-set-quotient R B f) →
    ( Ug : is-set-quotient R C g) →
    ( h ∘ map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug) ~ id
  is-section-map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug =
    htpy-eq
      ( is-injective-is-equiv
      ( Ug C)
      { h ∘ map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug}
      { id}
      ( ( precomp-comp-Set-Quotient R C g B
          ( map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug)
          ( C)
          ( h)) ∙
        ( ( ap
            ( λ t → precomp-Set-Quotient R B t C h)
            ( eq-htpy-reflecting-map-equivalence-relation R B
              ( precomp-Set-Quotient R C g B
                ( map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug))
              ( f)
              ( triangle-universal-property-set-quotient-is-set-quotient
                R C g Ug B f))) ∙
          ( ( eq-htpy-reflecting-map-equivalence-relation R C
              ( precomp-Set-Quotient R B f C h) g H) ∙
            ( inv (precomp-id-Set-Quotient R C g))))))

  is-retraction-map-inv-is-equiv-is-set-quotient-is-set-quotient :
    ( Uf : is-set-quotient R B f) →
    ( Ug : is-set-quotient R C g) →
    ( map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug ∘ h) ~ id
  is-retraction-map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug =
    htpy-eq
      ( is-injective-is-equiv
      ( Uf B)
      { map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug ∘ h}
      { id}
      ( ( precomp-comp-Set-Quotient R B f C h B
          ( map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug)) ∙
        ( ( ap
            ( λ t →
              precomp-Set-Quotient R C t B
                ( map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug))
            ( eq-htpy-reflecting-map-equivalence-relation R C
              ( precomp-Set-Quotient R B f C h)
              ( g)
              ( H))) ∙
          ( ( eq-htpy-reflecting-map-equivalence-relation R B
              ( precomp-Set-Quotient R C g B
                ( map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug))
              ( f)
              ( triangle-universal-property-set-quotient-is-set-quotient
                R C g Ug B f)) ∙
            ( inv (precomp-id-Set-Quotient R B f))))))

  is-equiv-is-set-quotient-is-set-quotient :
    is-set-quotient R B f →
    is-set-quotient R C g →
    is-equiv h
  is-equiv-is-set-quotient-is-set-quotient Uf Ug =
    is-equiv-is-invertible
      ( map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug)
      ( is-section-map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug)
      ( is-retraction-map-inv-is-equiv-is-set-quotient-is-set-quotient Uf Ug)

  is-set-quotient-is-set-quotient-is-equiv :
    is-equiv h → is-set-quotient R B f → is-set-quotient R C g
  is-set-quotient-is-set-quotient-is-equiv E Uf {l} X =
    is-equiv-left-map-triangle
      ( precomp-Set-Quotient R C g X)
      ( precomp-Set-Quotient R B f X)
      ( precomp h (type-Set X))
      ( λ k →
        eq-htpy-reflecting-map-equivalence-relation R X
          ( precomp-Set-Quotient R C g X k)
          ( precomp-Set-Quotient R B f X (k ∘ h))
          ( inv-htpy (k ·l H)))
      ( is-equiv-precomp-is-equiv h E (type-Set X))
      ( Uf X)

  is-set-quotient-is-equiv-is-set-quotient :
    is-set-quotient R C g → is-equiv h → is-set-quotient R B f
  is-set-quotient-is-equiv-is-set-quotient Ug E {l} X =
    is-equiv-right-map-triangle
      ( precomp-Set-Quotient R C g X)
      ( precomp-Set-Quotient R B f X)
      ( precomp h (type-Set X))
      ( λ k →
        eq-htpy-reflecting-map-equivalence-relation R X
          ( precomp-Set-Quotient R C g X k)
          ( precomp-Set-Quotient R B f X (k ∘ h))
          ( inv-htpy (k ·l H)))
      ( Ug X)
      ( is-equiv-precomp-is-equiv h E (type-Set X))

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} (R : equivalence-relation l2 A)
  (B : Set l3) (f : reflecting-map-equivalence-relation R (type-Set B))
  (Uf : is-set-quotient R B f)
  (C : Set l4) (g : reflecting-map-equivalence-relation R (type-Set C))
  (Ug : is-set-quotient R C g)
  where

  uniqueness-set-quotient :
    is-contr
      ( Σ ( type-Set B ≃ type-Set C)
          ( λ e →
            ( map-equiv e ∘ map-reflecting-map-equivalence-relation R f) ~
            ( map-reflecting-map-equivalence-relation R g)))
  uniqueness-set-quotient =
    is-torsorial-Eq-subtype
      ( universal-property-set-quotient-is-set-quotient R B f Uf C g)
      ( is-property-is-equiv)
      ( map-universal-property-set-quotient-is-set-quotient R B f Uf C g)
      ( triangle-universal-property-set-quotient-is-set-quotient R B f Uf C g)
      ( is-equiv-is-set-quotient-is-set-quotient R B f C g
        ( triangle-universal-property-set-quotient-is-set-quotient
          R B f Uf C g)
        ( Uf)
        ( Ug))

  equiv-uniqueness-set-quotient : type-Set B ≃ type-Set C
  equiv-uniqueness-set-quotient =
    pr1 (center uniqueness-set-quotient)

  map-equiv-uniqueness-set-quotient : type-Set B → type-Set C
  map-equiv-uniqueness-set-quotient = map-equiv equiv-uniqueness-set-quotient

  triangle-uniqueness-set-quotient :
    ( map-equiv-uniqueness-set-quotient ∘
      map-reflecting-map-equivalence-relation R f) ~
    ( map-reflecting-map-equivalence-relation R g)
  triangle-uniqueness-set-quotient =
    pr2 (center uniqueness-set-quotient)

Recent changes