minor edit

rzk-lang · Nov 11, 2023 · a3c4139 · a3c4139
1 parent 95fe8f3
commit a3c4139
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md
@@ -440,13 +440,13 @@ Furthermore, we observe that the pair `left-leg-of-Δ ⊂ Δ¹×Δ¹` is the pro
 `Δ¹` with the left anodyne pair `{0} ⊂ Δ¹`, hence left anodyne itself.
 
 ```rzk
-#def is-left-anodyne-left-leg-of-Λ-Δ¹×Δ¹
+#def is-left-anodyne-left-leg-of-Λ-Δ¹×Δ¹ uses (extext)
   : is-left-anodyne ( 2 × 2)
     ( \ ts → Δ¹×Δ¹ ts) ( \ ts → left-leg-of-Λ ts)
   :=
-  \ A' A α is-left-fib-α →
+  \ A' A α →
     is-right-orthogonal-to-shape-product extext A' A α
-      2 Δ¹ 2 Δ¹ ( \ s → s ≡ 0₂) is-left-fib-α
+      2 Δ¹ 2 Δ¹ ( \ s → s ≡ 0₂)
 ```
 
 Next, we use the left cancellation of left anodyne shape inclusions to deduce