fact: Definition F_rec@{i} {T : Type@{i} } {sT : IsHSet T} : forall (dclass : Frac R -> T) (dequiv : forall x y, equiv x y -> dclass x = dclass y), F -> T := quotient_rec equiv.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields