[ add ] Pointed extension of an ordering
#2813
Conversation
| @@ -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 | |||
There was a problem hiding this comment.
Why binary? Don't you want to say that for any I-indexed family of points, there's a 'z' that is below all of them?
There was a problem hiding this comment.
See below.
But indeed, generalising may also be worthwhile, but ... downstream?
| @@ -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 _ | |||
There was a problem hiding this comment.
Can you give a reference for this definition? Google did not help me find anything relevant.
There was a problem hiding this comment.
https://en.wikipedia.org/wiki/Directed_set
The definition is taken from #2809 where it is currently called SemiDirected, but/and I'm not sure the Semi really makes sense. Moreover its use there can be (better?) refactored into this one, plus a use of change-of-base via _on_. So it definitely seems worth adding on its own terms, in some form or other.
The official definition requires A also to be inhabited (which can be finessed in any mode-of-use by an additional assumption x : A), but the 'condition' is indeed this one of having binary (and hence: any finite) upper bounds.
The lemma ≲∙-directed is precisely motivated by the observation that any relation satisfying the condition may be freely completed (preserving and reflecting the existing instances) to an inhabited relation satisfying the condition. It is the core of the 'lifting' construction on (pre)domains, but is minimal wrt its commitments to any other properties of the underlying relation. Not finding such a lemma motivated this PR as an addition/'infrastructure'...
But it perhaps/probably makes more sense to uncouple the definition of Relation.Binary.Construct.Add.Point.Order from these considerations, until we agree on suitable names/definitions for 'directed'ness as a property?
There was a problem hiding this comment.
Thanks - and @TOTBWF also expanded on this. There's a fairly non-trivial refactor of that PR incoming, after we discussed how to make things more stdlib-friendly.
See also #2809 which this is (largely) independent from, but inspires these additions, as 'infrastructure'.
Adds:
Directedas property simply of a raw relationPointedextension≲∙-directed