Lemma isgrdirprod (X Y : gr) : isgrop (@op (setwithbinopdirprod X Y)). Proof. exists (ismonoiddirprod X Y). exists (λ xy, (pr1 xy)^-1 ,, (pr2 xy)^-1). split. - intro xy. induction xy as [ x y ]. unfold unel_is. simpl. apply pathsdirprod. apply (grlinvax X x). apply (grlinvax Y y). - intro xy. induction xy as [ x y ]. unfold unel_is. simpl. apply pathsdirprod. apply (grrinvax X x). apply (grrinvax Y y). Defined.
Require Import UniMath.MoreFoundations.Subtypes.