[ add ] Pointed extension of an ordering

[jamesmckinna]

See also #2809 which this is (largely) independent from, but inspires these additions, as 'infrastructure'.

Adds:

• Directed as property simply of a raw relation
• lifting orderings to the free Pointed extension
• properties thereof, specifically ≲∙-directed

[JacquesCarette]

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?

[jamesmckinna]

See below.

But indeed, generalising may also be worthwhile, but ... downstream?

[JacquesCarette]

Can you give a reference for this definition? Google did not help me find anything relevant.

[jamesmckinna]

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?

[JacquesCarette]

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.

[jamesmckinna]

See my comments on #2829 ... I (still) think that we should isolate, and agree upon, a definition of Directed, and then use it appropriately downstream, as here, or in whatever version of DCPO we end up adopting...

[jamesmckinna]

Hmmm... if we instead go for

FinitelyDirected : Rel A ℓ → Set _
FinitelyDirected _≤_ = ∀ {n} (f : Fin n → A) → ∃[ z ] ∀ i → f i ≲ z

then n = 0 ensures that A is inhabited... and n = 2 gives us the binary definition... hmmm.

UPDATED: but introducing such a definition causes a dependency cycle between

• Relation.Binary.Definitions
• Relation.Binary.PropositionalEquality.Core
• Data.Fin.Base
  grrr....

[TOTBWF]

Directed definitely does need to include the point! The unbiased definition is cute, but ends up not being the most ergonomic definition. It's akin to defining Monoid via foldMap: this is a useful theorem, but kind of an annoying definition.

For semidirected, we could just call it HasBinaryUpperBounds or something? Also, we will want both UpwardsDirected and DownwardsDirected: we can get them by taking opposites, but experience in agda-categories shows that defining things via duality gives absolutely dreadful goals.

[jamesmckinna]

@TOTBWF As I have said elsewhere, in any deployment context in which we want a Directed gadget, adding an explicit inhabitant to the list of hypotheses is/could be seen as a 'neutral' way to resolve this question.

But given the experiments I've made on https://github.com/jamesmckinna/agda-stdlib/tree/directed I'm happy that the Fin-based version seems to have smoother consequences, including inhabitedness built-in. But adding it without further thought/refactoring leads, unfortunately, to a dependency cycle.

Reifying 'Inhabited' plus HasUpperBounds' as a record (as in the original PR, which I objected to for other reasons) may be the solution you seek, but for @JacquesCarette 's (implied) request to avoid a merely binary version (with the need for appeals to Transitiveto go beyondn = 2` in a unifiorm way) in favour of a (more) evenhandedly finitary definition.

I guess things will bottom out when DCPO/Filter/... reaches a stable point, at which point I'd be happy to refactor the original content here, namely that passage to the lifting-with-bottom-element preserve such any directedness, to such a future.