off-by-three

agda · Aug 29, 2022 · 5b372f0 · 5b372f0
1 parent 1eab83b
commit 5b372f0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Cubical/Foundations/Cubes/Base.agda b/Cubical/Foundations/Cubes/Base.agda
@@ -82,7 +82,7 @@ makeCube {n = suc n} a₋ = _ , λ i → a₋ i .snd
 -- A cube is just a path of cubes of one-lower-dimension.
 -- Unfortunately the following function cannot begin at 0,
 -- because Agda doesn't support pattern matching on ℕ towards pre-types.
--- P.S. It will be fixed in Agda 2.9.3 when I → A becomes fibrant.
+-- P.S. It will be fixed in Agda 2.6.3 when I → A becomes fibrant.
 pathCube : (n : ℕ) → (I → Cube (suc n) A) → Cube (suc (suc n)) A
 pathCube n p = _ , λ i → p i .snd