Lemma issurjcomp {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (isf : issurjective f) (isg : issurjective g) : issurjective (funcomp f g). Proof. intros. unfold issurjective. intro z. apply (λ ff, hinhuniv ff (isg z)). intro ye. apply (hinhfun (hfibersftogf f g z ye)). apply (isf). Defined.