Notice the 'edit' I exported earlier could be reused to simplify the w implementation of the proof that Box is a transitive relation

.gitignore

@@ -1,2 +1,3 @@
 dist*/
 .ghc.environment.*
+cabal.project.local

src/PDF/Box.hs

@@ -25,7 +25,7 @@ modifyAt i f = get >>= edit i f >>= put
 
 instance (Box m i a b, Box m j b c) => Box m (i, j) a c where
   r (i, j) a = r i a >>= r j
-  w (i, j) a c = r i a >>= flip (w j) c >>= w i a
+  w (i, j) a c = edit i (flip (w j) c) a
 
 infixr 6 .@
 (.@) :: a -> b -> (a, b)