V_rec' (P : Type) (H_0trunc : IsTrunc 0 P) (H_set : forall (A : Type), (A -> V) -> (A -> P) -> P) (H_setext' : forall (A B : Type) (f : A -> V) (g : B -> V), (equal_img f g) -> forall (H_f : A -> P) (H_g : B -> P), (equal_img H_f H_g) -> (H_set A f H_f) = (H_set B g H_g) ) : V -> P. Proof. refine (V_rec _ _ H_set _). intros A B R bitot_R h H_h. apply H_setext'. - split. + intro a. generalize (fst bitot_R a). apply (Trunc_functor (-1)). intros [b r]. exists b. exact (ap h (spglue R r)). + intro b. generalize (snd bitot_R b). apply (Trunc_functor (-1)). intros [a r]. exists a. exact (ap h (spglue R r)). - split. + intro a. generalize (fst bitot_R a). apply (Trunc_functor (-1)). intros [b r]. exists b. exact (ap H_h (spglue R r)). + intro b. generalize (snd bitot_R b). apply (Trunc_functor (-1)). intros [a r]. exists a. exact (ap H_h (spglue R r)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.