Categorical view of loop invariants