Corollary isweqfinfibseq {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (fs : fibseqstr f g z) (isz : iscontr Z) : isweq f. Proof. intros. apply (isofhlevelfffromZ 0 f g z fs (isapropifcontr isz)). Defined.