From 03cdc65a7b288096f9ce88c2a47f7f7455534f35 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 2 Mar 2024 14:56:04 -0800 Subject: [PATCH] Format AboveBelow a bit better (round two) Signed-off-by: Danila Fedorin --- Lattice/AboveBelow.agda | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda index d8e3587..b1ad4ca 100644 --- a/Lattice/AboveBelow.agda +++ b/Lattice/AboveBelow.agda @@ -11,11 +11,13 @@ 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) +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) +open IsEquivalence ≈₁-equiv using () + renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans) data AboveBelow : Set a where ⊥ : AboveBelow @@ -104,7 +106,8 @@ module Plain where ... | 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 : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → + (ab₁ ⊔ ab₃) ≈ (ab₂ ⊔ ab₄) ≈-⊔-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 _ | 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₃ = ≈-refl ⊔-assoc [ x₁ ] ⊤ ab₃ = ≈-⊤-⊤