diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda
index d8e3587..b1ad4ca 100644
--- a/Lattice/AboveBelow.agda
+++ b/Lattice/AboveBelow.agda
@@ -11,11 +11,13 @@ open import Data.Empty using (⊥-elim)
 open import Data.Product using (_,_)
 open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc)
 open import Function using (_∘_)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl)
+open import Relation.Binary.PropositionalEquality as Eq
+    using (_≡_; sym; subst; refl)
 
 import Chain
 
-open IsEquivalence ≈₁-equiv using () renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
+open IsEquivalence ≈₁-equiv using ()
+    renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
 
 data AboveBelow : Set a where
     ⊥ : AboveBelow
@@ -104,7 +106,8 @@ module Plain where
     ...   | yes x≈₁y = ⊥-elim (x̷≈₁y x≈₁y)
     ...   | no x̷≈₁y = refl
 
-    ≈-⊔-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊔ ab₃) ≈ (ab₂ ⊔ ab₄)
+    ≈-⊔-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ →
+               (ab₁ ⊔ ab₃) ≈ (ab₂ ⊔ ab₄)
     ≈-⊔-cong ≈-⊤-⊤ ≈-⊤-⊤ = ≈-⊤-⊤
     ≈-⊔-cong ≈-⊤-⊤ ≈-⊥-⊥ = ≈-⊤-⊤
     ≈-⊔-cong ≈-⊥-⊥ ≈-⊤-⊤ = ≈-⊤-⊤
@@ -120,7 +123,8 @@ module Plain where
     ...   | no  a₁̷≈a₃     | yes a₂≈a₄ = ⊥-elim (a₁̷≈a₃ (≈₁-trans a₁≈a₂ (≈₁-trans a₂≈a₄ (≈₁-sym a₃≈a₄))))
     ...   | no  _         | no  _     = ≈-⊤-⊤
 
-    ⊔-assoc : ∀ (ab₁ ab₂ ab₃ : AboveBelow) → ((ab₁ ⊔ ab₂) ⊔ ab₃) ≈ (ab₁ ⊔ (ab₂ ⊔ ab₃))
+    ⊔-assoc : ∀ (ab₁ ab₂ ab₃ : AboveBelow) →
+              ((ab₁ ⊔ ab₂) ⊔ ab₃) ≈ (ab₁ ⊔ (ab₂ ⊔ ab₃))
     ⊔-assoc ⊤ ab₂ ab₃ = ≈-⊤-⊤
     ⊔-assoc ⊥ ab₂ ab₃ = ≈-refl
     ⊔-assoc [ x₁ ] ⊤ ab₃ = ≈-⊤-⊤