make usage of extext explicit

rzk-lang · Oct 14, 2023 · b84295e · b84295e
1 parent 3098910
commit b84295e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
@@ -1896,7 +1896,7 @@ Segal type. This is an instance of a general statement about types with unique
 extensions for the shape inclusion `Λ ⊂ Δ²`.
 
 ```rzk
-#def is-fiberwise-segal-are-segal
+#def is-fiberwise-segal-are-segal uses (extext weakextext)
   ( A B : U)
   ( f : A → B)
   ( is-segal-A : is-segal A)