Update src/hott/08-families-of-maps.rzk.md

Co-authored-by: Nikolai Kudasov <fizruk@users.noreply.github.com>
rzk-lang · Jul 23, 2024 · 8bf2fbe · 8bf2fbe
1 parent 6bc3790
commit 8bf2fbe
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md
@@ -789,8 +789,8 @@ contractible.
 
 The proof of `weakfunext-funext` from `06-contractible.rzk` works with a weaker
 version of function extensionality only requiring the map in the converse
-direction. We can then prove a cycle of implications between FunExt, NaiveFunExt
-and WeakFunExt.
+direction. We can then prove a cycle of implications between `#!rzk FunExt`, `#!rzk NaiveFunExt`
+and `#!rzk WeakFunExt`.
 
 ```rzk
 #def NaiveFunExt