Definition entrywise_monoidop (monoidax : ismonoidop op) : ismonoidop (entrywise n m op). Proof. use make_ismonoidop. - apply entrywise_assoc, assocax_is; assumption. - use make_isunital. + apply (const_matrix (unel_is monoidax)). + apply entrywise_unit, unax_is. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.FiniteSequences. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.RigsAndRings.