The groupoid of algebraic expressions and proofs 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$.
 A: That kind of algebraic manipulation and composition of proofs has strong affinities and resemblence to Justification Logic, where for example one write $s:A$ to mean that $s$ is a justification (or "proof") of $A$, and then there is a composition process by which from $s:A$ and $t:A\to B$,  you may deduce $s\cdot t:B$, where $s\cdot t$ is the compositional process for implementing modus ponens. One then has other such operations, such as:


*

*from $s:A$ and $t:B$, deduce $(s+t):A$ and $(s+t):B$. 

*from $s:A$ you may deduce $!s:s:A$. 


So $s+t$ is the justification of either $A$ or $B$, and $!s$ is the proof that $s$ proves $A$. Justification logic also provides a concept of proof constant that is similar to your use of CoA(x,y).
In this way, justification logic is the logic of reasoning with explicit justifications. The idea was first suggested by Gödel, but carried further by Sergei Artemov. 
(Although I find a strong resemblence between your proposal and justification logic, I am not aware of any treatment of justification logic that uses the kind of category-theoretic language you suggest.)
I just attended yesterday a seminar talk by Mel Fitting on this topic, and he mentioned that he had a number of programs available on his web page for implementing explicit manipulation of this justification algebra. (Mel Fitting was the winner of the Herbrand prize a few years ago for automated theorem proving.)
A: The construction you describe seems more like the the category of reductions generated by the abstract rewrite system given by an algebraic theory.
I suggest you take a look to section 8.2("Rewrite systems revisited") of  Term Rewriting System where these concepts are defined.
Here a short summary of basic the idea: you can consider a rewrite system as a graph whose vertex are terms of the signature and arrows are step of reduction.
From this data enclosing by some operations you get what in the reference is called an abstract rewrite system with compositions, whose objects are terms for the signature and whose morphisms are proof of reductions. Quotienting this structure for axioms of category you get the category of reductions.
Hope this helps.
A: I don't have any direct reference for the notion that you are describing, however the notions of $E_n$-algebras and (topological) operads are very close. Firstly, you should note that you need equalities of higher orders, i.e. not only a proof that $a+(b+c) = (a+b)+c$, but also higher coherence laws between such proofs, like the MacLane pentagon. Let me use the language of type theory. In type theory for any $X: Type$ we have a 2-parametic type family $x,y: X \vdash x =_X y : Type$. An element of such type is a proof of equality between $x$ and $y$. It can be defined inductively as a universal 2-parametric type family generated by $x:X \vdash refl_x : x = x$. The details don't matter here, what matters is that for any $p,q: x=y$ you also have a type $p=q : Type$ et cetera. Thus it is obvious that to specify your algebraic structure you must also specify elements like $s: p=q$, where $p$ and $q$ are two different associativity morphisms $((a+b)+c)+d = a + (b+ (c+d))$.
A more-or-less universal example of such hierarchical object is a topological space (better, a simplicial set). That is, we interpret types as spaces, elements of types as points in spaces and equality types as the space of paths between two points. There are some technical issues, but the picture is like this. Formally such a structure is called $\infty$-groupoid. An $\infty$-groupoid is like a set but even better, since it carries information about the ways that we can identify its points. In particular, we can define many categorical notions with $\infty$-groupoids instead of sets, like $\infty$-categories (categories enriched over $\infty$-groupoids) and $\infty$-Lawvere theories. A particular case of $\infty$-Lawvere theories is the theory of (topological) operads and things like $E_n$-structures. There is actually quite a bit of technical issues to make it all work, but they can be overcome. A possible (but very intimidating) reference is the books "Higher topos theory" and "Higher algebra" by J. Lurie.
You can simplify the theory of $\infty$-groupoids by passing to n-truncation. A 0-truncation is just the category of sets: any two paths $p,q: x=y$ between $x,y: X$ are defined to be trivially equal. A 1-truncation is a 0-truncation on the level of paths, i.e. for any $x,y:X$ and $p,q:x=y$ we define that $p=q$ is just a set (all its paths are trivial). An n-truncation is defined inductively as (n-1)-truncation on the level of paths, but it quickly gets complicated. Note that 1-truncation of $Type$ is just the category of groupoids in the classical sense, i.e. categories such that any morphism is invertible. In this simple case you don't need the full-blown theory of $\infty$-groupoids and can specify all relations explicitly. For example, if you describe the 1-truncated theory of monoids, then you will come to the notion of a monoidal category. An analogue of abelian monoids is the notion of symmetric monoidal category, and there is also an intermediary ($E_2$) case of braided monoidal categories.
In summary, you need the notion of (probably multisorted) Lawvere theories enriched in groupoids. This structure remembers all the explicit relations that you want to specify. While you are more interested in the groupoidal structure, it makes sense to consider a Lawvere theory as a whole, since you should anyway explicitly define you n-ary operations that you are discussing.
A: What is this construction called, how can we rigorously define it, and where can I read about it?
For starters, it's a category and not usually a groupoid because the morphisms need not be invertible and even for a theory with a single sort $X$ you need objects standing for $X^2$, $X^3$, ... in order to take account of binary, ternary, ... operations.
This category is known as a Lawvere theory and was introduced in his PhD thesis c1963. Such a category has finite products, although it is sometimes presented as its opposite, having coproducts instead.
The hom-sets $Law_T(X^n,X)$ of this category, ie the sets of all expressions in $n$ variables, had previously been known in Universal Algebra under the name of clone. I think this idea was due to Peter Hall.
The universal property of the Lawvere theory $Law_T$ is that models (algebras) for the theory $T$ in any category $C$ with finite products correspond naturally and bijectively to product-preserving functors $Law_T\to C$.
We can generalise from finite products to finite limits and the corresponding notion is called an essentially algebraic theory.  A leading example is that of categories.
However, such theories are often better described as dependently typed.  For example, a category qua essentially algebraic theory has a single type of all morphisms, with conditional composition, whereas it is more natural to take the dependent type $C(x,y)$ where $x$ and $y$ range over the type of objects.
Dependently typed theories with singletons and equality types are equivalent to essentially algebraic theories.  Without these, these is a class of distinguished display maps that needs to be closed under pullbacks. These were introduced in my PhD theses and described more (accurately and) fully in Chapter VIII of my book Practical Foundations of Mathematics (CUP, 1999).
A similar construction also lends itself to type-theoretic constructors such as quantifiers, as is described in Chapter IX of the book.   I describe the category as that of contexts and substitutions.
