whatever

cmcmA20 · Oct 11, 2024 · 7c50e7e · 7c50e7e
1 parent bb372a4
commit 7c50e7e
Show file tree

Hide file tree

Showing 5 changed files with 24 additions and 68 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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<y = LT x<y
   ... | no  x≮y with d .is-decidable-strict-total-order.dec-< {y} {x}
   ... | yes y<x = GT y<x
-  ... | no  y≮x = ⊥.rec (x≠y (d .is-decidable-strict-total-order.connex x y x≮y y≮x))
+  ... | no  y≮x = EQ
+    (d .is-decidable-strict-total-order.has-is-strict-total .is-strict-total-order.connex
+      x y x≮y y≮x)
 
   module _ (t : is-trichotomous S) where
     open is-trichotomous t hiding (Ob; _<_)