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