(P : rng_localization -> Type) (H : forall x, IsHProp (P x)) (Hin : forall x, P (loc_in x)) (Hinv : forall x (H : IsInvertible rng_localization x), P x -> P (inverse_elem x)) (Hmul : forall x y, P x -> P y -> P (x * y)) : forall x, P x. Proof. srapply Quotient_ind. - intros f. refine (transport P (fraction_decompose f)^ _). apply Hmul. + apply Hin. + apply Hinv, Hin. - intros f1 f2 p. apply path_ishprop. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient