Fix definition of 'less than' to not involve a third variable.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Fixedpoint.agda

@@ -30,14 +30,14 @@ private
     ⊥ᴬ≼ a with ≈-dec a ⊥ᴬ
     ...   | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
     ...   | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ)
-    ...         | yes ⊥ᴬ≈a⊓⊥ᴬ = (a , ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ)))
+    ...         | yes ⊥ᴬ≈a⊓⊥ᴬ = ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))
     ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight))))
                     where
                         ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
                         ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
 
                         x≺⊥ᴬ : (⊥ᴬ ⊓ a) ≺ ⊥ᴬ
-                        x≺⊥ᴬ = ((⊥ᴬ , ≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a))) , ⊥ᴬ⊓a̷≈⊥ᴬ)
+                        x≺⊥ᴬ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a)) , ⊥ᴬ⊓a̷≈⊥ᴬ)
 
     -- using 'g', for gas, here helps make sure the function terminates.
     -- since A forms a fixed-height lattice, we must find a solution after

Lattice.agda

@@ -19,7 +19,7 @@ record IsSemilattice {a} (A : Set a)
     (_⊔_ : A → A → A) : Set a where
 
     _≼_ : A → A → Set a
-    a ≼ b = Σ A (λ c → (a ⊔ c) ≈ b)
+    a ≼ b = (a ⊔ b) ≈ b
 
     _≺_ : A → A → Set a
     a ≺ b = (a ≼ b) × (¬ a ≈ b)
@@ -34,11 +34,22 @@ record IsSemilattice {a} (A : Set a)
 
     open IsEquivalence ≈-equiv public
 
+    open import Relation.Binary.Reasoning.Base.Single _≈_ ≈-refl ≈-trans
+
     ≼-refl : ∀ (a : A) → a ≼ a
-    ≼-refl a = (a , ⊔-idemp a)
+    ≼-refl a = ⊔-idemp a
 
     ≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄
-    ≼-cong a₁≈a₂ a₃≈a₄ (c₁ , a₁⊔c₁≈a₃) = (c₁ , ≈-trans (≈-⊔-cong (≈-sym a₁≈a₂) ≈-refl) (≈-trans a₁⊔c₁≈a₃ a₃≈a₄))
+    ≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁⊔a₃≈a₃ =
+        begin
+            a₂ ⊔ a₄
+        ∼⟨ ≈-⊔-cong (≈-sym a₁≈a₂) (≈-sym a₃≈a₄) ⟩
+            a₁ ⊔ a₃
+        ∼⟨ a₁⊔a₃≈a₃ ⟩
+            a₃
+        ∼⟨ a₃≈a₄ ⟩
+            a₄
+        ∎
 
     ≺-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≺ a₃ → a₂ ≺ a₄
     ≺-cong a₁≈a₂ a₃≈a₄ (a₁≼a₃ , a₁̷≈a₃) =

Lattice/AboveBelow.agda

@@ -282,29 +282,26 @@ module Plain where
     open IsLattice isLattice using (_≼_; _≺_)
 
     ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ]
-    ⊥≺[x] x = (([ x ] , ≈-refl) , λ ())
+    ⊥≺[x] x = (≈-refl , λ ())
 
-    x≺[y]⇒y≡⊥ : ∀ (x : AboveBelow) (y : A) → x ≺ [ y ] → x ≡ ⊥
-    x≺[y]⇒y≡⊥  x y ((d , x⊔d≈[y]) , x̷≈[y]) with d
-    ... | ⊥ rewrite x⊔⊥≡x x with ≈-lift a≈y ← x⊔d≈[y] = ⊥-elim (x̷≈[y] (≈-lift a≈y))
-    ... | ⊤ rewrite x⊔⊤≡⊤ x with () <- x⊔d≈[y]
-    ... | [ a ] with x
-    ...     | ⊥ = refl
-    ...     | ⊤ with () <- x⊔d≈[y]
-    ...     | [ b ] with ≈₁-dec b a
-    ...         | yes _ with ≈-lift b≈y ← x⊔d≈[y] = ⊥-elim (x̷≈[y] (≈-lift b≈y))
-    ...         | no _ with () <- x⊔d≈[y]
+    x≺[y]⇒x≡⊥ : ∀ (x : AboveBelow) (y : A) → x ≺ [ y ] → x ≡ ⊥
+    x≺[y]⇒x≡⊥  x y ((x⊔[y]≈[y]) , x̷≈[y]) with x
+    ... | ⊥ = refl
+    ... | ⊤ with () ← x⊔[y]≈[y]
+    ... | [ b ] with ≈₁-dec b y
+    ...     | yes b≈y = ⊥-elim (x̷≈[y] (≈-lift b≈y))
+    ...     | no _ with () ← x⊔[y]≈[y]
 
     [x]≺⊤ : ∀ (x : A) → [ x ] ≺ ⊤
-    [x]≺⊤ x rewrite x⊔⊤≡⊤ [ x ] = ((⊤ , ≈-⊤-⊤) , λ ())
+    [x]≺⊤ x rewrite x⊔⊤≡⊤ [ x ] = (≈-⊤-⊤ , λ ())
 
     [x]≺y⇒y≡⊤ : ∀ (x : A) (y : AboveBelow) → [ x ] ≺ y → y ≡ ⊤
-    [x]≺y⇒y≡⊤ x y ((d , [x]⊔d≈y) , [x]̷≈y) with d
-    ... | ⊥ rewrite x⊔⊥≡x [ x ] with ≈-lift x≈a ← [x]⊔d≈y = ⊥-elim ([x]̷≈y (≈-lift x≈a))
-    ... | ⊤ rewrite x⊔⊤≡⊤ [ x ] with ≈-⊤-⊤ ← [x]⊔d≈y = refl
+    [x]≺y⇒y≡⊤ x y ([x]⊔y≈y , [x]̷≈y) with y
+    ... | ⊥ with () ← [x]⊔y≈y
+    ... | ⊤ = refl
     ... | [ a ] with ≈₁-dec x a
-    ...     | yes _   with ≈-lift x≈a ← [x]⊔d≈y = ⊥-elim ([x]̷≈y (≈-lift x≈a))
-    ...     | no _    with ≈-⊤-⊤ ← [x]⊔d≈y = refl
+    ...     | yes x≈a = ⊥-elim ([x]̷≈y (≈-lift x≈a))
+    ...     | no _  with () ← [x]⊔y≈y
 
     open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
 
@@ -313,7 +310,7 @@ module Plain where
         longestChain = step (⊥≺[x] x) ≈-refl (step ([x]≺⊤ x) ≈-⊤-⊤ (done ≈-⊤-⊤))
 
         ¬-Chain-⊤ : ∀ {ab : AboveBelow} {n : ℕ} → ¬ Chain ⊤ ab (suc n)
-        ¬-Chain-⊤ (step ((d , ⊤⊔d≈x) , ⊤̷≈x) _ _) rewrite ⊤⊔x≡⊤ d = ⊥-elim (⊤̷≈x ⊤⊔d≈x)
+        ¬-Chain-⊤ {x} (step (⊤⊔x≈x , ⊤̷≈x) _ _) rewrite ⊤⊔x≡⊤ x = ⊥-elim (⊤̷≈x ⊤⊔x≈x)
 
         isLongest : ∀ {ab₁ ab₂ : AboveBelow} {n : ℕ} → Chain ab₁ ab₂ n → n ≤ 2
         isLongest (done _) = z≤n

Lattice/Prod.agda

@@ -114,13 +114,13 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
 
     private
         a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b))
-        a,∙-Monotonic a {b₁} {b₂} (b , b₁⊔b≈b₂) = ((a , b) , (⊔₁-idemp a , b₁⊔b≈b₂))
+        a,∙-Monotonic a {b₁} {b₂} b₁⊔b₂≈b₂ = (⊔₁-idemp a , b₁⊔b₂≈b₂)
 
         a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶  _≈_
         a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂)
 
         ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b))
-        ∙,b-Monotonic b {a₁} {a₂} (a , a₁⊔a≈a₂) = ((a , b) , (a₁⊔a≈a₂ , ⊔₂-idemp b))
+        ∙,b-Monotonic b {a₁} {a₂} a₁⊔a₂≈a₂ = (a₁⊔a₂≈a₂ , ⊔₂-idemp b)
 
         ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶  _≈_
         ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
@@ -139,17 +139,17 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
 
         unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂)))
         unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
-        unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} (((d₁ , d₂) , (a₁⊔d₁≈a , b₁⊔d₂≈b)) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂)
+        unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼b) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂)
             with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂
         ...   | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b))
         ...   | no a₁̷≈a  | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
-                ((suc n₁ , n₂) , ((step₁ ((d₁ , a₁⊔d₁≈a) , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂)))
+                ((suc n₁ , n₂) , ((step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂)))
         ...   | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
-                ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ ((d₂ , b₁⊔d₂≈b) , b₁̷≈b) b≈b' c₂)
+                ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
                                  , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)
                                  ))
         ...   | no a₁̷≈a  | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
-                ((suc n₁ , suc n₂) , ( (step₁ ((d₁ , a₁⊔d₁≈a) , a₁̷≈a) a≈a' c₁ , step₂ ((d₂ , b₁⊔d₂≈b) , b₁̷≈b) b≈b' c₂)
+                ((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
                                      , ≤-stepsˡ 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
                                      ))
 

Lattice/Unit.agda

@@ -96,7 +96,7 @@ private
     longestChain = done refl
 
     isLongest : ∀ {t₁ t₂ : ⊤} {n : ℕ} → Chain t₁ t₂ n → n ≤ 0
-    isLongest {tt} {tt} (step ((tt , tt⊔tt≈tt) , tt≈tt) _ _) = ⊥-elim (tt≈tt refl)
+    isLongest {tt} {tt} (step (tt⊔tt≈tt , tt̷≈tt) _ _) = ⊥-elim (tt̷≈tt refl)
     isLongest (done _) = z≤n
 
 isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_