Fix whitespace

agda · Sep 7, 2024 · f60761c · f60761c
1 parent 96d8ccc
commit f60761c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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)