white space errors

Author: rw111

Cubical/Data/Rationals/MoreRationals/QuoQ/Extras.agda

@@ -6,7 +6,7 @@ open import Cubical.Data.Int.MoreInts.QuoInt renaming (_·_ to _ℤ·_)
 open import Cubical.Data.Int as Int renaming (ℤ to Int)
 open import Cubical.Foundations.Prelude
 
-open import Cubical.HITs.SetQuotients 
+open import Cubical.HITs.SetQuotients
 
 open import Cubical.Relation.Binary.Base
 open BinaryRelation
@@ -22,7 +22,7 @@ iso/rHlp (z , n) = ∼≡-lemma (Int→ℤ (ℤ→Int z)) z n (ℤ→Int→ℤ z
 Int≡Int→ℤ·≡ℤ· : ∀ x y → x Int.· (Rationals.ℕ₊₁→ℤ y) ≡ ℤ→Int ((Int→ℤ x) ℤ· (Quo.ℕ₊₁→ℤ y))
 Int≡Int→ℤ·≡ℤ· x y = (cong₂ (λ u v → u Int.· v) (sym (Int→ℤ→Int x)) refl) ∙
                      sym (ℤ→IntIsHom· (Int→ℤ x) (Quo.ℕ₊₁→ℤ y))
-                     
+
 ∼'→R* : ∀ u v → (u Rationals∼ v) → R* {ER = Quo.isEquivRel∼}
                                 {iso/r = iso/R (λ x → ℤ→Int (fst x) , (snd x))
                                   (λ x → (Int→ℤ (fst x)) , (snd x)) λ u → iso/rHlp u} u v