Definition pointwise {X : UU} (n : nat) (op : binop X) : binop (Vector X n) := λ v1 v2 i, op (v1 i) (v2 i).
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.