[ add ] Pointed extension of an ordering

CHANGELOG.md

@@ -48,6 +48,9 @@ New modules
 
 * `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.
 
+* `Relation.Binary.Construct.Add.Point.Order` to extend a given (order) relation so that
+  the point is below everything else in `Pointed A`.
+
 Additions to existing modules
 -----------------------------
 
@@ -99,6 +102,11 @@ 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.Definitions`
+  ```agda
+  Directed _≤_ = ∀ x y → ∃[ z ] x ≤ z × y ≤ z
+  ```
+
 * In `Relation.Nullary.Negation.Core`
   ```agda
   ¬¬-η : A → ¬ ¬ A

src/Relation/Binary/Construct/Add/Point/Order.agda

@@ -0,0 +1,109 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A pointwise lifting of a relation to incorporate an additional point,
+-- assumed to be 'below' everything else in `Pointed A`.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+-- This module is designed to be used with
+-- Relation.Nullary.Construct.Add.Point
+
+open import Relation.Binary.Core using (Rel; _⇒_)
+
+module Relation.Binary.Construct.Add.Point.Order
+  {a ℓ} {A : Set a} (_≲_ : Rel A ℓ) where
+
+open import Data.Product.Base using (_,_)
+open import Level using (Level; _⊔_)
+open import Function.Base using (id; _∘_; _∘′_)
+import Relation.Binary.Construct.Add.Point.Equality as Equality
+open import Relation.Binary.Structures
+  using (IsPreorder; IsPartialOrder)
+open import Relation.Binary.Definitions
+  using (Reflexive; Transitive; Antisymmetric; Directed; Decidable; Irrelevant)
+import Relation.Binary.PropositionalEquality.Core as ≡
+open import Relation.Nullary.Decidable.Core as Dec
+  using (yes; no)
+open import Relation.Nullary.Construct.Add.Point as Point
+  using (Pointed; ∙ ;[_])
+
+
+private
+  variable
+    ℓ′ : Level
+    x∙ : Pointed A
+    x y : A
+
+------------------------------------------------------------------------
+-- Definition
+
+infix 4 _≲∙_
+
+data _≲∙_ : Rel (Pointed A) (a ⊔ ℓ) where
+  ∙≲_ : ∀ x∙  → ∙     ≲∙ x∙
+  [_] : x ≲ y → [ x ] ≲∙ [ y ]
+
+pattern ∙≲∙ = ∙≲ ∙
+
+------------------------------------------------------------------------
+-- Relational properties
+
+[≲]-injective : [ x ] ≲∙ [ y ] → x ≲ y
+[≲]-injective [ x≲y ] = x≲y
+
+≲∙-refl : Reflexive _≲_ → Reflexive _≲∙_
+≲∙-refl ≲-refl {∙}     = ∙≲∙ 
+≲∙-refl ≲-refl {[ x ]} = [ ≲-refl ]
+
+≲∙-trans : Transitive _≲_ → Transitive _≲∙_
+≲∙-trans ≲-trans (∙≲ _)  _       = ∙≲ _
+≲∙-trans ≲-trans [ x≲y ] [ y≲z ] = [ ≲-trans x≲y y≲z ]
+
+≲∙-directed : Directed _≲_ → Directed _≲∙_
+≲∙-directed dir ∙     ∙     = ∙ , ∙≲∙ , ∙≲∙
+≲∙-directed dir [ x ] ∙     = let z , x≲z , _ = dir x x in [ z ] , [ x≲z ] , (∙≲ _)
+≲∙-directed dir ∙     [ y ] = let z , _ , y≲z = dir y y in [ z ] , (∙≲ _) , [ y≲z ]
+≲∙-directed dir [ x ] [ y ] = let z , x≲z , y≲z = dir x y in [ z ] , [ x≲z ] , [ y≲z ]
+
+≲∙-dec : Decidable _≲_ → Decidable _≲∙_
+≲∙-dec _≟_ ∙     _     = yes (∙≲ _)
+≲∙-dec _≟_ [ x ] ∙     = no λ()
+≲∙-dec _≟_ [ x ] [ y ] = Dec.map′ [_] [≲]-injective (x ≟ y)
+
+≲∙-irrelevant : Irrelevant _≲_ → Irrelevant _≲∙_
+≲∙-irrelevant ≲-irr (∙≲ _) (∙≲ _) = ≡.refl
+≲∙-irrelevant ≲-irr [ p ]  [ q ]  = ≡.cong _ (≲-irr p q)
+
+------------------------------------------------------------------------
+-- Relativised to a putative `Setoid`
+
+module _ {_≈_ : Rel A ℓ′} where
+
+  open Equality _≈_
+
+  ≲∙-reflexive : (_≈_ ⇒ _≲_) → (_≈∙_ ⇒ _≲∙_)
+  ≲∙-reflexive ≲-reflexive ∙≈∙     = ∙≲∙
+  ≲∙-reflexive ≲-reflexive [ x≈y ] = [ ≲-reflexive x≈y ]
+
+  ≲∙-antisym : Antisymmetric _≈_ _≲_ →  Antisymmetric _≈∙_ _≲∙_
+  ≲∙-antisym ≲-antisym ∙≲∙     ∙≲∙     = ∙≈∙
+  ≲∙-antisym ≲-antisym [ x≤y ] [ y≤x ] = [ ≲-antisym x≤y y≤x ]
+
+------------------------------------------------------------------------
+-- Structures
+
+  ≲∙-isPreorder : IsPreorder _≈_ _≲_ → IsPreorder _≈∙_ _≲∙_
+  ≲∙-isPreorder ≲-isPreorder = record
+    { isEquivalence = Equality.≈∙-isEquivalence _ isEquivalence
+    ; reflexive  = ≲∙-reflexive reflexive
+    ; trans = ≲∙-trans trans
+    } where open IsPreorder ≲-isPreorder
+
+
+  ≲∙-isPartialOrder : IsPartialOrder _≈_ _≲_ → IsPartialOrder _≈∙_ _≲∙_
+  ≲∙-isPartialOrder ≲-isPartialOrder = record
+    { isPreorder = ≲∙-isPreorder isPreorder
+    ; antisym = ≲∙-antisym antisym
+    } where open IsPartialOrder ≲-isPartialOrder

src/Relation/Binary/Definitions.agda

@@ -96,6 +96,11 @@ Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)
 Dense : Rel A ℓ → Set _
 Dense _<_ = ∀ {x y} → x < y → ∃[ z ] x < z × z < y
 
+-- Directedness (but: we drop the inhabitedness condition)
+
+Directed : Rel A ℓ → Set _
+Directed _≤_ = ∀ x y → ∃[ z ] x ≤ z × y ≤ z
+
 -- Generalised connex - at least one of the two relations holds.
 
 Connex : REL A B ℓ₁ → REL B A ℓ₂ → Set _