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