w

aljungstrom · Jun 8, 2023 · 227b10b · 227b10b
1 parent 3acc6b8
commit 227b10b
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda
@@ -171,7 +171,6 @@ compPath-filler' {z = z} p q j i =
                  ; (i = i1) → q k
                  ; (j = i0) → q (i ∧ k) })
         (p (i ∨ ~ j))
-
 -- Note: We can omit a (j = i1) case here since when (j = i1), the whole expression is
 --  definitionally equal to `p ∙ q`. (Notice that `p ∙ q` is also an hcomp.) Nevertheless,
 --  we could have given `compPath-filler p q k i` as the (j = i1) case.