forall (r : V -> V) (x : V), hexists (fun w => forall y, y ∈ w <-> hexists (fun z => z ∈ x * (r z = y))). Proof. intro r. refine (V_ind_hprop _ _ _). intros A f _. apply tr. exists (set (r o f)). split. - apply (Trunc_functor (-1)). intros [a p]. exists (f a). split. + apply tr; exists a; auto. + assumption. - apply Trunc_rec. intros [z [h p]]. generalize h. apply (Trunc_functor (-1)). intros [a p']. exists a. transitivity (r z); auto with path_hints. exact (ap r p'). Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.