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.
Require Import UniMath.Combinatorics.GraphPaths. Require Import UniMath.MoreFoundations.Subtypes.