Definition pointwise_unit (un : X) (unax : isunit op un) : isunit (pointwise n op) (const_vec un). Proof. use make_isunit. - apply pointwise_lunit; exact (pr1 unax). - apply pointwise_runit; exact (pr2 unax). 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.