quotient R -> A -> HProp. Proof. refine (quotient_ind R (fun _ => A -> HProp) (fun a b => Build_HProp (R a b)) _). intros. eapply concat;[apply transport_const|]. apply path_forall. intro z. apply path_hprop; simpl. apply @equiv_iff_hprop; eauto. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.