Equivalence Relations

Table of Contents

1 Equivalence relations

module Lib.EquivalenceRelations where

This file defines equivalence relations.

1.1 Packages imports

The imported packages can be accessed via the following links: 

import Lib.SubTypes
import Lib.Prop.Proposition

1.2 Definitions

An equivalence relation is a binary relation such that it is:

  • reflexive ;
  • transitive, and ;
  • symmetric.
Relation (A : U) : U =
  A → A → U

is-reflexive (A : U) (R : Relation A) : U =
  (x : A) → R x x  

is-transitive (A : U) (R : Relation A) : U =
  (x y z : A) → R x y → R y z → R x z

is-symmetric (A : U) (R : Relation A) : U =
  (x y : A) → R x y → R y x

An equivalence relation can be valued in the Prop universe. 

Relation-Prop (A : U) : U =
  A → A → UU-Prop

Relation-Prop/type (A : U) (R : Relation-Prop A) : Relation A =
  λx y. Prop/type (R x y)

Relation-Prop/is-reflexive (A : U) (R : Relation-Prop A) : U =
  is-reflexive A (Relation-Prop/type A R)

Relation-Prop/is-transitive (A : U) (R : Relation-Prop A) : U =
  is-transitive A (Relation-Prop/type A R)

Relation-Prop/is-symmetric (A : U) (R : Relation-Prop A) : U =
  is-symmetric A (Relation-Prop/type A R)

1.3 As properties

On relations valued in the Prop universe, is-reflexive, is-transitive and is-symmetric are Prop. 

is-reflexive/is-prop (A : U) (R : Relation-Prop A) : is-prop (Relation-Prop/is-reflexive A R) =
  is-prop/pi A
    ( λx. Prop/type (R x x))
    ( λx. Prop/is-prop (R x x))

is-reflexive/Prop (A : U) (R : Relation-Prop A) : UU-Prop =
  ( Relation-Prop/is-reflexive A R,
    is-reflexive/is-prop A R)

is-transitive/is-prop (A : U) (R : Relation-Prop A) : is-prop (Relation-Prop/is-transitive A R) =
  is-prop/pi A
    ( λx. (y z : A) → Prop/type (R x y) → Prop/type (R y z) → Prop/type (R x z))
    ( λx. is-prop/pi A
          ( λy. (z : A) → Prop/type (R x y) → Prop/type (R y z) → Prop/type (R x z))
          ( λy. is-prop/pi A
                ( λz. Prop/type (R x y) → Prop/type (R y z) → Prop/type (R x z))
                ( λz. is-prop/pi
                      ( Prop/type (R x y))
                      ( λ_. Prop/type (R y z) → Prop/type (R x z))
                      ( λ_. is-prop/pi
                            ( Prop/type (R y z))
                            ( λ_. Prop/type (R x z))
                            ( λ_. Prop/is-prop (R x z))))))

is-transitive/Prop (A : U) (R : Relation-Prop A) : UU-Prop =
  ( Relation-Prop/is-transitive A R,
    is-transitive/is-prop A R)

is-symmetric/is-prop (A : U) (R : Relation-Prop A) : is-prop (Relation-Prop/is-symmetric A R) =
  is-prop/pi A
    ( λx. (y : A) → Prop/type (R x y) → Prop/type (R y x))
    ( λx. is-prop/pi A
          ( λy. Prop/type (R x y) → Prop/type (R y x))
          ( λy. is-prop/pi
                ( Prop/type (R x y))
                ( λ_. Prop/type (R y x))
                ( λ_. Prop/is-prop (R y x))))

is-symmetric/Prop (A : U) (R : Relation-Prop A) : UU-Prop =
  ( Relation-Prop/is-symmetric A R,
    is-symmetric/is-prop A R)

1.4 Equivalence relation

is-equivalence-relation (A : U) (R : Relation-Prop A) : U =
  Relation-Prop/is-reflexive A R *
    ( Relation-Prop/is-symmetric A R *
      Relation-Prop/is-transitive A R)

Eq-Rel (A : U) : U =
  Σ (Relation-Prop A) (is-equivalence-relation A)

Getters. 

Eq-Rel/Relation (A : U) (R : Eq-Rel A) : Relation-Prop A = R.1

Eq-Rel/type (A : U) (R : Eq-Rel A) (x y : A) : U = Prop/type (Eq-Rel/Relation A R x y)

Eq-Rel/is-reflexive (A : U) (R : Eq-Rel A) : Relation-Prop/is-reflexive A (Eq-Rel/Relation A R) = R.2.1

Eq-Rel/is-symmetric (A : U) (R : Eq-Rel A) : Relation-Prop/is-symmetric A (Eq-Rel/Relation A R) = R.2.2.1

Eq-Rel/is-transitive (A : U) (R : Eq-Rel A) : Relation-Prop/is-transitive A (Eq-Rel/Relation A R) = R.2.2.2

Being a reflection of the identity is a property. 

reflects-Eq-Rel (A : U) (R : Eq-Rel A) (B : U) (f : A → B) : U =
  (x y : A) → (Eq-Rel/type A R x y) → Path B (f x) (f y)

reflecting-map-Eq-Rel (A : U) (R : Eq-Rel A) (B : U) : U =
  Σ (A → B) (reflects-Eq-Rel A R B)

reflecting-map-Eq-Rel/map (A : U) (R : Eq-Rel A) (B : U) (t : reflecting-map-Eq-Rel A R B) : A → B = t.1

reflecting-map-Eq-Rel/reflects-Eq (A : U) (R : Eq-Rel A) (B : U) (t : reflecting-map-Eq-Rel A R B) : reflects-Eq-Rel A R B (reflecting-map-Eq-Rel/map A R B t) = t.2  

reflects-Eq-Rel/is-prop (A : U) (R : Eq-Rel A) (B : UU-Set) (f : A → Set/type B)
                           : is-prop (reflects-Eq-Rel A R (Set/type B) f) =
  is-prop/pi-2 A
    ( λ_. A)
    ( λx y. Eq-Rel/type A R x y → Path (Set/type B) (f x) (f y))
    ( λx y. is-prop/pi
            ( Eq-Rel/type A R x y)
            ( λ_. Path (Set/type B) (f x) (f y))
            ( λ_. Set/is-set B (f x) (f y)))

We characterize the equality of reflecting-map-Eq-Rel. 

reflecting-map-Eq-Rel/htpy (A : U) (R : Eq-Rel A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B)) (g : reflecting-map-Eq-Rel A R (Set/type B)) : U =
  Htpy' A (Set/type B) f.1 g.1

reflecting-map-Eq-Rel/refl-htpy (A : U) (R : Eq-Rel A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B)) : reflecting-map-Eq-Rel/htpy A R B f f =
  Htpy'/refl A (Set/type B) f.1

reflecting-map-Eq-Rel/eq-htpy (A : U) (R : Eq-Rel A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B)) (g : reflecting-map-Eq-Rel A R (Set/type B))
                              (p : Path (reflecting-map-Eq-Rel A R (Set/type B)) f g) : reflecting-map-Eq-Rel/htpy A R B f g =
  J ( reflecting-map-Eq-Rel A R (Set/type B)) f
    ( λh _. reflecting-map-Eq-Rel/htpy A R B f h)
    ( reflecting-map-Eq-Rel/refl-htpy A R B f) g p

reflecting-map-Eq-Rel/is-contr-total-htpy (A : U) (R : Eq-Rel A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B))
                                             : is-contr (Σ (reflecting-map-Eq-Rel A R (Set/type B)) (reflecting-map-Eq-Rel/htpy A R B f)) =
  substructure/is-contr-total-Eq
    ( A → (Set/type B))
    ( Htpy' A (Set/type B) f.1)
    ( reflects-Eq-Rel A R (Set/type B))
    ( Htpy/is-contr-total-htpy A
      ( λ_. Set/type B) f.1)
    ( reflects-Eq-Rel/is-prop A R B) f.1
    ( reflecting-map-Eq-Rel/refl-htpy A R B f) f.2

reflecting-map-Eq-Rel/eq-htpy/is-equiv (A : U) (R : Eq-Rel A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B)) (g : reflecting-map-Eq-Rel A R (Set/type B))
                                          : is-equiv (Path (reflecting-map-Eq-Rel A R (Set/type B)) f g)
                                                     (reflecting-map-Eq-Rel/htpy A R B f g) (reflecting-map-Eq-Rel/eq-htpy A R B f g) =
  fundamental-theorem-id
    ( reflecting-map-Eq-Rel A R (Set/type B))
    ( reflecting-map-Eq-Rel/htpy A R B f) f
    ( reflecting-map-Eq-Rel/eq-htpy A R B f)
    ( reflecting-map-Eq-Rel/is-contr-total-htpy A R B f) g

reflecting-map-Eq-Rel/htpy-eq (A : U) (R : Eq-Rel A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B)) (g : reflecting-map-Eq-Rel A R (Set/type B))
                                 : (reflecting-map-Eq-Rel/htpy A R B f g) → (Path (reflecting-map-Eq-Rel A R (Set/type B)) f g) =
  is-equiv/inv-map
    ( Path (reflecting-map-Eq-Rel A R (Set/type B)) f g)
    ( reflecting-map-Eq-Rel/htpy A R B f g)
    ( reflecting-map-Eq-Rel/eq-htpy A R B f g)
    ( reflecting-map-Eq-Rel/eq-htpy/is-equiv A R B f g)

reflecting-map-Eq-Rel/Equiv (A : U) (R : Eq-Rel A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B)) (g : reflecting-map-Eq-Rel A R (Set/type B))
                               : Equiv (Path (reflecting-map-Eq-Rel A R (Set/type B)) f g) (reflecting-map-Eq-Rel/htpy A R B f g) =
  ( reflecting-map-Eq-Rel/eq-htpy A R B f g,
    reflecting-map-Eq-Rel/eq-htpy/is-equiv A R B f g)

Author: Johann Rosain

Created: 2024-07-23 Tue 13:50

Validate