From a69a4226c62c956a0a8eac504439e90ba90a88ec Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 5 Sep 2018 15:11:35 +0200
Subject: [PATCH] reorder arguments of definitions about squares and
 squareovers

This is to be consistent with the order of the type square. These arguments are mostly implicit, with as most notable exception the square(over) fillers.
---
 hott/cubical/cube.hlean       | 16 ++++++++--------
 hott/cubical/square.hlean     |  4 ++--
 hott/cubical/squareover.hlean | 10 ++++------
 3 files changed, 14 insertions(+), 16 deletions(-)

diff --git a/hott/cubical/cube.hlean b/hott/cubical/cube.hlean
index 6d476e058..151413e06 100644
--- a/hott/cubical/cube.hlean
+++ b/hott/cubical/cube.hlean
@@ -204,8 +204,8 @@ namespace eq
   definition cube_fill110 : Σ lid, cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ lid s₁₁₂ :=
   begin
     induction s₀₁₁, induction s₂₁₁,
-    let fillsq := square_fill_l (eq_of_vdeg_square s₁₀₁)
-        (eq_of_hdeg_square s₁₁₂) (eq_of_vdeg_square s₁₂₁),
+    let fillsq := square_fill_l (eq_of_vdeg_square s₁₀₁) (eq_of_vdeg_square s₁₂₁)
+      (eq_of_hdeg_square s₁₁₂),
     apply sigma.mk,
     apply cube_transport101 (left_inv (vdeg_square_equiv _ _) s₁₀₁),
     apply cube_transport112 (left_inv (hdeg_square_equiv _ _) s₁₁₂),
@@ -216,8 +216,8 @@ namespace eq
   definition cube_fill112 : Σ lid, cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ lid :=
   begin
     induction s₀₁₁, induction s₂₁₁,
-    let fillsq := square_fill_r (eq_of_vdeg_square s₁₀₁)
-        (eq_of_hdeg_square s₁₁₀) (eq_of_vdeg_square s₁₂₁),
+    let fillsq := square_fill_r (eq_of_vdeg_square s₁₀₁) (eq_of_vdeg_square s₁₂₁)
+      (eq_of_hdeg_square s₁₁₀),
     apply sigma.mk,
     apply cube_transport101 (left_inv (vdeg_square_equiv _ _) s₁₀₁),
     apply cube_transport110 (left_inv (hdeg_square_equiv _ _) s₁₁₀),
@@ -228,8 +228,8 @@ namespace eq
   definition cube_fill011 : Σ lid, cube lid s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂ :=
   begin
     induction s₁₀₁, induction s₁₂₁,
-    let fillsq := square_fill_t (eq_of_vdeg_square s₁₁₀) (eq_of_vdeg_square s₁₁₂)
-      (eq_of_vdeg_square s₂₁₁),
+    let fillsq := square_fill_t (eq_of_vdeg_square s₂₁₁) (eq_of_vdeg_square s₁₁₀)
+      (eq_of_vdeg_square s₁₁₂),
     apply sigma.mk,
     apply cube_transport110 (left_inv (vdeg_square_equiv _ _) s₁₁₀),
     apply cube_transport211 (left_inv (vdeg_square_equiv _ _) s₂₁₁),
@@ -252,8 +252,8 @@ namespace eq
   definition cube_fill101 : Σ lid, cube s₀₁₁ s₂₁₁ lid s₁₂₁ s₁₁₀ s₁₁₂ :=
   begin
     induction s₁₁₀, induction s₁₁₂,
-    let fillsq := square_fill_t (eq_of_hdeg_square s₀₁₁) (eq_of_hdeg_square s₂₁₁)
-      (eq_of_hdeg_square s₁₂₁),
+    let fillsq := square_fill_t (eq_of_hdeg_square s₁₂₁) (eq_of_hdeg_square s₀₁₁)
+      (eq_of_hdeg_square s₂₁₁),
     apply sigma.mk,
     apply cube_transport011 (left_inv (hdeg_square_equiv _ _) s₀₁₁),
     apply cube_transport211 (left_inv (hdeg_square_equiv _ _) s₂₁₁),
diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean
index cfed932e0..807e8f418 100644
--- a/hott/cubical/square.hlean
+++ b/hott/cubical/square.hlean
@@ -12,10 +12,10 @@ namespace eq
 
   variables {A B C : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A}
             /-a₀₀-/ {p₁₀ p₁₀' : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/
-       {p₀₁ p₀₁' : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ p₂₁' : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂}
             /-a₀₂-/ {p₁₂ p₁₂' : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/
-       {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄}
             /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/
+       {p₀₁ p₀₁' : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ p₂₁' : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂}
+       {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄}
             {b : B} {c : C}
 
   inductive square {A : Type} {a₀₀ : A}
diff --git a/hott/cubical/squareover.hlean b/hott/cubical/squareover.hlean
index 3513536be..8168330a8 100644
--- a/hott/cubical/squareover.hlean
+++ b/hott/cubical/squareover.hlean
@@ -28,10 +28,10 @@ namespace eq
   variables {A A' : Type} {B : A → Type}
             {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ : A}
             /-a₀₀-/ {p₁₀ : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/
-       {p₀₁ : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂}
             /-a₀₂-/ {p₁₂ : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/
-       {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄}
             /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/
+       {p₀₁ : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂}
+       {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄}
             {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} {s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁}
             {s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃} {s₃₃ : square p₃₂ p₃₄ p₂₃ p₄₃}
 
@@ -40,10 +40,10 @@ namespace eq
             {b₀₂ : B a₀₂} {b₂₂ : B a₂₂} {b₄₂ : B a₄₂}
             {b₀₄ : B a₀₄} {b₂₄ : B a₂₄} {b₄₄ : B a₄₄}
             /-b₀₀-/ {q₁₀ : b₀₀ =[p₁₀] b₂₀} /-b₂₀-/ {q₃₀ : b₂₀ =[p₃₀] b₄₀} /-b₄₀-/
-   {q₀₁ : b₀₀ =[p₀₁] b₀₂} /-t₁₁-/ {q₂₁ : b₂₀ =[p₂₁] b₂₂} /-t₃₁-/ {q₄₁ : b₄₀ =[p₄₁] b₄₂}
             /-b₀₂-/ {q₁₂ : b₀₂ =[p₁₂] b₂₂} /-b₂₂-/ {q₃₂ : b₂₂ =[p₃₂] b₄₂} /-b₄₂-/
-   {q₀₃ : b₀₂ =[p₀₃] b₀₄} /-t₁₃-/ {q₂₃ : b₂₂ =[p₂₃] b₂₄} /-t₃₃-/ {q₄₃ : b₄₂ =[p₄₃] b₄₄}
             /-b₀₄-/ {q₁₄ : b₀₄ =[p₁₄] b₂₄} /-b₂₄-/ {q₃₄ : b₂₄ =[p₃₄] b₄₄} /-b₄₄-/
+   {q₀₁ : b₀₀ =[p₀₁] b₀₂} /-t₁₁-/ {q₂₁ : b₂₀ =[p₂₁] b₂₂} /-t₃₁-/ {q₄₁ : b₄₀ =[p₄₁] b₄₂}
+   {q₀₃ : b₀₂ =[p₀₃] b₀₄} /-t₁₃-/ {q₂₃ : b₂₂ =[p₂₃] b₂₄} /-t₃₃-/ {q₄₃ : b₄₂ =[p₄₃] b₄₄}
 
   definition squareo := @squareover A B a₀₀
   definition idsquareo [reducible] [constructor] (b₀₀ : B a₀₀) := @squareover.idsquareo A B a₀₀ b₀₀
@@ -311,8 +311,6 @@ namespace eq
     squareover B s q q₁₂ q₀₁ (q' ⬝o q₂₁) :=
   begin induction q', induction q, induction q₂₁, exact t end
 
-  /- TODO: replace the version in the library by this -/
-
   variables (s₁₁ q₀₁ q₁₀ q₂₁ q₁₂)
   definition squareover_fill_t : Σ (q : b₀₀ =[p₁₀] b₂₀), squareover B s₁₁ q q₁₂ q₀₁ q₂₁ :=
   begin