proposition: Theorem path_quotient : forall x y, R x y <~> (class_of R x = class_of R y).
proof: Proof. intros ??. apply equiv_iff_hprop. - apply qglue. - apply related_quotient_paths. Defined.
imports: Basics Types HSet TruncType Colimits.GraphQuotient Truncations.Core PropResizing