Theorem samehfibers {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (is1 : isincl g) (y : Y) : hfiber f y ≃ hfiber (g ∘ f) (g y). Proof. intros. exists (hfibersftogf f g (g y) (make_hfiber g y (idpath _))). set (z := g y). set (ye := make_hfiber g y (idpath _)). intro xe. apply (iscontrweqf (X := hfibersgftog f g z xe = ye)). { exists (ezmap _ _ _ (fibseq1 _ _ _ (fibseqhf f g z ye) _)). exact (isweqezmap1 _ _ _ _ _). } apply isapropifcontr. apply iscontrhfiberofincl. exact is1. Defined.