Add some large Grothendieck abelian categories

[ScriptRaccoon]

This PR continues #359 and adds some examples of Grothendieck abelian categories that are not locally ess. small. The goal is to bring down the number of missing combinations (cf. this milestone). In fact, this PR decreases that number from 625 to 495. Jackpot!

The following categories are added:

• [Set_disc, Ab] as a basic example of a Grothendieck abelian category that is not locally ess. small (like the next two)
• [On, Ab] as an example of a Grothendieck abelian category that does not have a cogenerator
• Vect^s_K, the category of large vector spaces over a large field that have a small basis, as an example of a Grothendieck abelian category that is not complete

All properties are decided.

New combinations

Found 130 unique witnessed combinations by the supplied structures (Set_disc_Ab, TransSeqAb, Vect_large):

Directly witnessed:
- Grothendieck abelian ∧ ¬accessible
- CIP ∧ ¬concretizable
- Grothendieck abelian ∧ ¬concretizable
- abelian ∧ ¬concretizable
- additive ∧ ¬concretizable
- biproducts ∧ ¬concretizable
- cokernels ∧ ¬concretizable
- conormal ∧ ¬concretizable
- counital ∧ ¬concretizable
- kernels ∧ ¬concretizable
- normal ∧ ¬concretizable
- pointed ∧ ¬concretizable
- preadditive ∧ ¬concretizable
- unital ∧ ¬concretizable
- zero morphisms ∧ ¬concretizable
- Grothendieck abelian ∧ ¬cototal
- Grothendieck abelian ∧ ¬finitely accessible
- CIP ∧ ¬locally essentially small
- Grothendieck abelian ∧ ¬locally essentially small
- abelian ∧ ¬locally essentially small
- additive ∧ ¬locally essentially small
- biproducts ∧ ¬locally essentially small
- cokernels ∧ ¬locally essentially small
- conormal ∧ ¬locally essentially small
- counital ∧ ¬locally essentially small
- kernels ∧ ¬locally essentially small
- normal ∧ ¬locally essentially small
- pointed ∧ ¬locally essentially small
- preadditive ∧ ¬locally essentially small
- unital ∧ ¬locally essentially small
- zero morphisms ∧ ¬locally essentially small
- Grothendieck abelian ∧ ¬locally finitely multi-presentable
- Grothendieck abelian ∧ ¬locally finitely presentable
- Grothendieck abelian ∧ ¬locally multi-presentable
- Grothendieck abelian ∧ ¬locally poly-presentable
- Grothendieck abelian ∧ ¬locally presentable
- CIP ∧ ¬locally small
- Grothendieck abelian ∧ ¬locally small
- abelian ∧ ¬locally small
- additive ∧ ¬locally small
- biproducts ∧ ¬locally small
- cokernels ∧ ¬locally small
- conormal ∧ ¬locally small
- counital ∧ ¬locally small
- kernels ∧ ¬locally small
- normal ∧ ¬locally small
- pointed ∧ ¬locally small
- preadditive ∧ ¬locally small
- unital ∧ ¬locally small
- zero morphisms ∧ ¬locally small
- Grothendieck abelian ∧ ¬locally ℵ₁-presentable
- Grothendieck abelian ∧ ¬total
- CIP ∧ ¬well-copowered
- Grothendieck abelian ∧ ¬well-copowered
- abelian ∧ ¬well-copowered
- additive ∧ ¬well-copowered
- biproducts ∧ ¬well-copowered
- cokernels ∧ ¬well-copowered
- conormal ∧ ¬well-copowered
- counital ∧ ¬well-copowered
- kernels ∧ ¬well-copowered
- normal ∧ ¬well-copowered
- pointed ∧ ¬well-copowered
- preadditive ∧ ¬well-copowered
- unital ∧ ¬well-copowered
- zero morphisms ∧ ¬well-copowered
- CIP ∧ ¬well-powered
- Grothendieck abelian ∧ ¬well-powered
- abelian ∧ ¬well-powered
- additive ∧ ¬well-powered
- biproducts ∧ ¬well-powered
- cokernels ∧ ¬well-powered
- conormal ∧ ¬well-powered
- counital ∧ ¬well-powered
- kernels ∧ ¬well-powered
- normal ∧ ¬well-powered
- pointed ∧ ¬well-powered
- preadditive ∧ ¬well-powered
- unital ∧ ¬well-powered
- zero morphisms ∧ ¬well-powered
- Grothendieck abelian ∧ ¬ℵ₁-accessible
- Barr-coexact ∧ ¬cogenerating set
- Grothendieck abelian ∧ ¬cogenerating set
- abelian ∧ ¬cogenerating set
- additive ∧ ¬cogenerating set
- coregular ∧ ¬cogenerating set
- normal ∧ ¬cogenerating set
- preadditive ∧ ¬cogenerating set
- Grothendieck abelian ∧ ¬cogenerator
- Grothendieck abelian ∧ ¬extremal cogenerating set
- abelian ∧ ¬extremal cogenerating set
- additive ∧ ¬extremal cogenerating set
- normal ∧ ¬extremal cogenerating set
- preadditive ∧ ¬extremal cogenerating set
- Grothendieck abelian ∧ ¬extremal cogenerator
- Grothendieck abelian ∧ ¬CIP
- Grothendieck abelian ∧ ¬cocartesian cofiltered limits
- Grothendieck abelian ∧ ¬cofiltered limits
- Grothendieck abelian ∧ ¬complete
- split abelian ∧ ¬concretizable
- Grothendieck abelian ∧ ¬connected limits
- Grothendieck abelian ∧ ¬cosifted limits
- Grothendieck abelian ∧ ¬countable powers
- Grothendieck abelian ∧ ¬countable products
- Grothendieck abelian ∧ ¬directed limits
- Grothendieck abelian ∧ ¬disjoint products
- split abelian ∧ ¬locally essentially small
- split abelian ∧ ¬locally small
- Grothendieck abelian ∧ ¬multi-complete
- Grothendieck abelian ∧ ¬powers
- Grothendieck abelian ∧ ¬products
- Grothendieck abelian ∧ ¬sequential limits
- Grothendieck abelian ∧ ¬wide pullbacks
- Grothendieck abelian ∧ ¬ℵ₂-small powers
- Grothendieck abelian ∧ ¬ℵ₂-small products

Dually witnessed:
- CSP ∧ ¬concretizable
- CSP ∧ ¬locally essentially small
- CSP ∧ ¬locally small
- CSP ∧ ¬well-powered
- CSP ∧ ¬well-copowered
- Barr-exact ∧ ¬generating set
- abelian ∧ ¬generating set
- additive ∧ ¬generating set
- regular ∧ ¬generating set
- conormal ∧ ¬generating set
- preadditive ∧ ¬generating set
- abelian ∧ ¬extremal generating set
- additive ∧ ¬extremal generating set
- conormal ∧ ¬extremal generating set
- preadditive ∧ ¬extremal generating set