Classical axiomatic set theories (eg ZFC, NGB) are formulated in first-order logic with equality, so any things you can quantify over (i.e. that you can talk about as actual objects of the language), you can talk about equality of, as a basic given of the language.

In particular, in either ZFC or NGB, you can certainly talk about equality of vector spaces. In ZFC, you can’t talk about beasts as quantify-over-able objects (since they can only be represented as proper classes, not as sets); in NGB, you can, and so you get equality of them.

Cardinality is a bit slipperier: it’s generally considered as a defined rather than a basic notion, and the exact definitions used vary in ways your question will be sensitive to. Most often, an object called the “cardinality” is only specifically defined for sets^[1]; for classes, “C and D have the same cardinality” is considered syntactic sugar for “there is a class-bijection between C and D”. So it’s not quite clear what it means to ask if a class “has cardinality”, but whatever it is depends heavily on having an equality relation on it, to be able to talk about bijections to/from it.

On the other hand, there are some more recent set/type theories in which equality isn’t given, or is a more flexible notion.

In some versions of the Calculus of Constructions, if I remember right, there is a universe of small sets (possibly multiple universes), and an arbitrary product of sets is again a set, possibly in some higher universe (this has to be formulated carefully to avoid inconsistency); and each set has equality on it, but there’s no equality on the universe(s). So there, vector spaces wouldn’t form a set, and wouldn’t have an equality relation; but beasts would form a set (a certain product of hom-sets) so would have an equality relation. (The C of C’s is a little out of what I know, so this may need correcting by someone more knowledgeable.)

Similarly, there are versions of Martin-Löf Type Theory with identity types which address this issue; roughly, identity types can represent something like an ordinary equality relation, but more generally they can also look like the sets/categories of (weak) ismorphisms in a (higher) category. So you can define an object to be 0-categorical^[1] if all its identity types are just truth-values; then an arbitrary product of 0-categorical types is again 0-categorical.

In this setup, the type of all vector spaces within some universe will have identity types, so equality of a sort, but not of the objectionable kind — “equality” of vector spaces will exactly be isomorphism between them. The type of beasts over this universe will now be 0-categorical: we will have equality of beasts in the simplest sense. (Also, in this foundation, all beasts will automatically respect isomorphism!)

[1]: The two main definitions of $\|X\|$ I know are “the least ordinal bijective to $X$” (elegant, but requires choice to be defined for all $X$), or “$\{ Y \in V_\alpha\ |\ Y \cong X \}$, where $\alpha$ is minimal such that this is non-empty” (less transparent but more robust).

[2]: I first heard this definition from Voevodsky, though I’m pretty sure it had been considered by others before as well. He calls this property being a set, but I want to make unambiguous that it’s a restriction of categorical dimension not of size.

Classical axiomatic set theories (eg ZFC, NGB) are formulated in first-order logic with equality, so any things you can quantify over (i.e. that you can talk about as actual objects of the language), you can talk about equality of, as a basic given of the language.

In particular, in either ZFC or NGB, you can certainly talk about equality of vector spaces. In ZFC, you can’t talk about beasts as quantify-over-able objects (since they can only be represented as proper classes, not as sets); in NGB, you can, and so you get equality of them.

Cardinality is a bit slipperier: it’s generally considered as a defined rather than a basic notion, and the exact definitions used vary in ways your question will be sensitive to. Most often, an object called the “cardinality” is only specifically defined for sets^[1]; for classes, “C and D have the same cardinality” is considered syntactic sugar for “there is a class-bijection between C and D”. So it’s not quite clear what it means to ask if a class “has cardinality”, but whatever it is depends heavily on having an equality relation on it, to be able to talk about bijections to/from it.

On the other hand, there are some more recent set/type theories in which equality isn’t given, or is a more flexible notion.

In some versions of the Calculus of Constructions, if I remember right, there is a universe of small sets (possibly multiple universes), and an arbitrary product of sets is again a set, possibly in some higher universe (this has to be formulated carefully to avoid inconsistency); and each set has equality on it, but there’s no equality on the universe(s). So there, vector spaces wouldn’t form a set, and wouldn’t have an equality relation; but beasts would form a set (a certain product of hom-sets) so would have an equality relation. (The C of C’s is a little out of what I know, so this may need correcting by someone more knowledgeable.)

Similarly, there are versions of Martin-Löf Type Theory with identity types which address this issue; roughly, identity types can represent something like an ordinary equality relation, but more generally they can also look like the sets/categories of (weak) ismorphisms in a (higher) category. So you can define an object to be 0-categorical^[1] if all its identity types are just truth-values; then an arbitrary product of 0-categorical types is again 0-categorical.

In this setup, the type of all vector spaces within some universe will have identity types, so equality of a sort, but not of the objectionable kind — “equality” of vector spaces will exactly be isomorphism between them. The type of beasts over this universe will now be 0-categorical: we will have equality of beasts in the simplest sense. (Also, in this foundation, all beasts will automatically respect isomorphism!)

[1]: The two main definitions of $\|X\|$ I know are “the least ordinal bijective to $X$” (elegant, but requires choice to be defined for all $X$), or “$\{ Y \in V_\alpha\ |\ Y \cong X \}$, where $\alpha$ is minimal such that this is non-empty” (less transparent but more robust).

[2]: I first heard this definition from Voevodsky, though I’m pretty sure it had been considered by others before as well. He calls this property being a set, but I want to make unambiguous that it’s a restriction of categorical dimension not of size.

Classical axiomatic set theories (eg ZFC, NGB) are formulated in first-order logic with equality, so any things you can quantify over (i.e. that you can talk about as actual objects of the language), you can talk about equality of, as a basic given of the language.

In particular, in either ZFC or NGB, you can certainly talk about equality of vector spaces. In ZFC, you can’t talk about beasts as quantify-over-able objects (since they can only be represented as proper classes, not as sets); in NGB, you can, and so you get equality of them.

Cardinality is a bit slipperier: it’s generally considered as a defined rather than a basic notion, and the exact definitions used vary in ways your question will be sensitive to. Most often, an object called the “cardinality” is only specifically defined for sets^[1]; for classes, “C and D have the same cardinality” is considered syntactic sugar for “there is a class-bijection between C and D”. So it’s not quite clear what it means to ask if a class “has cardinality”, but whatever it is depends heavily on having an equality relation on it, to be able to talk about bijections to/from it.

On the other hand, there are some more recent set/type theories in which equality isn’t given, or is a more flexible notion.

In some versions of the Calculus of Constructions, if I remember right, there is a universe of small sets (possibly multiple universes), and an arbitrary product of sets is again a set, possibly in some higher universe (this has to be formulated carefully to avoid inconsistency); and each set has equality on it, but there’s no equality on the universe(s). So there, vector spaces wouldn’t form a set, and wouldn’t have an equality relation; but beasts would form a set (a certain product of hom-sets) so would have an equality relation. (The C of C’s is a little out of what I know, so this may need correcting by someone more knowledgeable.)

Similarly, there are versions of Martin-Löf Type Theory with identity types which address this issue; roughly, identity types can represent something like an ordinary equality relation, but more generally they can also look like the sets/categories of (weak) ismorphisms in a (higher) category. So you can define an object to be 0-categorical^[1] if all its identity types are just truth-values; then an arbitrary product of 0-categorical types is again 0-categorical.

In this setup, the type of all vector spaces within some universe will have identity types, so equality of a sort, but not of the objectionable kind — “equality” of vector spaces will exactly be isomorphism between them. The type of beasts over this universe will now be 0-categorical: we will have equality of beasts in the simplest sense. (Also, in this foundation, all beasts will automatically respect isomorphism!)

[1]: The two main definitions of $\|X\|$ I know are “the least ordinal bijective to $X$” (elegant, but requires choice to be defined for all $X$), or “$\{ Y \in V_\alpha\ |\ Y \cong X \}$, where $\alpha$ is minimal such that this is non-empty.

[2]: I first heard this definition from Voevodsky, though I’m pretty sure it had been considered by others before as well. He calls this property being a set, but I want to make unambiguous that it’s a restriction of categorical dimension not of size.

Classical axiomatic set theories (eg ZFC, NGB) are formulated in first-order logic with equality, so any things you can quantify over (i.e. that you can talk about as actual objects of the language), you can talk about equality of, as a basic given of the language.

In particular, in either ZFC or NGB, you can certainly talk about equality of vector spaces. In ZFC, you can’t talk about beasts as quantify-over-able objects (since they can only be represented as proper classes, not as sets); in NGB, you can, and so you get equality of them.

Cardinality is a bit slipperier: it’s generally considered as a defined rather than a basic notion, and the exact definitions used vary in ways your question will be sensitive to. Most often, an object called the “cardinality” is only specifically defined for sets^[1]; for classes, “C and D have the same cardinality” is considered syntactic sugar for “there is a class-bijection between C and D”. So it’s not quite clear what it means to ask if a class “has cardinality”, but whatever it is depends heavily on having an equality relation on it, to be able to talk about bijections to/from it.

On the other hand, there are some more recent set/type theories in which equality isn’t given, or is a more flexible notion.

In some versions of the Calculus of Constructions, if I remember right, there is a universe of small sets (possibly multiple universes), and an arbitrary product of sets is again a set, possibly in some higher universe (this has to be formulated carefully to avoid inconsistency); and each set has equality on it, but there’s no equality on the universe(s). So there, vector spaces wouldn’t form a set, and wouldn’t have an equality relation; but beasts would form a set (a certain product of hom-sets) so would have an equality relation. (The C of C’s is a little out of what I know, so this may need correcting by someone more knowledgeable.)

Similarly, there are versions of Martin-Löf Type Theory with identity types which address this issue; roughly, identity types can represent something like an ordinary equality relation, but more generally they can also look like the sets/categories of (weak) ismorphisms in a (higher) category. So you can define an object to be 0-categorical^[1] if all its identity types are just truth-values; then an arbitrary product of 0-categorical types is again 0-categorical.

In this setup, the type of all vector spaces within some universe will have identity types, so equality of a sort, but not of the objectionable kind — “equality” of vector spaces will exactly be isomorphism between them. The type of beasts over this universe will now be 0-categorical: we will have equality of beasts in the simplest sense. (Also, in this foundation, all beasts will automatically respect isomorphism!)

[1]: The two main definitions of $\|X\|$ I know are “the least ordinal bijective to $X$” (elegant, but requires choice to be defined for all $X$), or “$\{ Y \in V_\alpha\ |\ Y \cong X \}$, where $\alpha$ is minimal such that this is non-empty” (less transparent but more robust).

[2]: I first heard this definition from Voevodsky, though I’m pretty sure it had been considered by others before as well. He calls this property being a set, but I want to make unambiguous that it’s a restriction of categorical dimension not of size.