We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 5479bcf commit 861451eCopy full SHA for 861451e
Cubical/Foundations/Function.agda
@@ -182,4 +182,3 @@ homotopyIdComm {f = f} H a i j = hcomp (λ k → λ where
182
(j = i0) → f (H a (~ k ∧ ~ i))
183
(j = i1) → H a (~ k)
184
) (H (H a (~ i ∨ j)) j)
185
-
0 commit comments