V_ind' (P : V -> Type) (H_0trunc : forall v : V, IsTrunc 0 (P v)) (H_set : forall (A : Type) (f : A -> V) (H_f : forall a : A, P (f a)), P (set f)) (H_setext' : forall (A B : Type) (f : A -> V) (g : B -> V) (eq_img: equal_img f g) (H_f : forall a : A, P (f a)) (H_g : forall b : B, P (g b)) (H_eqimg : (forall a : A, hexists (fun (b : B) => hexists (fun (p:f a = g b) => p # (H_f a) = H_g b))) * (forall b : B, hexists (fun (a : A) => hexists (fun (p:f a = g b) => p # (H_f a) = H_g b))) ), (setext' f g eq_img) # (H_set A f H_f) = (H_set B g H_g) ) : forall v : V, P v. Proof. apply V_ind with H_set; try assumption. intros A B R bitot_R h H_h. pose (f := h o spushl R : A -> V ). pose (g := h o spushr R : B -> V ). pose (H_f := H_h oD spushl R : forall a : A, P (f a)). pose (H_g := H_h oD spushr R : forall b : B, P (g b)). assert (eq_img : equal_img f g). { 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)). } transitivity (transport P (setext' (h o spushl R) (h o spushr R) eq_img) (H_set A (h o spushl R) (H_h oD spushl R))). { apply (ap (fun p => transport P p (H_set A (h o spushl R) (H_h oD spushl R)))). apply path_ishprop. } apply (H_setext' A B f g eq_img H_f H_g). split. - intro a. set (truncb := fst bitot_R a). generalize truncb. apply (Trunc_functor (-1)). intros [b Rab]. exists b. apply tr. exists (ap h (spglue R Rab)). apply (concatR (apD H_h (spglue R Rab))). apply inverse. unfold f, g. apply transport_compose. - intros b. set (trunca := snd bitot_R b). generalize trunca. apply (Trunc_functor (-1)). intros [a Rab]. exists a. apply tr. exists (ap h (spglue R Rab)). apply (concatR (apD H_h (spglue R Rab))). apply inverse. unfold f, g. apply transport_compose. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.