From d338241319c7ec22e5a2613ebaba41de0156cb7f Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 17 Sep 2023 20:01:32 -0700
Subject: [PATCH] Add a meet operation, too

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

diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda
index db178d0..0b7af33 100644
--- a/Lattice/AboveBelow.agda
+++ b/Lattice/AboveBelow.agda
@@ -151,3 +151,96 @@ module Plain where
         ; ⊔-comm = ⊔-comm
         ; ⊔-idemp = ⊔-idemp
         }
+
+    _⊓_ : AboveBelow → AboveBelow → AboveBelow
+    ⊥ ⊓ x = ⊥
+    ⊤ ⊓ x = x
+    [ x ] ⊓ [ y ] with ≈₁-dec x y
+    ...   | yes _ = [ x ]
+    ...   | no  _ = ⊥
+    x ⊓ ⊥ = ⊥
+    x ⊓ ⊤ = x
+
+    ⊥⊓x≡⊥ : ∀ (x : AboveBelow) → ⊥ ⊓ x ≡ ⊥
+    ⊥⊓x≡⊥ _ = refl
+
+    x⊓⊥≡⊥ : ∀ (x : AboveBelow) → x ⊓ ⊥ ≡ ⊥
+    x⊓⊥≡⊥ ⊤ = refl
+    x⊓⊥≡⊥ ⊥ = refl
+    x⊓⊥≡⊥ [ x ] = refl
+
+    ⊤⊓x≡x : ∀ (x : AboveBelow) → ⊤ ⊓ x ≡ x
+    ⊤⊓x≡x _ = refl
+
+    x⊓⊤≡x : ∀ (x : AboveBelow) → x ⊓ ⊤ ≡ x
+    x⊓⊤≡x ⊤ = refl
+    x⊓⊤≡x ⊥ = refl
+    x⊓⊤≡x [ x ] = refl
+
+    x≈y⇒[x]⊓[y]≡[x] : ∀ {x y : A} → x ≈₁ y → [ x ] ⊓ [ y ] ≡ [ x ]
+    x≈y⇒[x]⊓[y]≡[x] {x} {y} x≈₁y
+        with ≈₁-dec x y
+    ...   | yes _ = refl
+    ...   | no x̷≈₁y = ⊥-elim (x̷≈₁y x≈₁y)
+
+    x̷≈y⇒[x]⊓[y]≡⊥ : ∀ {x y : A} → ¬ x ≈₁ y → [ x ] ⊓ [ y ] ≡ ⊥
+    x̷≈y⇒[x]⊓[y]≡⊥ {x} {y} x̷≈₁y
+        with ≈₁-dec x y
+    ...   | yes x≈₁y = ⊥-elim (x̷≈₁y x≈₁y)
+    ...   | no x̷≈₁y = refl
+
+    ≈-⊓-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊓ ab₃) ≈ (ab₂ ⊓ ab₄)
+    ≈-⊓-cong ≈-⊤-⊤ ≈-⊤-⊤ = ≈-⊤-⊤
+    ≈-⊓-cong ≈-⊤-⊤ ≈-⊥-⊥ = ≈-⊥-⊥
+    ≈-⊓-cong ≈-⊥-⊥ ≈-⊤-⊤ = ≈-⊥-⊥
+    ≈-⊓-cong ≈-⊥-⊥ ≈-⊥-⊥ = ≈-⊥-⊥
+    ≈-⊓-cong ≈-⊤-⊤ (≈-lift x≈y) = ≈-lift x≈y
+    ≈-⊓-cong (≈-lift x≈y) ≈-⊤-⊤ = ≈-lift x≈y
+    ≈-⊓-cong ≈-⊥-⊥ (≈-lift x≈y) = ≈-⊥-⊥
+    ≈-⊓-cong (≈-lift x≈y) ≈-⊥-⊥ = ≈-⊥-⊥
+    ≈-⊓-cong (≈-lift {a₁} {a₂} a₁≈a₂) (≈-lift {a₃} {a₄} a₃≈a₄)
+        with ≈₁-dec a₁ a₃ | ≈₁-dec a₂ a₄
+    ...   | yes a₁≈a₃     | yes a₂≈a₄ = ≈-lift a₁≈a₂
+    ...   | yes a₁≈a₃     | no  a₂̷≈a₄ = ⊥-elim (a₂̷≈a₄ (≈₁-trans (≈₁-sym a₁≈a₂) (≈₁-trans (a₁≈a₃) a₃≈a₄)))
+    ...   | no  a₁̷≈a₃     | yes a₂≈a₄ = ⊥-elim (a₁̷≈a₃ (≈₁-trans a₁≈a₂ (≈₁-trans a₂≈a₄ (≈₁-sym a₃≈a₄))))
+    ...   | no  _         | no  _     = ≈-⊥-⊥
+
+    ⊓-assoc : ∀ (ab₁ ab₂ ab₃ : AboveBelow) → ((ab₁ ⊓ ab₂) ⊓ ab₃) ≈ (ab₁ ⊓ (ab₂ ⊓ ab₃))
+    ⊓-assoc ⊥ ab₂ ab₃ = ≈-⊥-⊥
+    ⊓-assoc ⊤ ab₂ ab₃ = ≈-refl
+    ⊓-assoc [ x₁ ] ⊥ ab₃ = ≈-⊥-⊥
+    ⊓-assoc [ x₁ ] ⊤ ab₃ = ≈-refl
+    ⊓-assoc [ x₁ ] [ x₂ ] ⊥ rewrite x⊓⊥≡⊥ ([ x₁ ] ⊓ [ x₂ ]) = ≈-⊥-⊥
+    ⊓-assoc [ x₁ ] [ x₂ ] ⊤ rewrite x⊓⊤≡x ([ x₁ ] ⊓ [ x₂ ]) = ≈-refl
+    ⊓-assoc [ x₁ ] [ x₂ ] [ x₃ ]
+        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₃) = ≈-⊥-⊥
+    ...   | 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
+    ...   | yes x₂≈x₃ | no  x₁̷≈x₂ rewrite x̷≈y⇒[x]⊓[y]≡⊥ x₁̷≈x₂ = ≈-⊥-⊥
+
+    ⊓-comm : ∀ (ab₁ ab₂ : AboveBelow) → (ab₁ ⊓ ab₂) ≈ (ab₂ ⊓ ab₁)
+    ⊓-comm ⊥ x rewrite x⊓⊥≡⊥ x = ≈-refl
+    ⊓-comm ⊤ x rewrite x⊓⊤≡x x = ≈-refl
+    ⊓-comm x ⊥ rewrite x⊓⊥≡⊥ x = ≈-refl
+    ⊓-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₁)) = ≈-⊥-⊥
+
+    ⊓-idemp : ∀ ab → (ab ⊓ ab) ≈ ab
+    ⊓-idemp ⊥ = ≈-⊥-⊥
+    ⊓-idemp ⊤ = ≈-⊤-⊤
+    ⊓-idemp [ x ] rewrite x≈y⇒[x]⊓[y]≡[x] (≈₁-refl {x}) = ≈-refl
+
+    isMeetSemilattice : IsSemilattice AboveBelow _≈_ _⊓_
+    isMeetSemilattice = record
+        { ≈-equiv = ≈-equiv
+        ; ≈-⊔-cong = ≈-⊓-cong
+        ; ⊔-assoc = ⊓-assoc
+        ; ⊔-comm = ⊓-comm
+        ; ⊔-idemp = ⊓-idemp
+        }