Equivalence relations
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Fernando Chu, Julian KG, fernabnor and louismntnu.
Created on 2022-09-01.
Last modified on 2023-09-11.
module foundation-core.equivalence-relations where
Imports
open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.inhabited-subtypes open import foundation.logical-equivalences open import foundation.propositional-truncations open import foundation.unit-type open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.equivalences open import foundation-core.propositions
Idea
An equivalence relation is a relation valued in propositions, which is reflexive,symmetric, and transitive.
Definition
is-equivalence-relation : {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A) → UU (l1 ⊔ l2) is-equivalence-relation R = is-reflexive-Relation-Prop R × ( is-symmetric-Relation-Prop R × is-transitive-Relation-Prop R) Equivalence-Relation : (l : Level) {l1 : Level} (A : UU l1) → UU ((lsuc l) ⊔ l1) Equivalence-Relation l A = Σ (Relation-Prop l A) is-equivalence-relation prop-Equivalence-Relation : {l1 l2 : Level} {A : UU l1} → Equivalence-Relation l2 A → Relation-Prop l2 A prop-Equivalence-Relation = pr1 sim-Equivalence-Relation : {l1 l2 : Level} {A : UU l1} → Equivalence-Relation l2 A → A → A → UU l2 sim-Equivalence-Relation R = type-Relation-Prop (prop-Equivalence-Relation R) abstract is-prop-sim-Equivalence-Relation : {l1 l2 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) (x y : A) → is-prop (sim-Equivalence-Relation R x y) is-prop-sim-Equivalence-Relation R = is-prop-type-Relation-Prop (prop-Equivalence-Relation R) is-prop-is-equivalence-relation : {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A) → is-prop (is-equivalence-relation R) is-prop-is-equivalence-relation R = is-prop-prod ( is-prop-is-reflexive-Relation-Prop R) ( is-prop-prod ( is-prop-is-symmetric-Relation-Prop R) ( is-prop-is-transitive-Relation-Prop R)) is-equivalence-relation-Prop : {l1 l2 : Level} {A : UU l1} → Relation-Prop l2 A → Prop (l1 ⊔ l2) pr1 (is-equivalence-relation-Prop R) = is-equivalence-relation R pr2 (is-equivalence-relation-Prop R) = is-prop-is-equivalence-relation R is-equivalence-relation-prop-Equivalence-Relation : {l1 l2 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) → is-equivalence-relation (prop-Equivalence-Relation R) is-equivalence-relation-prop-Equivalence-Relation R = pr2 R refl-Equivalence-Relation : {l1 l2 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) → is-reflexive (sim-Equivalence-Relation R) refl-Equivalence-Relation R = pr1 (is-equivalence-relation-prop-Equivalence-Relation R) symmetric-Equivalence-Relation : {l1 l2 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) → is-symmetric (sim-Equivalence-Relation R) symmetric-Equivalence-Relation R = pr1 (pr2 (is-equivalence-relation-prop-Equivalence-Relation R)) transitive-Equivalence-Relation : {l1 l2 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) → is-transitive (sim-Equivalence-Relation R) transitive-Equivalence-Relation R = pr2 (pr2 (is-equivalence-relation-prop-Equivalence-Relation R)) inhabited-subtype-Equivalence-Relation : {l1 l2 : Level} {A : UU l1} → Equivalence-Relation l2 A → A → inhabited-subtype l2 A pr1 (inhabited-subtype-Equivalence-Relation R x) = prop-Equivalence-Relation R x pr2 (inhabited-subtype-Equivalence-Relation R x) = unit-trunc-Prop (x , refl-Equivalence-Relation R x)
Properties
Symmetry induces equivalences R(x,y) ≃ R(y,x)
iff-symmetric-Equivalence-Relation : {l1 l2 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) {x y : A} → sim-Equivalence-Relation R x y ↔ sim-Equivalence-Relation R y x pr1 (iff-symmetric-Equivalence-Relation R) = symmetric-Equivalence-Relation R _ _ pr2 (iff-symmetric-Equivalence-Relation R) = symmetric-Equivalence-Relation R _ _ equiv-symmetric-Equivalence-Relation : {l1 l2 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) {x y : A} → sim-Equivalence-Relation R x y ≃ sim-Equivalence-Relation R y x equiv-symmetric-Equivalence-Relation R = equiv-iff' ( prop-Equivalence-Relation R _ _) ( prop-Equivalence-Relation R _ _) ( iff-symmetric-Equivalence-Relation R)
Transitivity induces equivalences R(y,z) ≃ R(x,z)
iff-transitive-Equivalence-Relation : {l1 l2 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) {x y z : A} → sim-Equivalence-Relation R x y → (sim-Equivalence-Relation R y z ↔ sim-Equivalence-Relation R x z) pr1 (iff-transitive-Equivalence-Relation R r) s = transitive-Equivalence-Relation R _ _ _ s r pr2 (iff-transitive-Equivalence-Relation R r) s = transitive-Equivalence-Relation R _ _ _ ( s) ( symmetric-Equivalence-Relation R _ _ r) equiv-transitive-Equivalence-Relation : {l1 l2 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) {x y z : A} → sim-Equivalence-Relation R x y → (sim-Equivalence-Relation R y z ≃ sim-Equivalence-Relation R x z) equiv-transitive-Equivalence-Relation R r = equiv-iff' ( prop-Equivalence-Relation R _ _) ( prop-Equivalence-Relation R _ _) ( iff-transitive-Equivalence-Relation R r)
Transitivity induces equivalences R(x,y) ≃ R(x,z)
iff-transitive-Equivalence-Relation' : {l1 l2 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) {x y z : A} → sim-Equivalence-Relation R y z → (sim-Equivalence-Relation R x y ↔ sim-Equivalence-Relation R x z) pr1 (iff-transitive-Equivalence-Relation' R r) = transitive-Equivalence-Relation R _ _ _ r pr2 (iff-transitive-Equivalence-Relation' R r) = transitive-Equivalence-Relation R _ _ _ ( symmetric-Equivalence-Relation R _ _ r) equiv-transitive-Equivalence-Relation' : {l1 l2 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) {x y z : A} → sim-Equivalence-Relation R y z → (sim-Equivalence-Relation R x y ≃ sim-Equivalence-Relation R x z) equiv-transitive-Equivalence-Relation' R r = equiv-iff' ( prop-Equivalence-Relation R _ _) ( prop-Equivalence-Relation R _ _) ( iff-transitive-Equivalence-Relation' R r)
Examples
The indiscrete equivalence relation on a type
indiscrete-Equivalence-Relation : {l1 : Level} (A : UU l1) → Equivalence-Relation lzero A pr1 (indiscrete-Equivalence-Relation A) x y = unit-Prop pr1 (pr2 (indiscrete-Equivalence-Relation A)) _ = star pr1 (pr2 (pr2 (indiscrete-Equivalence-Relation A))) _ _ _ = star pr2 (pr2 (pr2 (indiscrete-Equivalence-Relation A))) _ _ _ _ _ = star raise-indiscrete-Equivalence-Relation : {l1 : Level} (l2 : Level) (A : UU l1) → Equivalence-Relation l2 A pr1 (raise-indiscrete-Equivalence-Relation l A) x y = raise-unit-Prop l pr1 (pr2 (raise-indiscrete-Equivalence-Relation l A)) _ = raise-star pr1 (pr2 (pr2 (raise-indiscrete-Equivalence-Relation l A))) _ _ _ = raise-star pr2 (pr2 (pr2 (raise-indiscrete-Equivalence-Relation l A))) _ _ _ _ _ = raise-star
Recent changes
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-26. Fernando Chu and Fredrik Bakke. First definitions towards n-ary functoriality of set quotients (#528).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).