F_rect@{i} (P : F -> Type@{i}) {sP : forall x, IsHSet (P x)} (dclass : forall x : Frac R, P (' x)) (dequiv : forall x y E, (path E) # (dclass x) = (dclass y)) : forall q, P q := quotient_ind equiv P dclass dequiv.
Require Import HoTT.HIT.quotient. Require Import Import Frac.