diff --git a/src/foundation/commuting-squares-of-maps.lagda.md b/src/foundation/commuting-squares-of-maps.lagda.md
index ef6fc87e7c..40bd9a6857 100644
--- a/src/foundation/commuting-squares-of-maps.lagda.md
+++ b/src/foundation/commuting-squares-of-maps.lagda.md
@@ -396,7 +396,6 @@ X -----> A -----> B
 and transposing it by precomposition results in the square
 
 ```text
-
 W^D -----> W^B
  |          |
  |   W^H    |
diff --git a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md
index 4c67bbdee3..320a2039cb 100644
--- a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md
@@ -755,7 +755,7 @@ module _
     universal-property-pushout-pullback-property-pushout l f g
       ( h , k , bottom)
       ( λ W →
-       is-pullback-top-is-pullback-bottom-cube-is-equiv
+        is-pullback-top-is-pullback-bottom-cube-is-equiv
           ( precomp h' W)
           ( precomp k' W)
           ( precomp f' W)