Adding extrema to a non-strict order respects equality

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

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
 

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
 

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