# Equivalence classes

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Eléonore Mangel, Elisabeth Stenholm, Julian KG, fernabnor and louismntnu.

Created on 2022-02-17.

module foundation.equivalence-classes where
Imports
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.effective-maps-equivalence-relations
open import foundation.existential-quantification
open import foundation.functoriality-propositional-truncation
open import foundation.fundamental-theorem-of-identity-types
open import foundation.inhabited-subtypes
open import foundation.locally-small-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.reflecting-maps-equivalence-relations
open import foundation.slice
open import foundation.small-types
open import foundation.subtype-identity-principle
open import foundation.subtypes
open import foundation.surjective-maps
open import foundation.universal-property-image
open import foundation.universe-levels

open import foundation-core.cartesian-product-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.identity-types
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.torsorial-type-families

## 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 : equivalence-relation l2 A)
where

is-equivalence-class-Prop : subtype l2 A  Prop (l1  l2)
is-equivalence-class-Prop P =
A  x  has-same-elements-subtype-Prop P (prop-equivalence-relation 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-equivalence-relation :
subtype (l1  l2) (inhabited-subtype l2 A)
is-equivalence-class-inhabited-subtype-equivalence-relation 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-equivalence-relation R x
pr2 (class x) =
unit-trunc-Prop
( x , refl-has-same-elements-subtype (prop-equivalence-relation 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 (Q , H) =
apply-universal-property-trunc-Prop H
( is-inhabited-subtype-Prop (subtype-equivalence-class (Q , H)))
( λ u
unit-trunc-Prop
( pr1 u ,
backward-implication
( pr2 u (pr1 u))
( refl-equivalence-relation R (pr1 u))))

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-equivalence-relation 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-equivalence-relation R x)
( p)))))
( pr2 C)

is-image-equivalence-class :
is-image
( prop-equivalence-relation R)
( emb-equivalence-class)
( unit-im-equivalence-class)
is-image-equivalence-class =
is-image-is-surjective
( prop-equivalence-relation 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 : equivalence-relation 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-torsorial-has-same-elements-equivalence-class :
(C : equivalence-class R)
is-torsorial (has-same-elements-equivalence-class C)
is-torsorial-has-same-elements-equivalence-class C =
is-torsorial-Eq-subtype
( is-torsorial-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-torsorial-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 : equivalence-relation 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 =
( A)
( λ x
is-in-equivalence-class-Prop R C x  is-in-equivalence-class-Prop 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-equivalence-relation R v x
by φ x
sim-equivalence-relation R a x
by iff-transitive-equivalence-relation R
( symmetric-equivalence-relation
R _ _ (forward-implication (φ a) c))
sim-equivalence-relation R w x
by iff-transitive-equivalence-relation 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 (a , refl-equivalence-relation R a , H))

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

module _
{l1 l2 : Level} {A : UU l1} (R : equivalence-relation 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-equivalence-relation R a

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 (C , H) =
eq-type-subtype
( λ D  is-in-equivalence-class-Prop R D a)
( eq-class-equivalence-class R C H)

is-torsorial-is-in-equivalence-class :
is-torsorial  P  is-in-equivalence-class R P a)
pr1 is-torsorial-is-in-equivalence-class =
center-total-is-in-equivalence-class
pr2 is-torsorial-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-equivalence-relation R a

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-torsorial-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 : equivalence-relation 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-symmetric-equivalence-relation R) ∘e
( effective-quotient' x (class R y))

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

abstract
apply-effectiveness-class' :
{x y : A}  sim-equivalence-relation 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 : equivalence-relation 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 : equivalence-relation l2 A)
where

quotient-reflecting-map-equivalence-class :
reflecting-map-equivalence-relation 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 : equivalence-relation l2 A)
where

transitive-is-in-equivalence-class :
(P : equivalence-class R) (a b : A)
is-in-equivalence-class R P a  sim-equivalence-relation 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)
( λ (x , H)
backward-implication
( H b)
( transitive-equivalence-relation R _ a b
( r)
( forward-implication (H a) p)))

### The type of equivalence classes is locally small

module _
{l1 l2 : Level} {A : UU l1} (R : equivalence-relation 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 : equivalence-relation 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