Definition trivialsubgr (X : gr) : subgr X. Proof. exists (λ x, x = 1)%logic. split. - exact (pr2 (@trivialsubmonoid X)). - intro. intro eq_1. induction (!eq_1). apply grinvunel. Defined.
Require Import UniMath.MoreFoundations.Subtypes.