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 Sergie 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.)

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.)