Prove that the result of any nested composition of morphisms is independent of the placement of paranthesis.

Solution 1:

What you're "really" doing induction over is full binary trees representing different placements of parentheses. The suggested induction over $n$ isn't an induction over the length of the sequence of arrows but the number of leaves in the full binary tree. There are many full binary trees with $n$ leaves, and you need to prove that all of them can be reassociated into each other.

Let's instead do a structural induction over full binary trees. The theorem to prove is given an arbitrary full binary tree, it can be reassociated to a totally left associated tree.

The base case is a leaf and that's trivially left associated. The inductive case says given a branching node whose two subtrees can be reassociated into totally left associated trees, then we can reassociate this tree into a totally left associated tree. Call the totally left associated left and right subtrees $L$ and $R$ respectively, we have $(LR)$ and we want to show that it can be reassociated into a totally left associated tree. To prove this, we do an induction on the number of leaves in $R$. For the base case, $R = r_1$, we have $(Lr_1)$ which is totally left associated. In the inductive case we have $R = (R_nr_{n+1})$ and thus $(L(R_nr_{n+1}))$. We reassociate that to $((LR_n)r_{n+1})$ and then use the inductive hypothesis on $R_n$ to produce a totally left associated tree $L'$ whence $(L'r_{n+1})$ is then totally left associated and we're done.

Here is a complete formal proof in Agda following the above.