proposition: Lemma choose_quotient_ind_prop (P : (forall i, A i / R i) -> Type) `{!forall g, IsHProp (P g)} (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i))) (g : forall i, A i / R i) : P g.
proof: Proof. refine (choose_quotient_ind P a _ g). intros. apply path_ishprop. Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Truncations.Core HoTT.Colimits.Quotient HoTT.Projective