Frac_ishset' : IsHSet Frac. Proof. assert (E : sig (fun n : R => sig (fun d : R => d <> 0 )) <~> Frac). - issig. - apply (istrunc_equiv_istrunc _ E). Qed.
Require Import HoTT.HIT.quotient. Require Import Import Frac.