V_ind@{U' U u | U < U'} (P : V@{U' U} -> Type@{u}) (H_0trunc : forall v : V@{U' U}, IsTrunc 0 (P v)) (H_set : forall (A : Type@{U}) (f : A -> V) (H_f : forall a : A, P (f a)), P (set f)) (H_setext : forall (A B : Type@{U}) (R : A -> B -> HProp@{U}) (bitot_R : bitotal R) (h : SPushout R -> V) (H_h : forall x : SPushout R, P (h x)), transport@{U' u} _ (setext R bitot_R h) (H_set A (h o spushl R) (H_h oD spushl R)) = H_set B (h o spushr R) (H_h oD spushr R) ) (v : V) : P v := (match v with | set A f => fun _ _ => H_set A f (fun a => V_ind P H_0trunc H_set H_setext (f a)) end) H_setext H_0trunc.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.