Theorem weqhfibersofsumofmaps {X Y Z : UU} (f : X -> Z) (g : Y -> Z) (z : Z) : weq ((hfiber f z) ⨿ (hfiber g z)) (hfiber (sumofmaps f g) z). Proof. intros. set (ff := coprodofhfiberstohfiber f g z). set (gg := hfibertocoprodofhfibers f g z). split with ff. assert (effgg : ∏ hsfg : _, paths (ff (gg hsfg)) hsfg). { intro. induction hsfg as [ xy e ]. induction xy as [ x | y ]. - simpl. apply idpath. - simpl. apply idpath. } assert (eggff : ∏ hfg : _, paths (gg (ff hfg)) hfg). { intro. induction hfg as [ hf | hg ]. induction hf as [ x fe ]. - simpl. apply idpath. - induction hg as [ y ge ]. simpl. apply idpath. } apply (isweq_iso _ _ eggff effgg). Defined.