Foundations of Category Theory; The Axioms As I have been pursuing algebraic geometry over the last two years I have slowly developed some language of category theory to the point where category theory, in some sense, ‘seems natural’, because now it feels motivated by its interaction with algebraic geometry. Recently I have started skimming some books on general category theory, and I have some related questions pertaining to the axioms and definition of a category. I am using the definition given on Wikipedia. 
Most of my questions that follow are irrelevant as long as the category is ‘naturally arising’ in some way (e.g. at least locally small) and the morphisms are some familiar way of connecting objects (e.g. functions), so I ask my questions geared towards a completely arbitrary category, C, such that all of the data and axioms in the Wikipedia definition is satisfied. 


*

*Each part of the definition requires specifying a class of something (objects or morphisms). Is there a standard formalization of a proper class that is used in category theory? If not, is there some canonical way to think of a proper class that is sufficient for having a firm foundation for category theory? 

*By specifying my class of morphisms, we have the hom class, hom(a,b) (a subclass?), for any objects a and b. To define a category one must also specify how to compose morphisms. In a usual setting, specifying the morphisms alone usually carries this information without mention. This is the requirement that we have a binary operation hom(a,b) $/times$ hom(b,c) /to hom(a,c). My question here is, is the notion of cartesian product and binary operation formalized for proper classes? Can you just ‘localize’ the proper class to be a set in any specific place as needed? 
Also, for a long time I interpreted this axiom as essentially saying that anytime I have the morphisms f: A —> B, and g: B —> C, I necessarily have a commutative triangle where the diagonal arrow is $g /circ f$. Is this an acceptable way to think of this? I.e, if I specified some morphisms that had a natural way to be composed associatively (like functions of sets), but I perversely specified my binary composition operation to be something unusual, yet satisfying associativity and identity, it wouldn’t effect the fact that I have a commutative triangle because the composition operation I defined is the one the category would use to determine what diagrams are commutative and which aren’t? I.e the actual composition function in the usual sense $g /circ f$ may be a morphism in my hom class, but I have defined $g /circ f$ to be something different, is the triangle I get still considered commutative? I hope this question is clear, sorry for being confusing. 

*Lastly, the associativity axiom and the identity axiom both use the symbol “=“ as a connective between elements of the hom class (I don’t know anything about classes, I assume element is still used to mean something “in” the class?). Is this notion of “=“ something that is determined by how I have specified my hom class? For example, if morphisms are usual set theoretic functions, then we have a natural way to check if two functions are the same using the “subset of Cartesian product” definition, since the first axiom of ZFC tells us exactly what it means for two sets to be the equal. Then two such functions would be the “same” / “=“ in the sense that they represent the same element of my hom class, because I determined the truth of “f = g” using the “=“ determined by ZFC axiom 1. However, in this axiom, how the truth value is decided partially only clear since we only allow sets as elements, so when we compare elements of sets we always have the axiom to decide if two elements are equal. In usual Mathematics my elements could be anything. So how should I interpret the meaning of “=“ in the axioms of identity and associativity? Does it depend on the objects I define to be morphisms (depends of the specification of Hom class)? Does it depend on a logic (logical / first order characterizations using properties for what “=“ means)? Or is it actually a category theoretic notion of “=“, in the sense that we could characterize the equality of two morphisms by some universal property? 
Edit: 
Or is category theory avoiding these foundational issues by not making these things precise, and that it is just the case that if C Is some category, then “id $/circ f$ = f” is a true statement in whatever logic or interpretation has been chosen? 
Also, I’m really sorry my question is so sloppy. I’m on my phone right now but will be on a computer soon and polish this up a bit. 
 A: There are at least two well known set theories that can handle proper classes:


*

*NBG set theory (named after von Neumann, Bernays, Gödel). This is a conservative extension of ZFC, meaning that it proves the same sentences about sets as ZFC, but also handles proper classes. 

*MK set theory (named after Morse and Kelley, this is the set theory in the appendix of Kelley's General Topology). This is a stronger theory than NBG. For example, MK proves the consistency of ZFC while NBG does not. 
Either of these set theories can be used to formalize proper-class size categories such as Group, Set, etc.  In these categories, of course, the collection of objects and the collection of morphisms are proper classes.
The more challenging thing is when we begin to look at iterated universes: a universe of set theory contained inside a universe of set theory contained inside a universe of set theory, and so on.  
In this case, rather than trying to have a hierarchy of different kinds of proper classes, we typically use a hierarchy of inaccessible cardinals, so that each universe is the collection of sets whose rank is below one of these inaccesibles. This can be done directly in ZFC with an extra axiom "every cardinal is below some inaccessible cardinal", without the need to actually have proper classes.   So there is no issue finding formal systems of set theory that are strong enough to formalize category theory.  
A: 1) There isn't a standard formalisation of a proper class. Typically, this doesn't matter much, and when it does it is common to assume a hierarchy of Grothendieck universes to specify what is small relative to what. 
2) For the first part, cartesian products and relations are implicitly assumed to exist. More explicitly, this is taken care of by the Grothendieck universes. For the second part of the question, yes, your understanding is correct. The morphisms don't even need to be functions and the composition need not be anything in particular. It can be anything at all as long as the axioms hold. This is the same standard understanding in algebra generally. I.e., you can define a binary operation on, say,  $\mathbb N$ that has nothing to do with usually addition, but if the group axioms are satisfied, then it's a group. 
3) Category theory treats equality, in this context, just like the rest of mathematics. Without getting too philosophical, a notion of equality on a class is simply an equivalence relation on it which we take to mean for us that things that are equivalent are identical. There need not be a mechanism for testing for equality as part of the category theoretic machinery. 
Largely, yes, category theory avoids all of that since it is not the (primary) aim of category theory to get boggled down with such tedious details. It has more pressing business to attend to. 
