(C : V -> HProp) : forall a : V, hexists (fun w => forall x, x ∈ w <-> x ∈ a * (C x)). Proof. refine (V_ind_hprop _ _ _). intros A f _. apply tr. exists (set (fun z : {a : A & C (f a)} => f (pr1 z))). split. - apply Trunc_rec. intros [[a h] p]. split. + apply tr; exists a; assumption. + exact (transport C p h). - intros [H1 H2]. generalize H1. apply (Trunc_functor (-1)). intros [a p]. exists (a; transport C p^ H2). exact p. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.