diff --git a/Cubical/Relation/Binary/Order/Poset/Properties.agda b/Cubical/Relation/Binary/Order/Poset/Properties.agda
index 62799609a..8c38c1762 100644
--- a/Cubical/Relation/Binary/Order/Poset/Properties.agda
+++ b/Cubical/Relation/Binary/Order/Poset/Properties.agda
@@ -356,7 +356,7 @@ IsPosetEquivRespectsJoin : {P : Poset ℓ₀ ℓ₀'} {S : Poset ℓ₁ ℓ₁'}
                                  (equivFun (e .fst) a)
                                  (equivFun (e .fst) b)
                                  (equivFun (e .fst) a∨b)
-                                 
+
 IsPosetEquivRespectsJoin {P = P} {S = S} (e , posEq) a b a∨b
   = propBiimpl→Equiv (isPropIsJoin proP a b a∨b)
                      (isPropIsJoin proS (equivFun e a) (equivFun e b) (equivFun e a∨b))
diff --git a/Cubical/Relation/Binary/Order/Toset/Properties.agda b/Cubical/Relation/Binary/Order/Toset/Properties.agda
index 7bc73dde9..2bb17ea38 100644
--- a/Cubical/Relation/Binary/Order/Toset/Properties.agda
+++ b/Cubical/Relation/Binary/Order/Toset/Properties.agda
@@ -143,8 +143,8 @@ module _
 
   private
       pos = isToset→isPoset tos
-      
-      pre = isPoset→isProset pos  
+
+      pre = isPoset→isProset pos
 
       prop = IsToset.is-prop-valued tos
 
@@ -159,7 +159,7 @@ module _
   module _
     {P : Embedding A ℓ''}
     where
-    
+
     private
       toA = fst (snd P)