fact: Definition ezweqhf {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (ye : hfiber g z) : hfiber f (pr1 ye) ≃ hfiber (hfibersgftog f g z) ye := make_weq _ (isweqezmaphf f g z ye).
imports: UniMath.Foundations.Preamble