Definition eqrel_closure_hrel {X : UU} (R : hrel X) : hrel X := λ x y, ∥ gpaths (symmetric_closure R) x y ∥.
Require Import UniMath.Combinatorics.GraphPaths. Require Import UniMath.MoreFoundations.Subtypes.