Definition isweqvecfun {n} : isweq (el:vec A n → ⟦ n ⟧ → A) := isweq_iso el make_vec make_vec_el el_make_vec_fun.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.