Lemma matrix_hlevel (X : UU) (n m : nat) {o : nat} (ism : isofhlevel o X) : isofhlevel o (Matrix X n m). Proof. do 2 apply vector_hlevel; assumption. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.