(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). Section choose_has_quotient_choice. Context `{Univalence} {A : Type} {B : A -> Type} `{!forall x, IsHSet (B x)} (P : forall x, B x -> Type) `{!forall x (a : B x), IsHProp (P x a)}. Local RelClassEquiv (x : A) (a : B x) (b : B x) : Type := P x a <~> P x b. Local Instance reflexive_relclass : forall x, Reflexive (RelClassEquiv x). Proof. intros a b. apply equiv_idmap. Qed.
Require Import