In algebra, monads are used to reify the notion of an "explicit expression". So you have the integers, Z, and the monad m gives m(Z), the set of expressions (let's say sums) over Z. And then you have m(m(Z)) which is nested expressions and so on. An algebra for a monad evaluates an expression m(Z)->Z, and all the monad laws basically enforce the kind of equational reasoning ordinary notation takes for granted (eg sub-expressions can be replaced by their value, 1+(1+1)=1+2).

So those would be related in this way

                       join
  (1)+(1+1) : m(m(Z)) -----> 1+1+1 : m(Z)
             |                 |
  fmap(eval) |                 | eval
             v                 v
       1+2 : m(Z) -----------> 3 : Z
                    eval

That's the "infinity": ordinary (1-)categories have (1-)arrows between objects, 2-categories have 2-arrows between 1-arrows, 3-categories have 3-arrows between 2-arrows, and so on. Infinity-categories have (k+1)-arrows between k-arrows all the way up. (And a 0-category is just a set: objects, but no arrows)

> Is (1+(1+1)) the same amount of equivalence to 3 as 1+2 is? I'd much prefer a notion that could look at how 'equivalent' terms are opposed to just looking at equality after β-reduction.

"Amounts" of equivalence between terms isn't really the right notion here: there's not much you can do with "an equivalence exists", which is all that "X and Y are equivalent" really means. A 2-equivalence (which in this context I think is going to end up being something like a rewrite rule?) should be an equivalence between particular programs, not the whole space of programs implementing a given function.

There is such a notion. You write a number on the equality sign saying essentially how many operations can be performed so 1+2 is equal to 3 if that number is larger than 0 (the special case of 0 is reflexivity, i.e. true equality). This is used a lot in some computer science stuff I've seen.

thanks for letting me know, do you know if there's a term for that notation?