Definition isgropisof {X Y : setwithbinop} (f : binopiso X Y) (is : isgrop (@op X)) : isgrop (@op Y) := ismonoidopisof f is ,, (f ∘ grinv_is is ∘ invmap f) ,, isinvisof f (unel_is is) (grinv_is is) (pr2 (pr2 is)).