[Add] Initial files for Domain theory by jmougeot · Pull Request #2721 · agda/agda-stdlib

jmougeot · 2025-05-26T21:38:29Z

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 · 2025-05-28T15:20:48Z

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

JacquesCarette · 2025-05-28T18:44:02Z

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.

src/Relation/Binary/Domain/Definitions.agda

src/Relation/Binary/Domain/Structures.agda

MatthewDaggitt · 2025-06-02T02:51:08Z

src/Relation/Binary/Domain/Structures.agda

+  record IsDirectedFamily {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+    no-eta-equality
+    field
+      elt : Ix


What does elt stand for?

elt stands for element, should I change it ?

src/Relation/Binary/Domain/Structures.agda

src/Relation/Binary/Domain/Bundles.agda

src/Padrightpropertiesdraft.agda

JacquesCarette · 2025-06-04T18:28:25Z

src/Relation/Binary/Domain/Structures.agda

+  A B : Set a
+
+
+module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where


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.

The definition doesn't need a Poset, but this is essentially always going to be used with a Poset/Preorder. Using a bare relation could cause rather poor inference later down the line, so I'd hesitate a bit on this generalization.

We could also use a Preorder here, but that doesn't really buy us much. Doing posetal completions is really, really cheap with setoids, and the preorder versions of lemmas would be essentially the same thing as the plugging in a posetal completion to a poset-based version.

Speaking of which: is posetal completion anywhere in the stdlib?

Looping back to @TOTBWF 's question re poset completion: no. Please consider adding to stdlib!
As for 'not buying much' between Preorder and Poset, we tend to try to state (and prove!) things wrt maximum-sensible generality, and antisymmetry feels like 'noise' much of the time in developing the basics... but YMMV.

Apologies, I think I was wrong on poset completion: I think that

agda-stdlib/src/Relation/Binary/Construct/Interior/Symmetric.agda

Lines 84 to 107 in 54f5c38

module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where

isEquivalence : IsEquivalence (SymInterior R)

isEquivalence = record

{ refl = reflexive refl

; sym = symmetric

; trans = transitive trans

}

isPreorder : IsPreorder (SymInterior R) R

isPreorder = record

{ isEquivalence = isEquivalence

; reflexive = lhs≤rhs

; trans = trans

}

isPartialOrder : IsPartialOrder (SymInterior R) R

isPartialOrder = record

{ isPreorder = isPreorder

; antisym = _,_

}

poset : Poset _ ℓ ℓ

poset = record { isPartialOrder = isPartialOrder }

gives you what you want, but not necessarily in a recognisable form... I had to think about it a bit harder while looping back to #2070 / #2071

src/Relation/Binary/Domain/Definitions.agda

JacquesCarette · 2025-06-16T20:11:35Z

src/Relation/Binary/Domain/Definitions.agda

+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain.Definitions where


Given that neither of the definitions here depend on Poset (now), maybe they should go where all the other binary relations are defined?

What I mean is that all 3 definitions below should be moved to Relation.Binary.Definitions, with the naming made consistent with the names already in that file.

JacquesCarette · 2025-06-19T14:20:30Z

Could you please resolve the CHANGELOG conflicts?

JacquesCarette · 2025-06-19T14:22:50Z

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

JacquesCarette · 2025-06-26T14:05:39Z

src/Relation/Binary/Domain/Definitions.agda

+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain.Definitions where


What I mean is that all 3 definitions below should be moved to Relation.Binary.Definitions, with the naming made consistent with the names already in that file.

JacquesCarette · 2025-06-26T14:11:39Z

src/Relation/Binary/Domain/Structures.agda

+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain.Structures where


To 'fit' the rest of stdlib, even though this is all "most useful" for a full Poset, these structures should be in terms of a RawRelation, as that is all that is used in the definitions.

See my latest round of comments on #2809 ... further input from you would be welcome!

JacquesCarette · 2025-06-26T15:25:31Z

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

jamesmckinna · 2025-08-14T15:13:20Z

Suggest that we close in favour of #2809 ?

JacquesCarette · 2025-08-22T18:16:39Z

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

Definitons of domain theory

4486fd0

jmougeot force-pushed the domain_part1 branch from 1841d6e to 4486fd0 Compare May 26, 2025 23:12

MatthewDaggitt requested changes Jun 2, 2025

View reviewed changes

MatthewDaggitt added the addition label Jun 2, 2025

jmougeot added 3 commits June 3, 2025 14:14

1st review

34be6b0

whitespaces

502e288

@ review

63810b7

JacquesCarette requested changes Jun 4, 2025

View reviewed changes

remove the file Padrightdraft

87d5f16

jmougeot marked this pull request as ready for review June 9, 2025 22:49

jmougeot mentioned this pull request Jun 11, 2025

[Add] Properties for DCPOs in Relation.Binary.Properties.Domain #2734

Open

jmougeot requested a review from JacquesCarette June 16, 2025 18:20

quick fix

51954b6

JacquesCarette requested changes Jun 16, 2025

View reviewed changes

jmougeot requested review from JacquesCarette and MatthewDaggitt June 17, 2025 15:34

jmougeot added 5 commits June 24, 2025 14:11

add using to importation

85192d0

add perserveLub in defintion

ceb39d6

fixwhitespace

2384bd3

{I} instead of I

b753478

remove file

1e41d41

JacquesCarette requested changes Jun 26, 2025

View reviewed changes

gabriellisboaconegero mentioned this pull request Aug 13, 2025

[Add] Initial files for Domain theory - Continuation of #2721 #2809

Open

jamesmckinna mentioned this pull request Aug 18, 2025

Orders without equivalence relations #2070

Closed

jamesmckinna mentioned this pull request Aug 20, 2025

Predomains #2811

Closed

JacquesCarette closed this Aug 22, 2025

		A B : Set a


		module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where

	module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where

	isEquivalence : IsEquivalence (SymInterior R)
	isEquivalence = record
	{ refl = reflexive refl
	; sym = symmetric
	; trans = transitive trans
	}

	isPreorder : IsPreorder (SymInterior R) R
	isPreorder = record
	{ isEquivalence = isEquivalence
	; reflexive = lhs≤rhs
	; trans = trans
	}

	isPartialOrder : IsPartialOrder (SymInterior R) R
	isPartialOrder = record
	{ isPreorder = isPreorder
	; antisym = _,_
	}

	poset : Poset _ ℓ ℓ
	poset = record { isPartialOrder = isPartialOrder }


		{-# OPTIONS --cubical-compatible --safe #-}

		module Relation.Binary.Domain.Definitions where


		{-# OPTIONS --cubical-compatible --safe #-}

		module Relation.Binary.Domain.Structures where

Conversation

jmougeot commented May 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Source

Uh oh!

jamesmckinna commented May 28, 2025

Uh oh!

JacquesCarette commented May 28, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jmougeot Jun 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

JacquesCarette commented Jun 19, 2025

Uh oh!

JacquesCarette commented Jun 19, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

JacquesCarette commented Jun 26, 2025

Uh oh!

jamesmckinna commented Aug 14, 2025

Uh oh!

JacquesCarette commented Aug 22, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

jmougeot commented May 26, 2025 •

edited

Loading

jmougeot Jun 5, 2025 •

edited

Loading