[Add] Properties for DCPOs in Relation.Binary.Properties.Domain
#2734
Conversation
jmougeot
changed the title
Relation.Binary.Properties.DomainRelation.Binary.Properties.Domain
| record IsScottContinuous (f : P.Carrier → Q.Carrier) | ||
| : Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where | ||
| field | ||
| preserveLub : ∀ {B : Set c₁} {g : B → P.Carrier} |
There was a problem hiding this comment.
I don't think this layout is as per the style guide.
|
Could we get another review? @jamesmckinna ? @MatthewDaggitt ? |
| ------------------------------------------------------------------------ | ||
|
|
||
| -- IsSemidirectedFamily : (P : Poset c ℓ₁ ℓ₂) → ∀ {Ix : Set c} → (s : Ix → Poset.Carrier P) → Set _ | ||
| -- IsSemidirectedFamily P {Ix} s = ∀ i j → ∃[ k ] (Poset._≤_ P (s i) (s k) × Poset._≤_ P (s j) (s k)) |
There was a problem hiding this comment.
This should either be removed or uncommented?
| -- IsSemidirectedFamily : (P : Poset c ℓ₁ ℓ₂) → ∀ {Ix : Set c} → (s : Ix → Poset.Carrier P) → Set _ | ||
| -- IsSemidirectedFamily P {Ix} s = ∀ i j → ∃[ k ] (Poset._≤_ P (s i) (s k) × Poset._≤_ P (s j) (s k)) | ||
|
|
||
| semidirected : {A : Set a} → Rel A ℓ → (B : Set b) → (B → A) → Set _ |
There was a problem hiding this comment.
This implicit {A} is already available as a variable? Can B not be made implicit as well? It feels like it should be inferable from B -> A?
| -- Least upper bounds | ||
| ------------------------------------------------------------------------ | ||
|
|
||
| leastupperbound : {A : Set a} → Rel A ℓ → (B : Set b) → (B → A) → A → Set _ |
There was a problem hiding this comment.
The capitalisation on this name is odd. Same comments as before though.
|
|
||
|
|
||
|
|
||
|
|
There was a problem hiding this comment.
Too much whitespace.
| A B : Set a | ||
|
|
||
|
|
||
| module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where |
There was a problem hiding this comment.
c ℓ₁ ℓ₂ already exist as variables.
| isLeast : ∀ y → (∀ i → f i ≤ y) → lub ≤ y | ||
| isLeast = proj₂ isLeastUpperBound | ||
|
|
||
| record IsDirectedFamily {b : Level} {B : Set b} (f : B → Carrier) |
| open Poset P | ||
|
|
||
| record IsLub {b : Level} {B : Set b} (f : B → Carrier) | ||
| (lub : Carrier) : Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where |
There was a problem hiding this comment.
What's the point of this record if it just wraps leastupperbound?
| module _ {B : Set c} {f : B → Carrier} {dir : IsDirectedFamily f} where | ||
| open IsLub (⋁-isLub f dir) | ||
| renaming (isUpperBound to ⋁-≤; isLeast to ⋁-least) | ||
| public |
There was a problem hiding this comment.
public should before renaming according to the style guide
| elt : B | ||
| isSemidirected : semidirected _≤_ B f | ||
|
|
||
| record IsDirectedCompletePartialOrder : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where |
There was a problem hiding this comment.
These levels look deeply suspicious. It feels like the c level shouldn't exposed in the interface. I know you'll run into level problems in the type of the record if you internalise it so I'm not sure what the solution is, but it feels like a strong code smell.
| : Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where | ||
| no-eta-equality | ||
| field | ||
| elt : B |
There was a problem hiding this comment.
Is this simply trying to encode the fact that B is non-empty? Wouldn't be better to define and use a NonEmpty type (probably defining it in Relation.Nullary if it is not already there)
|
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 ;-) |
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.agdafile hereKey Changes:
1. Properties of Least Upper Bounds:
uniqueLub:Proves the uniqueness of least upper bounds.IsLub-cong: Demonstrates congruence of least upper bounds under equivalence.2. Scott Continuity and Monotonicity:
DirectedCompletePartialOrder+scott→monotone: Proves that Scott continuous functions are monotone.3. Scott Continuous Functions:
ScottId: Identity function as a Scott continuous function.scott-∘: Composition of Scott continuous functions.4. Suprema and Pointwise Ordering:
⋃-pointwise: Proves pointwise ordering of suprema in directed families.5. Scott Continuity Module:
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