Fix a set of variables $V$, and suppose we're given a presentation of a monosorted algebraic theory, with variable symbols taken from $V$. For the sake of example, suppose the presentation consists of a sort symbol $U$, a function symbol $+ : U \times U \rightarrow U,$ as well as an "explicitly named identity," expressing the commutativity of addition. $$\mathsf{CoA}(x,y) : x+y = y+x$$
We think of our identities as being morphisms, whose domain and codomain are well-formed algebraic expressions. Then there is a corresponding groupoid, whose objects are the well-formed algebraic expressions, and whose arrows are proofs of equality between two expressions.
Question. What is this construction called, how can we rigorously define it, and where can I read about it?
Let me be a little more explicit about what the groupoid looks like in the aforementioned example.
Objects are well-formed algebraic expressions such as $x+y$ and $a+(b+c)$. The variable symbols have to be taken from $V$, of course; I'm assuming that $\{x,y,a,b,c\} \subseteq V$.
Morphisms are proofs that one expression equals another. So for example, we have a morphism $$\mathsf{CoA}(x,y) : x+y = y+x$$ expressing that $x+y$ equals $y+x$; and another morphism $$a+\mathsf{CoA}(x,y) : a+(x+y) = a+(y+x)$$ expressing that $a+(x+y)$ equals $a+(y+x)$; and another morphism $$\mathsf{CoA}(x+y,a) : (x+y)+a = a+(x+y).$$ Furthermore, we can compose these to get a proof $$(\mathsf{CoA}(x+y,a)) \circ (a+\mathsf{CoA}(x,y)) : (x+y)+a = a+(y+x)$$ of the fact that $(x+y)+a=a+(y+x)$.
Note that we can also take inverses; this allows us to get a proof that $\sigma = \tau$ from a proof that $\tau = \sigma$.