Lemma issurjtwooutof3b {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (isgf : issurjective (funcomp f g)) : issurjective g. Proof. intros. unfold issurjective. intro z. apply (hinhfun (hfibersgftog f g z) (isgf z)). Defined.