From f60761c1529bcac34aff2eedbd57271971ccc3fd Mon Sep 17 00:00:00 2001
From: LuuBluum <bdragun+github@vivaldi.net>
Date: Sat, 7 Sep 2024 20:46:20 +0000
Subject: [PATCH] Fix whitespace

---
 Cubical/Relation/Binary/Order/Poset/Properties.agda | 2 +-
 Cubical/Relation/Binary/Order/Toset/Properties.agda | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

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)