Library UniMath.Combinatorics.Equivalence_Relations

Author: Floris van Doorn, december 2017

Equivalence relations.

Contents:

construction of the equivalence relation generated by an arbitrary relation, defined as the truncation of paths in a graph

Definition eqrel_closure_hrel {X : UU} (R : hrel X) : hrel X :=
  λ x y, ∥ gpaths (symmetric_closure R) x y ∥.

Lemma iseqrel_closure {X : UU} (R : hrel X) : iseqrel (eqrel_closure_hrel R).
Proof.
  use iseqrelconstr.
  - intros x y z. apply hinhfun2. apply concat.
  - intro x. apply hinhpr. apply nil.
  - intros x y. apply hinhfun. apply reverse_in_closure.
Defined.

Definition eqrel_closure {X : UU} (R : hrel X) : eqrel X :=
  make_eqrel _ (iseqrel_closure R).

Lemma eqrel_closure_minimal {X : UU} {R : hrel X} (S : eqrel X) (H : ∏ x x', R x x' → S x x') {x x' : X} :
  eqrel_closure R x x' → S x x'.
Proof.
  apply hinhuniv. revert x. apply gpaths_ind.
  - apply eqrelrefl.
  - intros x y r p HS. refine (eqreltrans S _ _ _ _ HS).
    induction r as [r|r].
    + apply H. exact r.
    + apply eqrelsymm. apply H. exact r.
Defined.