[Add] Initial files for Domain theory

[jmougeot]

This draft pull request introduces three new files under src/Relation/Binary/Domain, providing foundational modules for domain theory in the Agda standard library. The new modules include definitions and structures such as DCPO, Lub, and ScottContinuous, aiming to extend the library's support for domain-theoretic formalizations. This is an initial draft and feedback is welcome on the design and implementation.

For the second part see the pull request : [Add] Properties for DCPOs

The definition of Lub provided here is likely better placed elsewhere in the library and may require a different name. For further discussion, see issue #2717.

Source

1Lab library

[jamesmckinna]

Any particular reason to introduce this material as a separate sub-hierarchy under Relation.Binary.Domain?

[JacquesCarette]

Any particular reason to introduce this material as a separate sub-hierarchy under Relation.Binary.Domain?

Increased findability, because of the occurrence of Domain, I would think. This is a port from 1lab, where it uses an Order hierarchy where we "bury" a lot of stuff down into Relation.Binary. In retrospect, I think 1lab's scheme is better.

In any case, for agda-stdlib, the clear precedent is that Lattice hierarchy, which this follows.

[JacquesCarette]

Could you please resolve the CHANGELOG conflicts?

[JacquesCarette]

Also: you don't seem to have addressed the latest 2 items that I asked about?

[JacquesCarette]

Depending on what others think (and my review being taken into account), I do think this could make it to 2.3.

[jamesmckinna]

Suggest that we close in favour of #2809 ?

[JacquesCarette]

Since the attributions are correct in that further PR, it's probably best to close this one.