Add a lattice instance for the AboveBelow type

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

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-⊓-⊔
+        }