(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) (R : A -> B -> HProp) (bitot_R : bitotal R) (h : SPushout R -> V) (H_h : forall x : SPushout R, P (h x)), (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) ) (A B : Type) (R : A -> B -> HProp) (bitot_R : bitotal R) (h : SPushout R -> V) : apD (V_ind P H_0trunc H_set H_setext) (setext R bitot_R h) = H_setext A B R bitot_R h ((V_ind P H_0trunc H_set H_setext) oD h). Proof. apply path_ishprop. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.