whitespace fix

agda · Jan 22, 2025 · 522673c · 522673c
1 parent 8a6e91b
commit 522673c
Show file tree

Hide file tree

Showing 3 changed files with 139 additions and 115 deletions.
diff --git a/Cubical/Data/Rationals/Order/Properties.agda b/Cubical/Data/Rationals/Order/Properties.agda
@@ -1374,15 +1374,15 @@ q ／ℚ[ r , 0＃r ] = q · (invℚ r 0＃r)
 
 ℚ-x/y<z→x/z<y : ∀ x q r  → (0<x : 0 < x) → (0<q : 0 < q) → (0<r : 0 < r)
                → (x ／ℚ[ r , inl 0<r ]) < q
-               → (x ／ℚ[ q , inl 0<q ]) < r 
+               → (x ／ℚ[ q , inl 0<q ]) < r
 ℚ-x/y<z→x/z<y x q r 0<x 0<q 0<r p =
  subst2 _<_ (sym (·Assoc _ _ _)
    ∙  cong (x ·_) ((·Comm _ _) ∙
      cong (_· invℚ r (inl 0<r)) (·Comm _ _) ∙
       ℚ-[x·y]/y _ _ _ ) )
    ((·Comm _ _) ∙ ℚ-[x/y]·y _ _ _)
    (<-·o (x ／ℚ[ r , (inl 0<r) ]) q (r ／ℚ[ q , (inl 0<q) ])
-     (0<-m·n _ _ 0<r (invℚ-pos q (inl 0<q)  0<q)) p) 
+     (0<-m·n _ _ 0<r (invℚ-pos q (inl 0<q)  0<q)) p)
 
 invℚ≤invℚ : ∀ (p q : ℚ₊) → fst q ≤ fst p → fst (invℚ₊ p) ≤ fst (invℚ₊ q)
 invℚ≤invℚ p q x =

diff --git a/Cubical/HITs/CauchyReals/Derivative.agda b/Cubical/HITs/CauchyReals/Derivative.agda
@@ -97,7 +97,7 @@ IsContinuousInclLim≃IsContinuous : ∀ f  →
 IsContinuousInclLim≃IsContinuous f =
   propBiimpl→Equiv (isPropΠ2 λ _ _ → squash₁) (isPropIsContinuous f)
     (IsContinuousInclLim→IsContinuous f)
-     λ fc x → IsContinuousInclLim f x fc   
+     λ fc x → IsContinuousInclLim f x fc
 
 IsContinuousLimΔ : ∀ f x → IsContinuous f →
                     at 0 limitOf (λ Δx _ → f (x +ᵣ Δx)) is (f x)