From 1c3714123424cd30164f70ecf618b7ab7db36650 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Mon, 16 Feb 2026 17:41:26 -0800
Subject: [PATCH] Add more properties about lattices

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice.agda | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/Lattice.agda b/Lattice.agda
index 6f03d7f..d63aed5 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -96,6 +96,12 @@ record IsSemilattice {a} (A : Set a)
                     (a₁ ⊔ a) ⊔ (a₂ ⊔ a)
                 ∎
 
+    -- need to show: a₁ ⊔ (a₁ ⊔ a₂) ≈ a₁ ⊔ a₂
+    -- (a₁ ⊔ a₁) ⊔ a₂ ≈ a₁ ⊔ (a₁ ⊔ a₂)
+
+    x≼x⊔y : ∀ (a₁ a₂ : A) → a₁ ≼ (a₁ ⊔ a₂)
+    x≼x⊔y a₁ a₂ = ≈-sym (≈-trans (≈-⊔-cong (≈-sym (⊔-idemp a₁)) (≈-refl {a₂})) (⊔-assoc a₁ a₁ a₂))
+
     ≼-refl : ∀ (a : A) → a ≼ a
     ≼-refl a = ⊔-idemp a
 
@@ -113,6 +119,18 @@ record IsSemilattice {a} (A : Set a)
             a₃
         ∎
 
+    ≼-antisym : ∀ {a₁ a₂ : A} → a₁ ≼ a₂ → a₂ ≼ a₁ → a₁ ≈ a₂
+    ≼-antisym {a₁} {a₂} a₁⊔a₂≈a₂ a₂⊔a₁≈a₁ =
+        begin
+            a₁
+        ∼⟨ ≈-sym a₂⊔a₁≈a₁ ⟩
+            a₂ ⊔ a₁
+        ∼⟨ ⊔-comm _ _ ⟩
+            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₄ a₁⊔a₃≈a₃ =
         begin