w

Cubical/Foundations/Prelude.agda

@@ -172,13 +172,6 @@ compPath-filler' {z = z} p q j i =
                  ; (j = i0) → q (i ∧ k) })
         (p (i ∨ ~ j))
 
-compPath-filler'-filler : (p : x ≡ y) (q : y ≡ z) → (i j k : I) → _
-compPath-filler'-filler {z = z} p q j i k =
-  hfill (λ k → λ { (i = i0) → p (~ j)
-                 ; (i = i1) → q k
-                 ; (j = i0) → q (i ∧ k) })
-        (inS (p (i ∨ ~ j)))
-        k
 -- 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.