@BoazC ⍣ is a dyadic operator, so it binds +/ on the left and ≡ on the right. It then applies +/ continuously until a≡b (i.e. dyadic ≡) where a and b are two successive results from the +/ application. No connection to monadic ≡
I’m not sure you need more of an explanation but the reduce operator uses its operand to reduce the rank of the argument to the derived function. So if you only had +/a you’d get back a 2D matrix from summing across the final axis of the 3D array a. ⍣ says apply this derived function as @Adám described.
After one step it compares the original argument to the result of a single application of +/. Since the aren’t equal it applies it again to get a 1D vector. Still not the same so another application to give a scalar. Still not the same (remember the last result was 1D) so one more application but +/ on a scalar returns the same scalar and now this is the same as the last result and the function completes.
