A formalisation of arrow calculus with operations and effect handlers. The proof works with Agda 2.6.4.