diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda
index 6056e30..d8e3587 100644
--- a/Lattice/AboveBelow.agda
+++ b/Lattice/AboveBelow.agda
@@ -10,7 +10,9 @@ module Lattice.AboveBelow {a} (A : Set a)
 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)
+
 import Chain
 
 open IsEquivalence ≈₁-equiv using () renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
@@ -61,6 +63,9 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
 ≈-dec [ x ] ⊥ = no λ ()
 ≈-dec [ x ] ⊤ = no λ ()
 
+-- Any object can be wrapped in an 'above below' to make it a lattice,
+-- since ⊤ and ⊥ are the largest and least elements, and the rest are left
+-- unordered. That's what this module does.
 module Plain where
     _⊔_ : AboveBelow → AboveBelow → AboveBelow
     ⊥ ⊔ x = x
@@ -126,7 +131,7 @@ module Plain where
         with ≈₁-dec x₂ x₃ | ≈₁-dec x₁ x₂
     ...   | no  x₂̷≈x₃ | no _      rewrite x̷≈y⇒[x]⊔[y]≡⊤ x₂̷≈x₃ = ≈-⊤-⊤
     ...   | no  x₂̷≈x₃ | yes x₁≈x₂ rewrite x̷≈y⇒[x]⊔[y]≡⊤ x₂̷≈x₃
-                                  rewrite x̷≈y⇒[x]⊔[y]≡⊤ λ x₁≈x₃ → x₂̷≈x₃ (≈₁-trans (≈₁-sym x₁≈x₂) x₁≈x₃) = ≈-⊤-⊤
+                                  rewrite x̷≈y⇒[x]⊔[y]≡⊤ (x₂̷≈x₃ ∘ (≈₁-trans (≈₁-sym x₁≈x₂))) = ≈-⊤-⊤
     ...   | yes x₂≈x₃ | yes x₁≈x₂ rewrite x≈y⇒[x]⊔[y]≡[x] x₂≈x₃
                                   rewrite x≈y⇒[x]⊔[y]≡[x] x₁≈x₂
                                   rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-trans x₁≈x₂ x₂≈x₃) = ≈-refl
@@ -139,7 +144,7 @@ module Plain where
     ⊔-comm x ⊥ rewrite x⊔⊥≡x x = ≈-refl
     ⊔-comm [ x₁ ] [ x₂ ] with ≈₁-dec x₁ x₂
     ... | yes x₁≈x₂ rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-sym x₁≈x₂) = ≈-lift x₁≈x₂
-    ... | no  x₁̷≈x₂ rewrite x̷≈y⇒[x]⊔[y]≡⊤ λ x₂≈x₁ → (x₁̷≈x₂ (≈₁-sym x₂≈x₁)) = ≈-⊤-⊤
+    ... | no  x₁̷≈x₂ rewrite x̷≈y⇒[x]⊔[y]≡⊤ (x₁̷≈x₂ ∘ ≈₁-sym) = ≈-⊤-⊤
 
     ⊔-idemp : ∀ ab → (ab ⊔ ab) ≈ ab
     ⊔-idemp ⊤ = ≈-⊤-⊤