proposition: Lemma has_tr0_choice_quotientchoice : HasTrChoice 0 A.
proof: Proof. intros B sB f. transparent assert (g : (forall a, B a / RelUnit B a)). - intro a. specialize (f a). strip_truncations. exact (class_of _ f). - specialize (qch B _ (RelUnit B) _ _ _ _ g). strip_truncations. apply tr. apply qch. Qed.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Truncations.Core HoTT.Colimits.Quotient HoTT.Projective