Make variables names _∙∙_∙∙_ consistent with those in doubleComp-faces and remove an unnecessary space

[ShreckYe]

Hi Maintainers, I am new to Cubical Agda. The variable name order of "x", "y", "z", and "w" is different in the functions _∙∙_∙∙_ and doubleComp-faces which the former depends on, thus "p" and "r" in 2 functions have different types in reading. This confuses beginners like me when I learn their implementations for the first time.
I also notice that throughout the library the order of such plain letter variables is different in different functions. Maybe a rule/guideline of a canonical order can be enforced to reduce these confusions. Or ignore me if it's just a trivial beginner problem.

[MatthiasHu]

Thanks! Merging.

[MatthiasHu]

I also notice that throughout the library the order of such plain letter variables is different in different functions. Maybe a rule/guideline of a canonical order can be enforced to reduce these confusions.

There is indeed a lot of inconsistency (in style, naming, ...) in the library. I personally can't imagine a reasonable guideline to decide between "x y z w" and "w x y z". But if you find something that confuses or annoys you and you can fix it quickly, then I do think it is nice to make a PR out of it.