Q1: Can it be argued that if we cannot have more than one arrow (morphism) between two objects and morphisms can be composed, then the associativity of morphisms obviously holds since $f\circ(g\circ h)$ cannot be different than $(f\circ g) \circ h$ ?
I need this to prove that the $\subseteq$ relation (which is a partial order in sets using order theory terminology), or any partial order in general, corresponds to a thin category in category theory terminology.
Q2: is there some kind of terminology or theory that expresses or tries to define formally this notion of "equivalent" mathematical objects in different fields of mathematics? E.g. what is the most precise language that conveys the notion that every partial order has a corresponding thin category?
A1: Yes.
(Unnecessarily deep dive presenting an unusual perspective. Feel free to skip. Composition corresponds to transitivity. If we think (in poset terms) of $f : A \to B$ as being proof that $A\leq B$. Then composition takes proof that $A\leq B$ and $B\leq C$ and gives you a proof that $A \leq C$. Associativity then states that two ways of proving $A \leq D$ from proofs of $A\leq B$, $B\leq C$, and $C\leq D$ are equivalent. Of course, "normal" math is proof irrelevant, meaning for any statement, any proof of it is as good as any other. This is what a poset/thin category is like. A normal category then corresponds to a proof relevant context where $A\leq B$ can be true in more than one way.)
A2: Yes, category theory. The original paper introducing category theory was about "natural equivalences". That "precise language" would be a functor from the category of posets and monotone functions, $\mathbf{Pos}$, to the category of small categories, $\mathbf{Cat}$, and the properties of that functor. Or even better, you can make an equivalence of categories between $\mathbf{Pos}$ and $(0,1)\mathbf{Cat}$.