{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') (g : forall i, A i / R i) : B := choose_quotient_ind (fun _ => B) a (fun f f' r => transport_const _ _ @ E f f' r) g.
Require Import