Correct picture in Cubical/PathSquare

[Alizter]

The following picture in Cubical/PathSquare.v

x001----pi01----x101              x001----pi01----x101      
 |  \               \              |               |  \     
 |  p00i  ==si0i=>  p10i           |               |  p10i  
p0i1  \               \           p0i1 ==sii1=>   p1i1  \   
 |    x000----pi00----x100         |               |    x100
 |s0ii |               |    ===>   |               | s1ii|  
x011   |               |          x011----pi11----x111   |  
  \   p0i0  ==sii0=>  p1i0          \               \   p1i0
 p01i  |               |           p01i  ==si1i=>  p11i  |  
     \ |               |               \               \ |  
      x010----pi10----x110              x010----pi10----x110

is a bit misleading to how we have set cubes up. s0ii is the left face and sii0 is the top face, however currently the picture shows it to be at the front. This also means that the left half-cube in the picture is really the back of the cube rather than the front. We need to update this picture so it more correctly reflects what we are really doing in the library.

[Alizter]

Actually it seems that Cube left right front back top bottom should really be Cube left right back front top bottom.

[Alizter]

I'm closing this as there is nothing really actionable to do here. We don't use cubes so often and when we do it can be reasoned about without having to consult the diagram anyway.