category of large vector spaces over a large field with a small basis

Recall from our foundations that we work with sets ("small sets") and collections ("large sets"). A large field $K$ is a collection equipped with a field structure. Concrete examples are $\IQ(X_\alpha : \alpha \in \OnColl)$ and the field of nimbers $\On_2$. There is a well-behaved hypercategory $\Vect_K$ of large vector spaces over $K$, which are collections equipped with a suitable algebraic structure. (See the linked article on foundations for the definition of a hypercategory.) Since collections and sets behave mostly the same (both satisfy the ZFC-axioms), it has analogous properties to its small counterpart: it is a split abelian, finitary algebraic hypercategory, and every object is isomorphic to $K^{\oplus X}$ for a collection $X$.
In this entry, we consider the full sub-hypercategory $\Vect^s_K$ of $\Vect_K$ consisting of the large vector spaces that are isomorphic to $K^{\oplus X}$ for a set $X$. The relationship between $\Vect^s_K$ and $\Vect_K$ is similar to that between $\FinVect_K$ and $\Vect_K$. However, $\Vect^s_K$ is not self-dual, which breaks the analogy.
However, $\Vect^s_K$ is not a category as defined in our foundations, because the totality of its objects is not a collection. Even the totality of trivial large vector spaces is not a collection, analogous to the fact that the collection of trivial vector spaces is not a set. However, the totality of objects of $\Vect^s_K$ is in bijection with the collection of sets, so $\Vect^s_K$ is equivalent (as a hypercategory) to a category. This category has sets as objects and (not necessarily finite) column-finite matrices over $K$ as morphisms. Formally, we need to work with this category to stay within our framework, but it is easier and more natural to work with $\Vect^s_K$ instead, in particular when studying its properties. To decide all properties, we assume that $K$ is not essentially small.
This category does not appear in practice, but it provides an example of a Grothendieck abelian category that is not complete, which is impossible in the locally small case.