Lemma comp_hsubtype_preserving {X Y Z : UU} {U : hsubtype X} {V : hsubtype Y} {W : hsubtype Z} {f : X → Y} {g : Y → Z} (fsp : hsubtype_preserving U V f) (gsp : hsubtype_preserving V W g) : hsubtype_preserving U W (funcomp f g). Proof. intros z zinU. rewrite image_hsubtype_comp in zinU. apply (gsp _). unfold image_hsubtype. use (factor_through_squash _ _ zinU). { apply ishinh. } intro y. apply hinhpr. exists (pr1 y). exists (pr12 y). apply (fsp _). exact (pr22 y). Qed.