(P : Type) (H_0trunc : IsTrunc 0 P) (H_set : forall (A : Type), (A -> V) -> (A -> P) -> P) (H_setext : forall (A B : Type) (R : A -> B -> HProp) (bitot_R : bitotal R) (h : SPushout R -> V) (H_h : SPushout R -> P), H_set A (h o spushl R) (H_h o spushl R) = H_set B (h o spushr R) (H_h o spushr R) ) (A B : Type) (R : A -> B -> HProp) (bitot_R : bitotal R) (h : SPushout R -> V) : ap (V_rec P H_0trunc H_set H_setext) (setext R bitot_R h) = H_setext A B R bitot_R h ((V_rec P H_0trunc H_set H_setext) o 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.