From 0d90ad3a40bbd38e6e575977e15b646737f89b58 Mon Sep 17 00:00:00 2001
From: Shreck Ye <ShreckYe@gmail.com>
Date: Fri, 4 Aug 2023 10:40:24 +0800
Subject: [PATCH] =?UTF-8?q?Make=20variables=20names=20=5F=E2=88=99?=
 =?UTF-8?q?=E2=88=99=5F=E2=88=99=E2=88=99=5F=20consistent=20with=20those?=
 =?UTF-8?q?=20in=20doubleComp-faces=20and=20remove=20an=20unnecessary=20sp?=
 =?UTF-8?q?ace?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Cubical/Foundations/Prelude.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda
index a402935890..fa683d5273 100644
--- a/Cubical/Foundations/Prelude.agda
+++ b/Cubical/Foundations/Prelude.agda
@@ -110,12 +110,12 @@ congP₂ f p q i = f i (p i) (q i)
    `doubleCompPath-filler p q r` gives the whole square
 -}
 
-doubleComp-faces : {x y z w : A } (p : x ≡ y) (r : z ≡ w)
+doubleComp-faces : {x y z w : A} (p : x ≡ y) (r : z ≡ w)
                  → (i : I) (j : I) → Partial (i ∨ ~ i) A
 doubleComp-faces p r i j (i = i0) = p (~ j)
 doubleComp-faces p r i j (i = i1) = r j
 
-_∙∙_∙∙_ : w ≡ x → x ≡ y → y ≡ z → w ≡ z
+_∙∙_∙∙_ : x ≡ y → y ≡ z → z ≡ w → x ≡ w
 (p ∙∙ q ∙∙ r) i =
   hcomp (doubleComp-faces p r i) (q i)