diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md
index 7dc0b91d..b96a608a 100644
--- a/src/simplicial-hott/03-extension-types.rzk.md
+++ b/src/simplicial-hott/03-extension-types.rzk.md
@@ -1219,8 +1219,8 @@ The converse is of course trivial.
 
 For simplicity, we only consider extesions of `#!rzk BOT`.
 
-For each map `f : A → B` and each shape inclusion `ϕ ⊂ ψ`,
-we have a commutative square.
+For each map `f : A → B` and each shape inclusion `ϕ ⊂ ψ`, we have a commutative
+square.
 
 ```
 (ψ → A') → (ψ → A)