proposition: Lemma Frac_ishset' : IsHSet Frac.
proof: Proof. assert (E : sig (fun n : R => sig (fun d : R => d <> 0 )) <~> Frac). - issig. - apply (istrunc_equiv_istrunc _ E). Qed.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields