Definition isaddmonoidfuntoringdiff (X : rig) : @ismonoidfun (rigaddabmonoid X) (rigtoring X) (toringdiff X) := isbinop1funtoringdiff X ,, isunital1funtoringdiff X.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.