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

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.