diff --git a/src/foundation/commuting-squares-of-maps.lagda.md b/src/foundation/commuting-squares-of-maps.lagda.md
index 40bd9a6857..37204c8c65 100644
--- a/src/foundation/commuting-squares-of-maps.lagda.md
+++ b/src/foundation/commuting-squares-of-maps.lagda.md
@@ -404,7 +404,7 @@ W^C -----> W^A -----> W^X
 ```
 
 This fact can be written as distribution of right whiskering over transposition:
-`W^(H ·r f) = W^f ·l W^H`
+`W^(H ·r f) = W^f ·l W^H`.
 
 ```agda
 module _