Definition hfiberbinop {A B : setwithbinop} (f : binopfun A B) (b1 b2 : B) (hf1 : hfiber (pr1 f) b1) (hf2 : hfiber (pr1 f) b2) : hfiber (pr1 f) (@op B b1 b2) := make_hfiber (pr1 f) (@op A (pr1 hf1) (pr1 hf2)) (hfiberbinop_path f b1 b2 hf1 hf2).