(P : V -> Type) (H_set : forall (A : Type) (f : A -> V) (H_f : forall a : A, P (f a)), P (set f)) (isHProp_P : forall v : V, IsHProp (P v)) : forall v : V, P v. Proof. refine (V_ind _ _ H_set _). intros. 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.