In the implementation of the prelude for cubical agda, there is a definition of 3 component path composition
_∙∙_∙∙_ : w ≡ x → x ≡ y → y ≡ z → w ≡ z
This definition feels reasonably natural and clean to me. But then to get the 2 component path composition operator there are 3 choices: One for fixing each of the arguments as refl.
The standard ∙ is done by fixing the first argument, and another implementation (∙') is given for fixing the third argument. There is then a proof that they are the same. But the version fixing the 2nd argument is not discussed.
It seems to me that the 2nd argument version (call it ∘) has a nice property that
sym (p1 ∘ p2) is equal to sym p2 ∘ sym p1 definitionally. This seems like it can reduce the book keeping in some proofs.
Are there reasons why this version is not the standard version? Are there other computational properties that are better with the standard version?