Equivalence classes

module foundation.equivalence-classes where
Imports
open import foundation.effective-maps-equivalence-relations
open import foundation.existential-quantification
open import foundation.functoriality-propositional-truncation
open import foundation.inhabited-subtypes
open import foundation.locally-small-types
open import foundation.propositional-truncations
open import foundation.reflecting-maps-equivalence-relations
open import foundation.slice
open import foundation.small-types
open import foundation.subtypes
open import foundation.surjective-maps
open import foundation.universal-property-image

open import foundation-core.cartesian-product-types
open import foundation-core.contractible-types
open import foundation-core.dependent-pair-types
open import foundation-core.embeddings
open import foundation-core.equivalence-relations
open import foundation-core.equivalences
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.fundamental-theorem-of-identity-types
open import foundation-core.identity-types
open import foundation-core.logical-equivalences
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.subtype-identity-principle
open import foundation-core.universe-levels

Idea

An equivalence class of an equivalence relation R on A is a subtype of A that is merely equivalent to a subtype of the form R x. The type of equivalence classes of an equivalence relation satisfies the universal property of the set quotient.

Definition

The condition on subtypes of A of being an equivalence class

module _
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A)
  where

  is-equivalence-class-Prop : subtype l2 A  Prop (l1  l2)
  is-equivalence-class-Prop P =
    ∃-Prop A  x  has-same-elements-subtype P (prop-Eq-Rel R x))

  is-equivalence-class : subtype l2 A  UU (l1  l2)
  is-equivalence-class P = type-Prop (is-equivalence-class-Prop P)

  is-prop-is-equivalence-class :
    (P : subtype l2 A)  is-prop (is-equivalence-class P)
  is-prop-is-equivalence-class P =
    is-prop-type-Prop (is-equivalence-class-Prop P)

The condition on inhabited subtypes of A of being an equivalence class

  is-equivalence-class-inhabited-subtype-Eq-Rel :
    subtype (l1  l2) (inhabited-subtype l2 A)
  is-equivalence-class-inhabited-subtype-Eq-Rel Q =
    is-equivalence-class-Prop (subtype-inhabited-subtype Q)

The type of equivalence classes

  equivalence-class : UU (l1  lsuc l2)
  equivalence-class = type-subtype is-equivalence-class-Prop

  class : A  equivalence-class
  pr1 (class x) = prop-Eq-Rel R x
  pr2 (class x) =
    unit-trunc-Prop (pair x (refl-has-same-elements-subtype (prop-Eq-Rel R x)))

  emb-equivalence-class : equivalence-class  subtype l2 A
  emb-equivalence-class = emb-subtype is-equivalence-class-Prop

  subtype-equivalence-class : equivalence-class  subtype l2 A
  subtype-equivalence-class = inclusion-subtype is-equivalence-class-Prop

  is-equivalence-class-equivalence-class :
    (C : equivalence-class)  is-equivalence-class (subtype-equivalence-class C)
  is-equivalence-class-equivalence-class =
    is-in-subtype-inclusion-subtype is-equivalence-class-Prop

  is-inhabited-subtype-equivalence-class :
    (C : equivalence-class)  is-inhabited-subtype (subtype-equivalence-class C)
  is-inhabited-subtype-equivalence-class (pair Q H) =
    apply-universal-property-trunc-Prop H
      ( is-inhabited-subtype-Prop (subtype-equivalence-class (pair Q H)))
      ( λ u 
        unit-trunc-Prop
          ( pair
            ( pr1 u)
            ( backward-implication (pr2 u (pr1 u)) (refl-Eq-Rel R))))

  inhabited-subtype-equivalence-class :
    (C : equivalence-class)  inhabited-subtype l2 A
  pr1 (inhabited-subtype-equivalence-class C) = subtype-equivalence-class C
  pr2 (inhabited-subtype-equivalence-class C) =
    is-inhabited-subtype-equivalence-class C

  is-in-equivalence-class : equivalence-class  (A  UU l2)
  is-in-equivalence-class P x = type-Prop (subtype-equivalence-class P x)

  abstract
    is-prop-is-in-equivalence-class :
      (x : equivalence-class) (a : A) 
      is-prop (is-in-equivalence-class x a)
    is-prop-is-in-equivalence-class P x =
      is-prop-type-Prop (subtype-equivalence-class P x)

  is-in-equivalence-class-Prop : equivalence-class  (A  Prop l2)
  pr1 (is-in-equivalence-class-Prop P x) = is-in-equivalence-class P x
  pr2 (is-in-equivalence-class-Prop P x) = is-prop-is-in-equivalence-class P x

  abstract
    is-set-equivalence-class : is-set equivalence-class
    is-set-equivalence-class =
      is-set-type-subtype is-equivalence-class-Prop is-set-subtype

  equivalence-class-Set : Set (l1  lsuc l2)
  pr1 equivalence-class-Set = equivalence-class
  pr2 equivalence-class-Set = is-set-equivalence-class

  unit-im-equivalence-class :
    hom-slice (prop-Eq-Rel R) subtype-equivalence-class
  pr1 unit-im-equivalence-class = class
  pr2 unit-im-equivalence-class x = refl

  is-surjective-class : is-surjective class
  is-surjective-class C =
    map-trunc-Prop
      ( tot
        ( λ x p 
          inv
            ( eq-type-subtype
              ( is-equivalence-class-Prop)
              ( eq-has-same-elements-subtype (pr1 C) (prop-Eq-Rel R x) p))))
      ( pr2 C)

  is-image-equivalence-class :
    {l : Level} 
    is-image l (prop-Eq-Rel R) emb-equivalence-class unit-im-equivalence-class
  is-image-equivalence-class =
    is-image-is-surjective
      ( prop-Eq-Rel R)
      ( emb-equivalence-class)
      ( unit-im-equivalence-class)
      ( is-surjective-class)

Properties

Characterization of equality of equivalence classes

Equivalence classes are equal if they contain the same elements

module _
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A)
  where

  has-same-elements-equivalence-class :
    (C D : equivalence-class R)  UU (l1  l2)
  has-same-elements-equivalence-class C D =
    has-same-elements-subtype
      ( subtype-equivalence-class R C)
      ( subtype-equivalence-class R D)

  refl-has-same-elements-equivalence-class :
    (C : equivalence-class R)  has-same-elements-equivalence-class C C
  refl-has-same-elements-equivalence-class C =
    refl-has-same-elements-subtype (subtype-equivalence-class R C)

  is-contr-total-has-same-elements-equivalence-class :
    (C : equivalence-class R) 
    is-contr (Σ (equivalence-class R) (has-same-elements-equivalence-class C))
  is-contr-total-has-same-elements-equivalence-class C =
    is-contr-total-Eq-subtype
      ( is-contr-total-has-same-elements-subtype
        ( subtype-equivalence-class R C))
      ( is-prop-is-equivalence-class R)
      ( subtype-equivalence-class R C)
      ( refl-has-same-elements-equivalence-class C)
      ( is-equivalence-class-equivalence-class R C)

  has-same-elements-eq-equivalence-class :
    (C D : equivalence-class R)  (C  D) 
    has-same-elements-equivalence-class C D
  has-same-elements-eq-equivalence-class C .C refl =
    refl-has-same-elements-subtype (subtype-equivalence-class R C)

  is-equiv-has-same-elements-eq-equivalence-class :
    (C D : equivalence-class R) 
    is-equiv (has-same-elements-eq-equivalence-class C D)
  is-equiv-has-same-elements-eq-equivalence-class C =
    fundamental-theorem-id
      ( is-contr-total-has-same-elements-equivalence-class C)
      ( has-same-elements-eq-equivalence-class C)

  extensionality-equivalence-class :
    (C D : equivalence-class R) 
    (C  D)  has-same-elements-equivalence-class C D
  pr1 (extensionality-equivalence-class C D) =
    has-same-elements-eq-equivalence-class C D
  pr2 (extensionality-equivalence-class C D) =
    is-equiv-has-same-elements-eq-equivalence-class C D

  eq-has-same-elements-equivalence-class :
    (C D : equivalence-class R) 
    has-same-elements-equivalence-class C D  C  D
  eq-has-same-elements-equivalence-class C D =
    map-inv-equiv (extensionality-equivalence-class C D)

Equivalence classes are equal if there exists an element contained in both

module _
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A)
  where

  share-common-element-equivalence-class-Prop :
    (C D : equivalence-class R)  Prop (l1  l2)
  share-common-element-equivalence-class-Prop C D =
    ∃-Prop A
      ( λ x  is-in-equivalence-class R C x × is-in-equivalence-class R D x)

  share-common-element-equivalence-class :
    (C D : equivalence-class R)  UU (l1  l2)
  share-common-element-equivalence-class C D =
    type-Prop (share-common-element-equivalence-class-Prop C D)

  abstract
    eq-share-common-element-equivalence-class :
      (C D : equivalence-class R) 
      share-common-element-equivalence-class C D  C  D
    eq-share-common-element-equivalence-class C D H =
      apply-three-times-universal-property-trunc-Prop
        ( H)
        ( is-equivalence-class-equivalence-class R C)
        ( is-equivalence-class-equivalence-class R D)
        ( Id-Prop (equivalence-class-Set R) C D)
        ( λ (a , c , d) (v , φ) (w , ψ) 
          eq-has-same-elements-equivalence-class R C D
            ( λ x 
              logical-equivalence-reasoning
                is-in-equivalence-class R C x
                   sim-Eq-Rel R v x
                    by φ x
                   sim-Eq-Rel R a x
                    by iff-trans-Eq-Rel R
                        ( symm-Eq-Rel R (forward-implication (φ a) c))
                   sim-Eq-Rel R w x
                    by iff-trans-Eq-Rel R (forward-implication (ψ a) d)
                   is-in-equivalence-class R D x
                    by inv-iff (ψ x)))

  eq-class-equivalence-class :
    (C : equivalence-class R) {a : A} 
    is-in-equivalence-class R C a  class R a  C
  eq-class-equivalence-class C {a} H =
    eq-share-common-element-equivalence-class
      ( class R a)
      ( C)
      ( unit-trunc-Prop (pair a (pair (refl-Eq-Rel R) H)))

The type of equivalence classes containing a fixed element a : A is contractible

module _
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A) (a : A)
  where

  center-total-is-in-equivalence-class :
    Σ (equivalence-class R)  P  is-in-equivalence-class R P a)
  pr1 center-total-is-in-equivalence-class = class R a
  pr2 center-total-is-in-equivalence-class = refl-Eq-Rel R

  contraction-total-is-in-equivalence-class :
    ( t :
      Σ ( equivalence-class R)
        ( λ C  is-in-equivalence-class R C a)) 
    center-total-is-in-equivalence-class  t
  contraction-total-is-in-equivalence-class (pair C H) =
    eq-type-subtype
      ( λ D  is-in-equivalence-class-Prop R D a)
      ( eq-class-equivalence-class R C H)

  is-contr-total-is-in-equivalence-class :
    is-contr
      ( Σ ( equivalence-class R)
          ( λ P  is-in-equivalence-class R P a))
  pr1 is-contr-total-is-in-equivalence-class =
    center-total-is-in-equivalence-class
  pr2 is-contr-total-is-in-equivalence-class =
    contraction-total-is-in-equivalence-class

  is-in-equivalence-class-eq-equivalence-class :
    (q : equivalence-class R)  class R a  q 
    is-in-equivalence-class R q a
  is-in-equivalence-class-eq-equivalence-class .(class R a) refl =
    refl-Eq-Rel R

  abstract
    is-equiv-is-in-equivalence-class-eq-equivalence-class :
      (q : equivalence-class R) 
      is-equiv (is-in-equivalence-class-eq-equivalence-class q)
    is-equiv-is-in-equivalence-class-eq-equivalence-class =
      fundamental-theorem-id
        ( is-contr-total-is-in-equivalence-class)
        ( is-in-equivalence-class-eq-equivalence-class)

The map class : A → equivalence-class R is an effective quotient map

module _
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A)
  where

  abstract
    effective-quotient' :
      (a : A) (q : equivalence-class R) 
      ( class R a  q) 
      ( is-in-equivalence-class R q a)
    pr1 (effective-quotient' a q) =
      is-in-equivalence-class-eq-equivalence-class R a q
    pr2 (effective-quotient' a q) =
      is-equiv-is-in-equivalence-class-eq-equivalence-class R a q

  abstract
    eq-effective-quotient' :
      (a : A) (q : equivalence-class R)  is-in-equivalence-class R q a 
      class R a  q
    eq-effective-quotient' a q =
      map-inv-is-equiv
        ( is-equiv-is-in-equivalence-class-eq-equivalence-class R a q)

  abstract
    is-effective-class :
      is-effective R (class R)
    is-effective-class x y =
      ( equiv-symm-Eq-Rel R) ∘e ( effective-quotient' x (class R y))

  abstract
    apply-effectiveness-class :
      {x y : A}  class R x  class R y  sim-Eq-Rel R x y
    apply-effectiveness-class {x} {y} =
      map-equiv (is-effective-class x y)

  abstract
    apply-effectiveness-class' :
      {x y : A}  sim-Eq-Rel R x y  class R x  class R y
    apply-effectiveness-class' {x} {y} =
      map-inv-equiv (is-effective-class x y)

The map class into the type of equivalence classes is surjective and effective

module _
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A)
  where

  is-surjective-and-effective-class :
    is-surjective-and-effective R (class R)
  pr1 is-surjective-and-effective-class =
    is-surjective-class R
  pr2 is-surjective-and-effective-class =
    is-effective-class R

The map class into the type of equivalence classes is a reflecting map

module _
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A)
  where

  quotient-reflecting-map-equivalence-class :
    reflecting-map-Eq-Rel R (equivalence-class R)
  pr1 quotient-reflecting-map-equivalence-class =
    class R
  pr2 quotient-reflecting-map-equivalence-class =
    apply-effectiveness-class' R
module _
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A)
  where

  transitive-is-in-equivalence-class :
    (P : equivalence-class R) (a b : A) 
    is-in-equivalence-class R P a  sim-Eq-Rel R a b 
    is-in-equivalence-class R P b
  transitive-is-in-equivalence-class P a b p r =
    apply-universal-property-trunc-Prop
      ( is-equivalence-class-equivalence-class R P)
      ( subtype-equivalence-class R P b)
      ( λ (pair x H) 
        backward-implication
          ( H b)
          ( trans-Eq-Rel R (forward-implication (H a) p) r))

The type of equivalence classes is locally small

module _
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A)
  where

  is-locally-small-equivalence-class :
    is-locally-small (l1  l2) (equivalence-class R)
  is-locally-small-equivalence-class C D =
    is-small-equiv
      ( has-same-elements-equivalence-class R C D)
      ( extensionality-equivalence-class R C D)
      ( is-small-Π
        ( is-small')
        ( λ x  is-small-logical-equivalence is-small' is-small'))

The type of equivalence classes is small

module _
  {l1 l2 : Level} {A : UU l1} (R : Eq-Rel l2 A)
  where

  is-small-equivalence-class : is-small (l1  l2) (equivalence-class R)
  is-small-equivalence-class =
    is-small-is-surjective
      ( is-surjective-class R)
      ( is-small-lmax l2 A)
      ( is-locally-small-equivalence-class R)

  equivalence-class-Small-Type : Small-Type (l1  l2) (l1  lsuc l2)
  pr1 equivalence-class-Small-Type = equivalence-class R
  pr2 equivalence-class-Small-Type = is-small-equivalence-class

  small-equivalence-class : UU (l1  l2)
  small-equivalence-class =
    small-type-Small-Type equivalence-class-Small-Type