From d96eaca1b6d176d1f341e29fc803aa541f6ab9f5 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Mon, 22 Dec 2025 20:43:24 +0100
Subject: [PATCH] Show adding extrema to a non-strict order respects equality

---
 CHANGELOG.md                                  | 30 +++++++++++++++++++
 .../Construct/Add/Extrema/NonStrict.agda      | 20 ++++++++++++-
 .../Construct/Add/Infimum/NonStrict.agda      | 28 +++++++++++++++--
 .../Construct/Add/Supremum/NonStrict.agda     | 27 +++++++++++++++--
 4 files changed, 99 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 38c13e12be..6192982a82 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -251,6 +251,36 @@ Additions to existing modules
                     updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ padRight m≤n x (updateAt xs i f)
   ```
 
+* In Relation.Binary.Construct.Add.Extrema.NonStrict:
+  ```agda
+  ≤±-respˡ-≡ : _≤±_ Respectsˡ _≡_
+  ≤±-respʳ-≡ : _≤±_ Respectsʳ _≡_
+  ≤±-resp-≡ : _≤±_ Respects₂ _≡_
+  ≤±-respˡ-≈± : _≤_ Respectsˡ _≈_ → _≤±_ Respectsˡ _≈±_
+  ≤±-respʳ-≈± : _≤_ Respectsʳ _≈_ → _≤±_ Respectsʳ _≈±_
+  ≤±-resp-≈± : _≤_ Respects₂ _≈_ → _≤±_ Respects₂ _≈±_
+  ```
+
+* In Relation.Binary.Construct.Add.Infimum.NonStrict:
+  ```agda
+  ≤₋-respˡ-≡ : _≤₋_ Respectsˡ _≡_
+  ≤₋-respʳ-≡ : _≤₋_ Respectsʳ _≡_
+  ≤₋-resp-≡ : _≤₋_ Respects₂ _≡_
+  ≤₋-respˡ-≈₋ : _≤_ Respectsˡ _≈_ → _≤₋_ Respectsˡ _≈₋_
+  ≤₋-respʳ-≈₋ : _≤_ Respectsʳ _≈_ → _≤₋_ Respectsʳ _≈₋_
+  ≤₋-resp-≈₋ : _≤_ Respects₂ _≈_ → _≤₋_ Respects₂ _≈₋_
+  ```
+
+* In Relation.Binary.Construct.Add.Extrema.Supremum.NonStrict:
+  ```agda
+  ≤⁺-respˡ-≡ : _≤⁺_ Respectsˡ _≡_
+  ≤⁺-respʳ-≡ : _≤⁺_ Respectsʳ _≡_
+  ≤⁺-resp-≡ : _≤⁺_ Respects₂ _≡_
+  ≤⁺-respˡ-≈⁺ : _≤_ Respectsˡ _≈_ → _≤⁺_ Respectsˡ _≈⁺_
+  ≤⁺-respʳ-≈⁺ : _≤_ Respectsʳ _≈_ → _≤⁺_ Respectsʳ _≈⁺_
+  ≤⁺-resp-≈⁺ : _≤_ Respects₂ _≈_ → _≤⁺_ Respects₂ _≈⁺_
+  ```
+
 * In `Relation.Nullary.Negation.Core`
   ```agda
   ¬¬-η           : A → ¬ ¬ A
diff --git a/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda b/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda
index f1b9880d0b..4e6c01bd52 100644
--- a/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda
@@ -20,7 +20,7 @@ open import Relation.Binary.Structures
         ; IsDecTotalOrder)
 open import Relation.Binary.Definitions
   using (Decidable; Transitive; Minimum; Maximum; Total; Irrelevant
-        ; Antisymmetric)
+        ; Antisymmetric; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
 open import Relation.Nullary.Construct.Add.Extrema using (⊥±; ⊤±; [_])
 import Relation.Nullary.Construct.Add.Infimum as I using (⊥₋; [_])
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
@@ -90,6 +90,15 @@ _≤⊤± : ∀ k → k ≤± ⊤±
 ≤±-antisym-≡ : Antisymmetric _≡_ _≤_ → Antisymmetric _≡_ _≤±_
 ≤±-antisym-≡ = Sup.≤⁺-antisym-≡ ∘′ Inf.≤₋-antisym-≡
 
+≤±-respˡ-≡ : _≤±_ Respectsˡ _≡_
+≤±-respˡ-≡ = Sup.≤⁺-respˡ-≡
+
+≤±-respʳ-≡ : _≤±_ Respectsʳ _≡_
+≤±-respʳ-≡ = Sup.≤⁺-respʳ-≡
+
+≤±-resp-≡ : _≤±_ Respects₂ _≡_
+≤±-resp-≡ = Sup.≤⁺-resp-≡
+
 ------------------------------------------------------------------------
 -- Relational properties + setoid equality
 
@@ -103,6 +112,15 @@ module _ {e} {_≈_ : Rel A e} where
   ≤±-antisym : Antisymmetric _≈_ _≤_ → Antisymmetric _≈±_ _≤±_
   ≤±-antisym = Sup.≤⁺-antisym ∘′ Inf.≤₋-antisym
 
+  ≤±-respˡ-≈± : _≤_ Respectsˡ _≈_ → _≤±_ Respectsˡ _≈±_
+  ≤±-respˡ-≈± = Sup.≤⁺-respˡ-≈⁺ ∘′ Inf.≤₋-respˡ-≈₋
+
+  ≤±-respʳ-≈± : _≤_ Respectsʳ _≈_ → _≤±_ Respectsʳ _≈±_
+  ≤±-respʳ-≈± = Sup.≤⁺-respʳ-≈⁺ ∘′ Inf.≤₋-respʳ-≈₋
+
+  ≤±-resp-≈± : _≤_ Respects₂ _≈_ → _≤±_ Respects₂ _≈±_
+  ≤±-resp-≈± = Sup.≤⁺-resp-≈⁺ ∘′ Inf.≤₋-resp-≈₋
+
 ------------------------------------------------------------------------
 -- Structures + propositional equality
 
diff --git a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
index b6b0ee8d27..1c59d03972 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
@@ -11,13 +11,13 @@
 
 open import Relation.Binary.Core using (Rel; _⇒_)
 
-
 module Relation.Binary.Construct.Add.Infimum.NonStrict
   {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where
 
 open import Level using (_⊔_)
+open import Data.Product.Base as Product using (_,_)
 open import Data.Sum.Base as Sum using (inj₁; inj₂)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; subst)
 import Relation.Binary.PropositionalEquality.Properties as ≡
   using (isEquivalence)
 import Relation.Binary.Construct.Add.Infimum.Equality as Equality
@@ -27,7 +27,8 @@ open import Relation.Binary.Structures
   using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder
         ; IsDecTotalOrder)
 open import Relation.Binary.Definitions
-  using (Minimum; Transitive; Total; Decidable; Irrelevant; Antisymmetric)
+  using (Minimum; Transitive; Total; Decidable; Irrelevant; Antisymmetric
+        ; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
 open import Relation.Nullary.Construct.Add.Infimum using (⊥₋; [_]; _₋; ≡-dec)
 open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 import Relation.Nullary.Decidable.Core as Dec using (map′)
@@ -78,6 +79,15 @@ data _≤₋_ : Rel (A ₋) (a ⊔ ℓ) where
 ≤₋-antisym-≡ antisym (⊥₋≤ _) (⊥₋≤ _) = refl
 ≤₋-antisym-≡ antisym [ p ] [ q ]     = cong [_] (antisym p q)
 
+≤₋-respˡ-≡ : _≤₋_ Respectsˡ _≡_
+≤₋-respˡ-≡ = subst (_≤₋ _)
+
+≤₋-respʳ-≡ : _≤₋_ Respectsʳ _≡_
+≤₋-respʳ-≡ = subst (_ ≤₋_)
+
+≤₋-resp-≡ : _≤₋_ Respects₂ _≡_
+≤₋-resp-≡ = ≤₋-respʳ-≡ , ≤₋-respˡ-≡
+
 ------------------------------------------------------------------------
 -- Relational properties + setoid equality
 
@@ -93,6 +103,18 @@ module _ {e} {_≈_ : Rel A e} where
   ≤₋-antisym ≤≥⇒≈ (⊥₋≤ _) (⊥₋≤ _) = ⊥₋≈⊥₋
   ≤₋-antisym ≤≥⇒≈ [ p ] [ q ] = [ ≤≥⇒≈ p q ]
 
+  ≤₋-respˡ-≈₋ : _≤_ Respectsˡ _≈_ → _≤₋_ Respectsˡ _≈₋_
+  ≤₋-respˡ-≈₋ ≤-respˡ-≈ [ p ] [ q ] = [ ≤-respˡ-≈ p q ]
+  ≤₋-respˡ-≈₋ ≤-respˡ-≈ ⊥₋≈⊥₋ q = q
+
+  ≤₋-respʳ-≈₋ : _≤_ Respectsʳ _≈_ → _≤₋_ Respectsʳ _≈₋_
+  ≤₋-respʳ-≈₋ ≤-respʳ-≈ [ _ ] (⊥₋≤ l) = ⊥₋≤ [ _ ]
+  ≤₋-respʳ-≈₋ ≤-respʳ-≈ [ p ] [ q ] = [ ≤-respʳ-≈ p q ]
+  ≤₋-respʳ-≈₋ ≤-respʳ-≈ ⊥₋≈⊥₋ q = q
+
+  ≤₋-resp-≈₋ : _≤_ Respects₂ _≈_ → _≤₋_ Respects₂ _≈₋_
+  ≤₋-resp-≈₋ = Product.map ≤₋-respʳ-≈₋ ≤₋-respˡ-≈₋
+
 ------------------------------------------------------------------------
 -- Structures + propositional equality
 
diff --git a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
index 58770eafd8..124068aa80 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
@@ -15,14 +15,16 @@ module Relation.Binary.Construct.Add.Supremum.NonStrict
   {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where
 
 open import Level using (_⊔_)
+open import Data.Product.Base as Product using (_,_)
 open import Data.Sum.Base as Sum
 open import Relation.Binary.Structures
   using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder)
 open import Relation.Binary.Definitions
-  using (Maximum; Transitive; Total; Decidable; Irrelevant; Antisymmetric)
+  using (Maximum; Transitive; Total; Decidable; Irrelevant; Antisymmetric
+        ; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
 import Relation.Nullary.Decidable.Core as Dec using (map′)
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; cong)
+  using (_≡_; refl; cong; subst)
 import Relation.Binary.PropositionalEquality.Properties as ≡
 open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Nullary.Decidable.Core using (yes; no)
@@ -76,6 +78,15 @@ data _≤⁺_ : Rel (A ⁺) (a ⊔ ℓ) where
 ≤⁺-antisym-≡ antisym (_ ≤⊤⁺) (_ ≤⊤⁺) = refl
 ≤⁺-antisym-≡ antisym [ p ] [ q ]     = cong [_] (antisym p q)
 
+≤⁺-respˡ-≡ : _≤⁺_ Respectsˡ _≡_
+≤⁺-respˡ-≡ = subst (_≤⁺ _)
+
+≤⁺-respʳ-≡ : _≤⁺_ Respectsʳ _≡_
+≤⁺-respʳ-≡ = subst (_ ≤⁺_)
+
+≤⁺-resp-≡ : _≤⁺_ Respects₂ _≡_
+≤⁺-resp-≡ = ≤⁺-respʳ-≡ , ≤⁺-respˡ-≡
+
 ------------------------------------------------------------------------
 -- Relation properties + setoid equality
 
@@ -91,6 +102,18 @@ module _ {e} {_≈_ : Rel A e} where
   ≤⁺-antisym ≤-antisym [ p ]    [ q ]  = [ ≤-antisym p q ]
   ≤⁺-antisym ≤-antisym (_ ≤⊤⁺) (_ ≤⊤⁺) = ⊤⁺≈⊤⁺
 
+  ≤⁺-respˡ-≈⁺ : _≤_ Respectsˡ _≈_ → _≤⁺_ Respectsˡ _≈⁺_
+  ≤⁺-respˡ-≈⁺ ≤-respˡ-≈ [ p ] [ q ] = [ ≤-respˡ-≈ p q ]
+  ≤⁺-respˡ-≈⁺ ≤-respˡ-≈ [ p ] (l ≤⊤⁺) = [ _ ] ≤⊤⁺
+  ≤⁺-respˡ-≈⁺ ≤-respˡ-≈ (⊤⁺≈⊤⁺) q = q
+
+  ≤⁺-respʳ-≈⁺ : _≤_ Respectsʳ _≈_ → _≤⁺_ Respectsʳ _≈⁺_
+  ≤⁺-respʳ-≈⁺ ≤-respʳ-≈ [ p ] [ q ] = [ ≤-respʳ-≈ p q ]
+  ≤⁺-respʳ-≈⁺ ≤-respʳ-≈ ⊤⁺≈⊤⁺ q = q
+
+  ≤⁺-resp-≈⁺ : _≤_ Respects₂ _≈_ → _≤⁺_ Respects₂ _≈⁺_
+  ≤⁺-resp-≈⁺ = Product.map ≤⁺-respʳ-≈⁺ ≤⁺-respˡ-≈⁺
+
 ------------------------------------------------------------------------
 -- Structures + propositional equality