Theorem isweqezmap1 {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (fs : fibseqstr f g z) (y : Y) : isweq (ezmap1 f g z fs y). Proof. intros. set (ff := ezmap1 f g z fs y). set (gg := invezmap1 f g z (pr1 fs) y). assert (egf : ∏ e : _, (gg (ff e)) = e). intro. simpl. apply (hfibertriangle1inv0 g (homotweqinvweq (ezweq f g z fs) (make_hfiber g y e))). assert (efg : ∏ xe : _, (ff (gg xe)) = xe). intro. induction xe as [ x e ]. induction e. simpl. unfold ff. unfold ezmap1. unfold d1. change (make_hfiber g (f x) (pr1 fs x)) with (ezmap f g z fs x). apply (hfibertriangle2 f (make_hfiber f (invmap (ezweq f g z fs) (ezmap f g z fs x)) _) (make_hfiber f x (idpath _)) (homotinvweqweq (ezweq f g z fs) x)). simpl. set (e1 := pathsinv0 (pathscomp0rid (maponpaths f (homotinvweqweq (ezweq f g z fs) x)))). assert (e2 : (maponpaths (hfiberpr1 g z) (homotweqinvweq (ezweq f g z fs) ((ezmap f g z fs) x))) = (maponpaths f (homotinvweqweq (ezweq f g z fs) x))). set (e3 := maponpaths (λ e : _, maponpaths (hfiberpr1 g z) e) (pathsinv0 (homotweqinvweqweq (ezweq f g z fs) x))). simpl in e3. set (e4 := maponpathscomp (ezmap f g z (pr1 fs)) (hfiberpr1 g z) (homotinvweqweq (ezweq f g z fs) x)). simpl in e4. apply (pathscomp0 e3 e4). apply (pathscomp0 e2 e1). apply (isweq_iso _ _ egf efg). Defined.