Lemma hfibertocoprodofhfibers {X Y Z : UU} (f : X -> Z) (g : Y -> Z) (z : Z) : hfiber (sumofmaps f g) z -> (hfiber f z) ⨿ (hfiber g z). Proof. intros hsfg. induction hsfg as [ xy e ]. induction xy as [ x | y ]. - simpl in e. apply (ii1 (make_hfiber _ x e)). - simpl in e. apply (ii2 (make_hfiber _ y e)). Defined.