fact: Definition col {X : UU} {m n : nat} (mat : Matrix X m n) : ⟦ n ⟧ → Vector X m := transpose mat.
imports: UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.Lists UniMath.Combinatorics.Vectors UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics