Lemma coprodofhfiberstohfiber {X Y Z : UU} (f : X -> Z) (g : Y -> Z) (z : Z) : (hfiber f z) ⨿ (hfiber g z) -> hfiber (sumofmaps f g) z. Proof. intros hfg. induction hfg as [ hf | hg ]. - induction hf as [ x fe ]. split with (ii1 x). simpl. assumption. - induction hg as [ y ge ]. split with (ii2 y). simpl. assumption. Defined.