Inconsistent use of i/j between diagrams and code in definition of Square

[juliapath]

Below is the diagram preceding the definition of Square in 1Lab.Path.

However, a value sq : Square p q s r, is usually used as sq i j, so that i corresponds to j in the diagram and j to i. This incongruence already happens in the definition of Square immediately following the diagram:

Square p q s r = PathP (λ i → p i ≡ r i) q s

I'd like to change the diagram so that i runs vertically along p and r and j horizontally along q and s. Further I'd like to change most other diagrams in 1Lab.Path so that i consistently parameterizes the vertical direction and j the horizontal, either just swapping i and j or transposing the whole diagram where necessary to avoid changing code.

Should I go forward preparing a PR?

[plt-amy]

A PR on this would be welcomed. To be honest, I'm very bad at any sort of visual thinking, so any diagrams I commit are slapped together post-facto, and I think that's responsible for most of these inconsistencies.