(a b : A) : R a b <~> (class_of R a = class_of R b). Proof. apply equiv_iff_hprop. - apply qglue. - apply related_quotient_paths. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.