Definition ezmap1 {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (fs : fibseqstr f g z) (y : Y) (e : (g y) = z) : hfiber f y. Proof. intros. split with (d1 f g z fs y e). unfold d1. change (f (invmap (ezweq f g z fs) (make_hfiber g y e))) with (hfiberpr1 _ _ (ezweq f g z fs (invmap (ezweq f g z fs) (make_hfiber g y e)))). apply (maponpaths (hfiberpr1 g z) (homotweqinvweq (ezweq f g z fs) (make_hfiber g y e))). Defined.