(P : (forall i, A i / R i) -> Type) `{!forall g, IsHSet (P g)} (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i))) (E : forall (f f' : forall i, A i) (r : forall i, R i (f i) (f' i)), qglue_forall f f' r # a f = a f') (g : forall i, A i / R i) : ChooseProp P a g. Proof. pose proof (has_quotient_choice_tr0choice I _ A _ R _ _ _ _ g) as h. strip_truncations. destruct h as [h p]. apply path_forall in p. refine (transport _ p _). exists (a h). apply tr. exists h. exists 1. apply E. Defined.
Require Import