proposition: Lemma choose_quotient_rec_compute {B : Type} `{!IsHSet B} (a : (forall i, A i) -> B) (E : forall (f f' : forall i, A i), (forall i, R i (f i) (f' i)) -> a f = a f') (f : forall i, A i) : choose_quotient_rec a E (fun i => class_of (R i) (f i)) = a f.
proof: Proof. apply (choose_quotient_ind_compute (fun _ => B)). Qed.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Truncations.Core HoTT.Colimits.Quotient HoTT.Projective