diff --git a/src/foundation/propositional-extensionality.lagda.md b/src/foundation/propositional-extensionality.lagda.md
index 0974810076..f8ffcf3422 100644
--- a/src/foundation/propositional-extensionality.lagda.md
+++ b/src/foundation/propositional-extensionality.lagda.md
@@ -118,7 +118,6 @@ pr2 (Prop-Set l) = is-set-type-Prop
 
 ### The canonical type family over `Prop` is univalent
 
-
 ```agda
 is-univalent-type-Prop : {l : Level} → is-univalent (type-Prop {l})
 is-univalent-type-Prop {l} P =