From c0db2ccd463d4523bb9ecaeb32649d2e372b2af3 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Mon, 18 Sep 2023 20:56:08 -0700
Subject: [PATCH] Add a lattice instance for the AboveBelow type

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

diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda
index 0b7af33..f410cd5 100644
--- a/Lattice/AboveBelow.agda
+++ b/Lattice/AboveBelow.agda
@@ -244,3 +244,34 @@ module Plain where
         ; ⊔-comm = ⊓-comm
         ; ⊔-idemp = ⊓-idemp
         }
+
+    absorb-⊔-⊓ : ∀ (ab₁ ab₂ : AboveBelow) → (ab₁ ⊔ (ab₁ ⊓ ab₂)) ≈ ab₁
+    absorb-⊔-⊓ ⊥ ab₂ rewrite ⊥⊓x≡⊥ ab₂ = ≈-⊥-⊥
+    absorb-⊔-⊓ ⊤ _ = ≈-⊤-⊤
+    absorb-⊔-⊓ [ x ] ⊥ rewrite x⊓⊥≡⊥ [ x ]
+                       rewrite x⊔⊥≡x [ x ] = ≈-refl
+    absorb-⊔-⊓ [ x ] ⊤ rewrite x⊓⊤≡x [ x ] = ⊔-idemp _
+    absorb-⊔-⊓ [ x ] [ y ]
+        with ≈₁-dec x y
+    ...   | yes x≈y rewrite x≈y⇒[x]⊓[y]≡[x] x≈y = ⊔-idemp _
+    ...   | no x̷≈y rewrite x̷≈y⇒[x]⊓[y]≡⊥ x̷≈y rewrite x⊔⊥≡x [ x ] = ≈-refl
+
+    absorb-⊓-⊔ : ∀ (ab₁ ab₂ : AboveBelow) → (ab₁ ⊓ (ab₁ ⊔ ab₂)) ≈ ab₁
+    absorb-⊓-⊔ ⊤ ab₂ rewrite ⊤⊔x≡⊤ ab₂ = ≈-⊤-⊤
+    absorb-⊓-⊔ ⊥ _ = ≈-⊥-⊥
+    absorb-⊓-⊔ [ x ] ⊤ rewrite x⊔⊤≡⊤ [ x ]
+                       rewrite x⊓⊤≡x [ x ] = ≈-refl
+    absorb-⊓-⊔ [ x ] ⊥ rewrite x⊔⊥≡x [ x ] = ⊓-idemp _
+    absorb-⊓-⊔ [ x ] [ y ]
+        with ≈₁-dec x y
+    ...   | yes x≈y rewrite x≈y⇒[x]⊔[y]≡[x] x≈y = ⊓-idemp _
+    ...   | no x̷≈y rewrite x̷≈y⇒[x]⊔[y]≡⊤ x̷≈y rewrite x⊓⊤≡x [ x ] = ≈-refl
+
+
+    isLattice : IsLattice AboveBelow _≈_ _⊔_ _⊓_
+    isLattice = record
+        { joinSemilattice = isJoinSemilattice
+        ; meetSemilattice = isMeetSemilattice
+        ; absorb-⊔-⊓ = absorb-⊔-⊓
+        ; absorb-⊓-⊔ = absorb-⊓-⊔
+        }