(A : Type) : HasTrChoice 0 A -> HasQuotientChoice A. Proof. intros ch B sB R pR rR sR tR f. set (P := fun a b => class_of (R a) b = f a). assert (forall a, merely ((fun x => {b | P x b}) a)) as g. - intro a. refine (Quotient_ind_hprop _ (fun c => merely {b | class_of (R a) b = c}) _ (f a)). intro b. apply tr. by exists b. - pose proof (ch (fun a => {b | P a b}) _ g) as h. strip_truncations. apply tr. exists (fun x => (h x).1). intro a. apply h. Qed.
Require Import