V@{U' U} -> V@{U' U} -> HProp@{U}. Proof. refine (V_rec' (V -> HProp) _ bisim_aux _). intros A B f g eq_img H_f H_g H_img. apply path_forall. refine (V_ind_hprop _ _ _). intros C h _; simpl. apply path_iff_hprop; simpl. - intros [H1 H2]; split. + intro b. refine (Trunc_rec _ (snd H_img b)). intros [a p]. generalize (H1 a). apply (Trunc_functor (-1)). intros [c H3]. exists c. exact ((ap10 p (h c)) # H3). + intro c. refine (Trunc_rec _ (H2 c)). intros [a H3]. generalize (fst H_img a). apply (Trunc_functor (-1)). intros [b p]. exists b. exact ((ap10 p (h c)) # H3). - intros [H1 H2]; split. + intro a. refine (Trunc_rec _ (fst H_img a)). intros [b p]. generalize (H1 b). apply (Trunc_functor (-1)). intros [c H3]. exists c. exact ((ap10 p^ (h c)) # H3). + intro c. refine (Trunc_rec _ (H2 c)). intros [b H3]. generalize (snd H_img b). apply (Trunc_functor (-1)). intros [a p]. exists a. exact ((ap10 p^ (h c)) # H3). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.