[Add] Properties for DCPOs in `Relation.Binary.Properties.Domain`

[jmougeot]

This pull request introduces new modules and properties for directed complete partial orders (DCPOs) in the Agda standard library. These additions are adapted from the 1Lab library.

The first part of this pull request is available at [Add] Initial files for Domain theory #2721 . Please comment only on the src/Relation/Binary/Properties/Domain.agda file here

Key Changes:

1. Properties of Least Upper Bounds:

• Added uniqueLub: Proves the uniqueness of least upper bounds.
• Added IsLub-cong: Demonstrates congruence of least upper bounds under equivalence.

2. Scott Continuity and Monotonicity:

• Added DirectedCompletePartialOrder+scott→monotone: Proves that Scott continuous functions are monotone.
• Added monotone∘directed: Shows that monotone functions preserve directed families.

3. Scott Continuous Functions:

• Added ScottId: Identity function as a Scott continuous function.
• Added scott-∘: Composition of Scott continuous functions.

4. Suprema and Pointwise Ordering:

• Added ⋃-pointwise : Proves pointwise ordering of suprema in directed families.

5. Scott Continuity Module:

• Added pres-⋁ : Proves preservation of least upper bounds under Scott continuous functions.

6. Conversion to Scott Continuity:

-Added to-scott: Converts monotone functions with preservation of least upper bounds into Scott continuous functions.

Source :

1Lab library

[JacquesCarette]

Could we get another review? @jamesmckinna ? @MatthewDaggitt ?

[JacquesCarette]

I've asked @e-mniang to take over this PR.

[jamesmckinna]

I've asked @e-mniang to take over this PR.

And so... I'll come back to review once they've had a chance to grok the details, and @MatthewDaggitt 's initial feedback... and I've recovered some bandwidth after the latest round of comments on #2795 and #2769 ;-)