From 112dcb220854c60b9788e938b2aee6be62b17639 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 2 Mar 2024 14:34:15 -0800 Subject: [PATCH] Clean up AboveBelow slightly Signed-off-by: Danila Fedorin --- Lattice/AboveBelow.agda | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda index 6056e30..d8e3587 100644 --- a/Lattice/AboveBelow.agda +++ b/Lattice/AboveBelow.agda @@ -10,7 +10,9 @@ module Lattice.AboveBelow {a} (A : Set a) open import Data.Empty using (⊥-elim) open import Data.Product using (_,_) open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc) +open import Function using (_∘_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl) + import Chain open IsEquivalence ≈₁-equiv using () renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans) @@ -61,6 +63,9 @@ data _≈_ : AboveBelow → AboveBelow → Set a where ≈-dec [ x ] ⊥ = no λ () ≈-dec [ x ] ⊤ = no λ () +-- Any object can be wrapped in an 'above below' to make it a lattice, +-- since ⊤ and ⊥ are the largest and least elements, and the rest are left +-- unordered. That's what this module does. module Plain where _⊔_ : AboveBelow → AboveBelow → AboveBelow ⊥ ⊔ x = x @@ -126,7 +131,7 @@ module Plain where 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₃) = ≈-⊤-⊤ + rewrite x̷≈y⇒[x]⊔[y]≡⊤ (x₂̷≈x₃ ∘ (≈₁-trans (≈₁-sym 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 @@ -139,7 +144,7 @@ module Plain where ⊔-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₁)) = ≈-⊤-⊤ + ... | no x₁̷≈x₂ rewrite x̷≈y⇒[x]⊔[y]≡⊤ (x₁̷≈x₂ ∘ ≈₁-sym) = ≈-⊤-⊤ ⊔-idemp : ∀ ab → (ab ⊔ ab) ≈ ab ⊔-idemp ⊤ = ≈-⊤-⊤