DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Format AboveBelow a bit better (round two)

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-02 14:56:04 -08:00
parent ec2b1ec3ba
commit 03cdc65a7b
1 changed files with 8 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Lattice/AboveBelow.agda
View File

@ -11,11 +11,13 @@ open import Data.Empty using (⊥-elim)
open import Data.Product using (_,_) open import Data.Product using (_,_)
open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc) open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc)
open import Function using (_∘_) open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl) open import Relation.Binary.PropositionalEquality as Eq
using (_≡_; sym; subst; refl)
import Chain import Chain
open IsEquivalence ≈₁-equiv using () renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans) open IsEquivalence ≈₁-equiv using ()
renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
data AboveBelow : Set a where data AboveBelow : Set a where
⊥ : AboveBelow ⊥ : AboveBelow
@ -104,7 +106,8 @@ module Plain where
... | yes x≈₁y = ⊥-elim (x̷≈₁y x≈₁y) ... | yes x≈₁y = ⊥-elim (x̷≈₁y x≈₁y)
... | no x̷≈₁y = refl ... | no x̷≈₁y = refl
≈-⊔-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊔ ab₃) ≈ (ab₂ ⊔ ab₄) ≈-⊔-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ →
(ab₁ ⊔ ab₃) ≈ (ab₂ ⊔ ab₄)
≈-⊔-cong ≈-⊤-⊤ ≈-⊤-⊤ = ≈-⊤-⊤ ≈-⊔-cong ≈-⊤-⊤ ≈-⊤-⊤ = ≈-⊤-⊤
≈-⊔-cong ≈-⊤-⊤ ≈-⊥-⊥ = ≈-⊤-⊤ ≈-⊔-cong ≈-⊤-⊤ ≈-⊥-⊥ = ≈-⊤-⊤
≈-⊔-cong ≈-⊥-⊥ ≈-⊤-⊤ = ≈-⊤-⊤ ≈-⊔-cong ≈-⊥-⊥ ≈-⊤-⊤ = ≈-⊤-⊤
@ -120,7 +123,8 @@ module Plain where
... | no a₁̷≈a₃ | yes a₂≈a₄ = ⊥-elim (a₁̷≈a₃ (≈₁-trans a₁≈a₂ (≈₁-trans a₂≈a₄ (≈₁-sym a₃≈a₄)))) ... | no a₁̷≈a₃ | yes a₂≈a₄ = ⊥-elim (a₁̷≈a₃ (≈₁-trans a₁≈a₂ (≈₁-trans a₂≈a₄ (≈₁-sym a₃≈a₄))))
... | no _ | no _ = ≈-⊤-⊤ ... | no _ | no _ = ≈-⊤-⊤
⊔-assoc : ∀ (ab₁ ab₂ ab₃ : AboveBelow) → ((ab₁ ⊔ ab₂) ⊔ ab₃) ≈ (ab₁ ⊔ (ab₂ ⊔ ab₃)) ⊔-assoc : ∀ (ab₁ ab₂ ab₃ : AboveBelow) →
((ab₁ ⊔ ab₂) ⊔ ab₃) ≈ (ab₁ ⊔ (ab₂ ⊔ ab₃))
⊔-assoc ⊤ ab₂ ab₃ = ≈-⊤-⊤ ⊔-assoc ⊤ ab₂ ab₃ = ≈-⊤-⊤
⊔-assoc ⊥ ab₂ ab₃ = ≈-refl ⊔-assoc ⊥ ab₂ ab₃ = ≈-refl
⊔-assoc [ x₁ ] ⊤ ab₃ = ≈-⊤-⊤ ⊔-assoc [ x₁ ] ⊤ ab₃ = ≈-⊤-⊤