Definition Matrix (X : UU) (m n : nat) : UU := Vector (Vector X n) m.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.