V -> V. Proof. simple refine (V_rec' _ _ _ _). - intros A f _. exact (set (fun (x : A + Unit) => match x with inl a => f a | inr tt => set f end)). - simpl; intros A B f g eq_img _ _ _. apply setext'. split. + intro. destruct a. * generalize (fst eq_img a). apply (Trunc_functor (-1)). intros [b p]. exists (inl b); exact p. * apply tr; exists (inr tt). destruct u. apply setext'; auto. + intro. destruct b. * generalize (snd eq_img b). apply (Trunc_functor (-1)). intros [a p]. exists (inl a); exact p. * apply tr; exists (inr tt). destruct u. apply setext'; auto. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.