Definition trivialsubmonoid (X : monoid) : @submonoid X. Proof. intros. exists (λ x, x = 1)%logic. split. - intros b c. induction b as [x p], c as [y q]. cbn in *. induction (!p), (!q). rewrite lunax. apply idpath. - apply idpath. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.