The category of finite dimensional vector spaces #
FinVect K, the category of finite dimensional vector spaces on a field
It is implemented as a full subcategory on a subtype of
We first create the instance as a category, then as a monoidal category and then as a rigid monoidal
Future work #
- Show that
FinVect Kis a symmetric monoidal category.