[Add] Initial files for Domain theory #2721
Conversation
|
Any particular reason to introduce this material as a separate sub-hierarchy under |
Increased findability, because of the occurrence of In any case, for |
| record IsDirectedFamily {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where | ||
| no-eta-equality | ||
| field | ||
| elt : Ix |
There was a problem hiding this comment.
What does elt stand for?
There was a problem hiding this comment.
elt stands for element, should I change it ?
| record IsDCPO : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where | ||
| field | ||
| ⋁ : ∀ {Ix : Set c} | ||
| → (s : Ix → Carrier) |
There was a problem hiding this comment.
Please use the standard formatting for laying out types over multiple lines (see the library style guide)
| A B : Set a | ||
|
|
||
|
|
||
| module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where |
There was a problem hiding this comment.
Do these definitions really need a Poset or just a relation? I don't immediately see the use of any of the other fields of Poset below.
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.
This is an import from the 1Lab library.
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.