(x : V) : V -> HProp. Proof. simple refine (V_rec' _ _ _ _). - intros A f _. exact (hexists (fun a : A => f a = x)). - simpl. intros A B f g eqimg _ _ _. apply path_iff_hprop; simpl. + intro H. refine (Trunc_rec _ H). intros [a p]. generalize (fst eqimg a). apply (Trunc_functor (-1)). intros [b p']. exists b. transitivity (f a); auto with path_hints. + intro H. refine (Trunc_rec _ H). intros [b p]. generalize (snd eqimg b). apply (Trunc_functor (-1)). intros [a p']. exists a. transitivity (g b); auto with path_hints. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.