A / R -> A -> HProp. Proof. intros x b; revert x. srapply Quotient_rec. 1: intro a; exact (Build_HProp (R a b)). intros a c p; cbn beta. apply path_hprop. srapply equiv_iff_hprop; cbn. 1: apply (transitivity (symmetry _ _ p)). apply (transitivity p). Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.