Categorical structure is a source of great guidance in Type-Directed Development, despite the fact that today’s advanced type systems do a relatively poor job of expressing it. Meanwhile, recent progress in typed languages for algebraic effects and handlers do a less than perfect job of capturing the coherences which handlers for effectful operations should respect. The problem, as ever, is equality, but Cubical Type Theory offers an opportunity to improve the situation, by changing the way in which coherence properties are captured and ensuring uniformity in the treatment of things and of the equations which relate things. Correspondingly, I will offer grounds for optimism.