Definition isgropisob {X Y : setwithbinop} (f : binopiso X Y) (is : isgrop (@op Y)) : isgrop (@op X) := ismonoidopisob f is ,, invmap f ∘ grinv_is is ∘ f ,, isinvisob f (unel_is is) (grinv_is is) (pr2 (pr2 is)).