Fixed typo.

agda · Feb 6, 2025 · 496aed8 · 496aed8
1 parent 2985e55
commit 496aed8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Categories/Diagram/Pullback/Properties.agda b/src/Categories/Diagram/Pullback/Properties.agda
@@ -194,7 +194,7 @@ module IsoPb {X Y Z} {f : X ⇒ Z} {g : Y ⇒ Z} (pull₀ pull₁ : Pullback f g
 -- pasting law for pullbacks:
 -- in a commutative diagram of the form
 -- A -> B -> C
--- |     |     |
+-- |    |    |
 -- D -> E -> F
 -- if the right square (BCEF) is a pullback,
 -- then the left square (ABDE) is a pullback