fact: Definition 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.
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient