fact: Definition HasQuotientChoice (A : Type) := forall (B : A -> Type), (forall x, IsHSet (B x)) -> forall (R : forall x, Relation (B x)) (pR : forall x, is_mere_relation (B x) (R x)), (forall x, Reflexive (R x)) -> (forall x, Symmetric (R x)) -> (forall x, Transitive (R x)) -> forall (f : forall x : A, B x / R x), hexists (fun g : (forall x : A, B x) => forall x, class_of (R x) (g x) = f x).
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Truncations.Core HoTT.Colimits.Quotient HoTT.Projective