From e6f00ba6501e6c21a5bdfa61610f9f7866ea64a8 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 20 Aug 2025 14:43:21 +0100 Subject: [PATCH 1/2] [ add ] `Pointed` lift of an order relation --- CHANGELOG.md | 8 ++++++++ src/Relation/Binary/Definitions.agda | 5 +++++ 2 files changed, 13 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 081dda5b66..6e2fee1786 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda index 80b9e5ff44..ad86037346 100644 --- a/src/Relation/Binary/Definitions.agda +++ b/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 _ From 328f322abb43baf0c68b8e298ffd61cde75ecec7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 20 Aug 2025 18:01:31 +0100 Subject: [PATCH 2/2] add: actual file --- .../Binary/Construct/Add/Point/Order.agda | 109 ++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 src/Relation/Binary/Construct/Add/Point/Order.agda diff --git a/src/Relation/Binary/Construct/Add/Point/Order.agda b/src/Relation/Binary/Construct/Add/Point/Order.agda new file mode 100644 index 0000000000..6de02083ce --- /dev/null +++ b/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