Definition iscontr_vector_0 X : iscontr (Vector X 0). Proof. intros. apply (@iscontrweqb _ (empty -> X)). - apply invweq. apply weqbfun. apply weqstn0toempty. - apply iscontrfunfromempty. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.