From 7c50e7e053e80bc49f8407fefc8754b20bbcd0ed Mon Sep 17 00:00:00 2001 From: Your Name Date: Sat, 12 Oct 2024 02:40:31 +0300 Subject: [PATCH] whatever --- src/Order/Diagram/Glb/Reasoning.agda | 40 ++++++--------------------- src/Order/Diagram/Join/Reasoning.agda | 2 +- src/Order/Diagram/Lub/Reasoning.agda | 40 ++++++--------------------- src/Order/Diagram/Meet/Reasoning.agda | 2 +- src/Order/Trichotomous.agda | 8 +++--- 5 files changed, 24 insertions(+), 68 deletions(-) diff --git a/src/Order/Diagram/Glb/Reasoning.agda b/src/Order/Diagram/Glb/Reasoning.agda index bde3c6f32..cca9ea82f 100644 --- a/src/Order/Diagram/Glb/Reasoning.agda +++ b/src/Order/Diagram/Glb/Reasoning.agda @@ -27,15 +27,16 @@ open glbs renaming ; greatest to ⋂-universal ) public -Top-Poset-Lub : Top P -Top-Poset-Lub .Top.top = ⋂ {I = ⊥} λ() -Top-Poset-Lub .Top.has-top _ = ⋂-universal _ λ () +instance + Top-Poset-Lub : Top P + Top-Poset-Lub .Top.top = ⋂ {I = ⊥} λ() + Top-Poset-Lub .Top.has-top _ = ⋂-universal _ λ () -Meet-Poset-Glb : Has-meets P -Meet-Poset-Glb {x} {y} .Meet.glb = ⋂ {I = Lift ℓ′ Bool} (rec! (if_then x else y)) -Meet-Poset-Glb .Meet.has-meet .is-meet.meet≤l = ⋂-proj (lift true) -Meet-Poset-Glb .Meet.has-meet .is-meet.meet≤r = ⋂-proj (lift false) -Meet-Poset-Glb .Meet.has-meet .is-meet.greatest ub′ p q = ⋂-universal _ (elim! (Bool.elim p q)) + Meet-Poset-Glb : Has-meets P + Meet-Poset-Glb {x} {y} .Meet.glb = ⋂ {I = Lift ℓ′ Bool} (rec! (if_then x else y)) + Meet-Poset-Glb .Meet.has-meet .is-meet.meet≤l = ⋂-proj (lift true) + Meet-Poset-Glb .Meet.has-meet .is-meet.meet≤r = ⋂-proj (lift false) + Meet-Poset-Glb .Meet.has-meet .is-meet.greatest ub′ p q = ⋂-universal _ (elim! (Bool.elim p q)) open Top Top-Poset-Lub public open import Order.Diagram.Meet.Reasoning P Meet-Poset-Glb public @@ -99,26 +100,3 @@ module @0 _ {I : Type ℓ′} where opaque ≤-antisym ∩-distrib-⋂-≤l (rec! (λ i → ∩-universal _ (⋂-proj i ∙ ∩≤l) (⋂≤⋂ λ _ → ∩≤r)) i) - -opaque - ∩-id-l : {x : Ob} → ⊤ ∩ x ＝ x - ∩-id-l {x} = ≤-antisym - ∩≤r - (∩-universal _ ! refl) - - ∩-id-r : {x : Ob} → x ∩ ⊤ ＝ x - ∩-id-r {x} = ≤-antisym - ∩≤l - (∩-universal _ refl !) - - ∩-is-comm-monoid : is-comm-monoid {A = Ob} _∩_ - ∩-is-comm-monoid = to-is-comm-monoid go where - open make-comm-monoid - go : make-comm-monoid Ob - go .monoid-is-set = ob-is-set - go .id = ⊤ - go ._⋆_ = _∩_ - go .id-l _ = ∩-id-l - go .id-r _ = ∩-id-r - go .assoc _ _ _ = ∩-assoc - go .comm _ _ = ∩-comm diff --git a/src/Order/Diagram/Join/Reasoning.agda b/src/Order/Diagram/Join/Reasoning.agda index 3c4f55413..a8c60206c 100644 --- a/src/Order/Diagram/Join/Reasoning.agda +++ b/src/Order/Diagram/Join/Reasoning.agda @@ -82,7 +82,7 @@ opaque ∪≃order = prop-extₑ! ∪→order order→∪ ∪≃≤× : x ∪ y ≤ z ≃ (x ≤ z) × (y ≤ z) - ∪≃≤× = prop-extₑ! (λ ∩≤z → l≤∪ ∙ ∩≤z , r≤∪ ∙ ∩≤z) λ where (x≤z , y≤z) → ∪-universal _ x≤z y≤z + ∪≃≤× = prop-extₑ! < l≤∪ ∙_ , r≤∪ ∙_ > (∪-universal _ $ₜ²_) ≤⊎→∪ : (z ≤ x) ⊎ (z ≤ y) → z ≤ x ∪ y ≤⊎→∪ = [ _∙ l≤∪ , _∙ r≤∪ ]ᵤ diff --git a/src/Order/Diagram/Lub/Reasoning.agda b/src/Order/Diagram/Lub/Reasoning.agda index 40ad2cc11..34e7ebc78 100644 --- a/src/Order/Diagram/Lub/Reasoning.agda +++ b/src/Order/Diagram/Lub/Reasoning.agda @@ -27,15 +27,16 @@ open lubs renaming ; least to ⋃-universal ) public -Bottom-Poset-Lub : Bottom P -Bottom-Poset-Lub .Bottom.bot = ⋃ {I = Lift ℓ′ ⊥} λ() -Bottom-Poset-Lub .Bottom.has-bot _ = ⋃-universal _ λ () +instance + Bottom-Poset-Lub : Bottom P + Bottom-Poset-Lub .Bottom.bot = ⋃ {I = Lift ℓ′ ⊥} λ() + Bottom-Poset-Lub .Bottom.has-bot _ = ⋃-universal _ λ () -Join-Poset-Lub : Has-joins P -Join-Poset-Lub {x} {y} .Join.lub = ⋃ {I = Lift ℓ′ Bool} (rec! (if_then x else y)) -Join-Poset-Lub .Join.has-join .is-join.l≤join = ⋃-inj (lift true) -Join-Poset-Lub .Join.has-join .is-join.r≤join = ⋃-inj (lift false) -Join-Poset-Lub .Join.has-join .is-join.least ub′ p q = ⋃-universal _ (elim! (Bool.elim p q)) + Join-Poset-Lub : Has-joins P + Join-Poset-Lub {x} {y} .Join.lub = ⋃ {I = Lift ℓ′ Bool} (rec! (if_then x else y)) + Join-Poset-Lub .Join.has-join .is-join.l≤join = ⋃-inj (lift true) + Join-Poset-Lub .Join.has-join .is-join.r≤join = ⋃-inj (lift false) + Join-Poset-Lub .Join.has-join .is-join.least ub′ p q = ⋃-universal _ (elim! (Bool.elim p q)) open Bottom Bottom-Poset-Lub public open import Order.Diagram.Join.Reasoning P Join-Poset-Lub public @@ -99,26 +100,3 @@ module @0 _ {I : Type ℓ′} where opaque ≤-antisym ∪-distrib-⋃-≤-l (rec! (λ i → ∪-universal _ (l≤∪ ∙ ⋃-inj i) (⋃≤⋃ λ _ → r≤∪)) i) - -opaque - ∪-id-l : {x : Ob} → ⊥ ∪ x ＝ x - ∪-id-l {x} = ≤-antisym - (∪-universal _ ¡ refl) - r≤∪ - - ∪-id-r : {x : Ob} → x ∪ ⊥ ＝ x - ∪-id-r {x} = ≤-antisym - (∪-universal _ refl ¡) - l≤∪ - - ∪-is-comm-monoid : is-comm-monoid {A = Ob} _∪_ - ∪-is-comm-monoid = to-is-comm-monoid go where - open make-comm-monoid - go : make-comm-monoid Ob - go .monoid-is-set = ob-is-set - go .id = ⊥ - go ._⋆_ = _∪_ - go .id-l _ = ∪-id-l - go .id-r _ = ∪-id-r - go .assoc _ _ _ = ∪-assoc - go .comm _ _ = ∪-comm diff --git a/src/Order/Diagram/Meet/Reasoning.agda b/src/Order/Diagram/Meet/Reasoning.agda index a9cb33e12..a969d3ff4 100644 --- a/src/Order/Diagram/Meet/Reasoning.agda +++ b/src/Order/Diagram/Meet/Reasoning.agda @@ -82,7 +82,7 @@ opaque ∩≃order = prop-extₑ! ∩→order order→∩ ∩≃≤× : z ≤ x ∩ y ≃ (z ≤ x) × (z ≤ y) - ∩≃≤× = prop-extₑ! (λ z≤∩ → z≤∩ ∙ ∩≤l , z≤∩ ∙ ∩≤r) λ where (z≤x , z≤y) → ∩-universal _ z≤x z≤y + ∩≃≤× = prop-extₑ! < _∙ ∩≤l , _∙ ∩≤r > (∩-universal _ $ₜ²_) ≤⊎→∩ : (x ≤ z) ⊎ (y ≤ z) → x ∩ y ≤ z ≤⊎→∩ = [ ∩≤l ∙_ , ∩≤r ∙_ ]ᵤ diff --git a/src/Order/Trichotomous.agda b/src/Order/Trichotomous.agda index a71dbfbe4..779240923 100644 --- a/src/Order/Trichotomous.agda +++ b/src/Order/Trichotomous.agda @@ -41,13 +41,13 @@ module _ {o ℓ} {S : StrictPoset o ℓ} where : is-decidable-strict-total-order S → is-trichotomous S dec-strict-total-order→tri-order d .is-trichotomous.trisect x y - with d .is-decidable-strict-total-order.has-discrete {x} {y} - ... | yes x=y = EQ x=y - ... | no x≠y with d .is-decidable-strict-total-order.dec-< {x} {y} + with d .is-decidable-strict-total-order.dec-< {x} {y} ... | yes x