It's actually not very interesting formulation of category theory. You can't express a category of categories, with isomorphic categories considered equal in this way. Partially, this can be worked around if we state that everything important preserves equivalence (i.e. if A ~ A` and B ~ B` A x B ~ A` x B`). Though, if you want to express this in full generality, you will need Homotopy Type Theory.

But, all in all, even formulating all this and proving theorems was a good exercise. Good job!