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

gabriellisboaconegero · 2025-08-13T20:41:43Z

This pull request aims to continue and complete the work started in #2721

The first version already includes changes requested by @JacquesCarette, such as moving the definition of DirectedFamily to Relation.Binary.Definitions.agda and IsDirectedFamily to Relation.Binary.Structures.agda, as well as the proper bundling of Lub.

jamesmckinna

Thanks for picking up from @jmougeot 's initial contribution.
I don't think this design is quite ready yet, and needs more thought wrt:

placement of concepts
naming of them
parametrisation of them

At a first cut, I'm not quite clear what should go where, so will need to think about this more, but this is a prompt to other reviewers also to think about these questions. It seems that I might be in conflict with @JacquesCarette over what the right answers might be!?

jamesmckinna · 2025-08-14T14:21:37Z

src/Relation/Binary/Structures.agda

+record IsDirectedFamily {b : Level} {B : Set b} (_≤_ : Rel A ℓ₂) (f : B → A) :
+                        Set (a ⊔ b ⊔ ℓ₂) where
+  field
+    elt            : B


We might want to revisit this name before committing to it? eg inhabitant as an alternative?

Perhaps point?

Else reuse the symbol from Relation.Construct.Add.Point?

Indeed, why make the point explicit (in B) at all?
Is this definition equivalent to one where, instead of f : B → A with b : B, we instead consider arbitrary f : B → A, together with rephrasing SemiDirected in terms of Maybe B → A (so the assumption shifts to A being inhabited..., so that such a lifting is definable?), together with the canonical lifting of a relation on B to one on Maybe B which makes nothing ≤ anything and just x ≤ just y = x ≤ y?

This makes the definition much clunkier to use for types that are already inhabited. For example, every DCPO is an omega-CPO, but proving this with a Maybe in the definition of a directed family would require you to fiddle with Maybe Nat when constructing the family which adds a lot of incidental complexity.

See #2811 for comparison.

The two are not equivalent: it's important that the distinguished point be in the set/family we are taking a join of. Joins over the empty set give you a bottom element, and not every DCPO has a bottom.

A good counter example of this is the order on non-empty subsets of Nat (though any type with at least two distinct elements will do). This actually has joins of all nonempty subsets via union, and is nonempty. However, it does not have a bottom.

So I'm clear about making the bottom-/non-bottom- containing distinction in #2811 ; my real concern with making b part of the data for a directed family, rather than its image under f in A is one of artificiality/unnaturalness in terms of the encoding, when, at least morally as I understand it, and the counterexamples don't appear to contradict, is that such f b can be chosen so as to be a lower bound on any hypothetical lub associated with the family. That's the view made concrete in #2811 , and indeed as you point out, is reconciled (or at least, appears to be) with the one here in the presence of bottoms. But you're right, I should try to express your example in Pow(Nat) in those terms, so thanks for that!

As it currently stands, #2811 has the problem I mentioned with bottoms.

You can try and ask for an element of A along with a point in the setoidal fibre of the family (EG, an x : P and a b : B such that f b P.≈ x but this is quite a bit of extra data.

The definition here already has too much data to begin with, as we should only require the mere existence of an element of B and the mere existence of upper bounds. A 100% correct definition would impose an equivalence relation on the type of directed families that essentially truncates away the point and upper bounds, and then require that the joins be congruent with respect to that relation. However, this seems to be against the stdlib style, as these sorts of truncations don't seem common.

Regarding the last paragraph, one way to introduce truncation, at least as I imperfectly understand it, would be to mark fields as irrelevant with a dot, so that there can be no dependency in their actual witness. But that may still not be enough for a 1lab-style definition.

But such considerations are taking us well beyond this individual PR... so I think in the interests of making progress on it, I'm going to step back from the reviewing discussion.

jamesmckinna · 2025-08-14T14:23:46Z

src/Relation/Binary/Structures.agda

+                        Set (a ⊔ b ⊔ ℓ₂) where
+  field
+    elt            : B
+    isSemidirected : SemiDirected _≤_ f


This doesn't seem to be consistent... wrt our naming conventions camelCase : CamelCase, nor wrt use of isX to refer to an IsX *structure...

Suggested change

isSemidirected : SemiDirected _≤_ f

semiDirected : SemiDirected _≤_ f

Last thoughts on this/suggestion:

because the concept of DirectedFamily is used only as an argument to the definitions of ⋁ and ⋁-isLub, it's probably simpler still to avoid reifying the notion entirely, and simply make a telescope of assumptions

as elsewhere in this discussion, if you want to remove explicit dependency on any choice of b : B, then it might be easiest to mark that argument as irrelevant

yielding:

⋁ : ∀ {I : Set c} → .I → (f : I → Carrier) → Directed (_≤_ on f) → Carrier ⋁-isLub : ∀ {I : Set c} .(i : I) (f : I → Carrier) (d : Directed (_≤_ on f)) → IsLub f (⋁ i f dir)

jamesmckinna · 2025-08-14T14:28:38Z

src/Relation/Binary/Domain/Structures.agda

+module _ (P : Poset c ℓ₁ ℓ₂) where
+  open Poset P


I think that this has come up before in this context; we tend to define this kind of parametrised record on the underlying Raw structure (because none of the axioms for a Poset are involved in the definition, only the underlying relations).

Not least because domain theory ought better to be built on Preorder-based foundations? Antisymmetry plays almost no direct role in the axiomatisation of the concepts you define?

Anyway: meta design principle is/ought to be 'structures don't depend on bundles'

I think (but happy to be contradicted) that UpperBound, Lub, DirectedFamily all belong in Relation.Binary.Domain.Definitions

You can blame this on me 😁

In setoid-based foundations, it doesn't really make sense to found order theory on preorders. To see why, let's look at a very relevant example: uniqueness of lubs. In a poset (P, _≈_, _≤_), if IsLub f x and IsLub f y, then we get x ≈ y. Conversely, if P is a preorder, the best we can do is (x ≤ y) × (y ≤ x). This looks something like the following:

module PosetAPI (P : Poset) where open Poset P Lub-unique : ∀ {Ix : Set} {f : Ix → Carrier} {x y} → IsLub f x → IsLub f y → x ≈ y Lub-unique = ... module PreorderAPI (P : Preorder) where open Preorder P Lub-unique : ∀ {Ix : Set} {f : Ix → Carrier} {x y} → IsLub f x → IsLub f y → (x ≤ y) × (y ≤ x) Lub-unique = ...

However, we can complete any preorder P to a poset PosetalCompletion P by replacing the equivalence relation on P with (x ≤ y × y ≤ x). If we instantiate the PosetAPI with PosetalCompletion P, we will get
exactly the theorem in PreorderAPI, so you don't lose any generality by just considering posets. In fact, you get a more general API: PreorderAPI is just PosetAPI with a particular choice of equivalence relation 🙂 .

As for parameterising by raw structures, my comments about poor inference from the last PR are still relevant. I don't really see anyone considering least-upper bounds in a raw structure, so the tradeoff of generality for inference performance doesn't seem worth it here. There is a lot of precedence for this choice in agda-categories: for instance, we don't ever talk about products in a raw category.

I commented on posetal completion on #2721 , sorry for that.

As for parametrisation by a Poset, also see my previous remarks about this form of 'structure on bundle' dependency being not the prevailing design heuristic of stdlib. As to what 'really' happens/should, and justification-by-precedent for alternative design philosophies/policies from other agda libraries or elsewhere, that's a bigger question than can be solved in one PR, so suggest it be opened as a library-design/discussion issue...

jamesmckinna · 2025-08-14T14:30:45Z

src/Relation/Binary/Domain/Structures.agda

+module _ (P : Poset c ℓ₁ ℓ₂) where
+  open Poset P
+
+  record IsLub {b : Level} {B : Set b} (f : B → Carrier)


b is already implicitly bound by a variable declaration (as is B!), so shouldn't need explicit mention here.

jamesmckinna · 2025-08-14T14:31:27Z

src/Relation/Binary/Domain/Structures.agda

+  record IsLub {b : Level} {B : Set b} (f : B → Carrier)
+               (lub : Carrier) : Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isUpperBound : UpperBound _≤_ f lub


camelCase : CamelCase is the usual convention in stdlib, accordingly:

Suggested change

isUpperBound : UpperBound _≤_ f lub

upperBound : UpperBound _≤_ f lub

jamesmckinna · 2025-08-14T14:33:05Z

src/Relation/Binary/Domain/Structures.agda

+               (lub : Carrier) : Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isUpperBound : UpperBound _≤_ f lub
+      isLeast : ∀ y → UpperBound _≤_ f y → lub ≤ y


Suggested change

isLeast : ∀ y → UpperBound _≤_ f y → lub ≤ y

minimal : ∀ y → UpperBound _≤_ f y → lub ≤ y

because being least only follows from the Poset axioms, whereas in their absence (as above), we only have/need a minimal upper bound?

jamesmckinna · 2025-08-14T14:47:46Z

src/Relation/Binary/Domain/Structures.agda

+    field
+      ⋁ : ∀ {B : Set c} →
+        (f : B → Carrier) →
+        IsDirectedFamily _≈_ _≤_ f →


The definition you give of IsDirectedFamily is only accidentally dependent on the underlying Setoid equality relation _≈_, so either you need to involve it by making f a suitable congruence wrt it, or else reconsider whether IsDirectedFamily really belongs in Relation.Binary.Structures?

As this stands, I think the design doesn't quite fit properly with the existing stdlib hierarchy.

Moreover, it's not a priori obvious that ⋁ should depend on its dir argument, as opposed to that clearly being a necessary precondition to ⋁-isLub...

This would no longer be a DCPO if that were the case.

jamesmckinna · 2025-08-14T14:51:33Z

src/Relation/Binary/Structures.agda

+-- DirectedFamily
+------------------------------------------------------------------------
+
+record IsDirectedFamily {b : Level} {B : Set b} (_≤_ : Rel A ℓ₂) (f : B → A) :


I'm not sure that this definition belongs in Relation.Binary.Structures, because it's not actually (an extension of) any of the existing relational structures, rather it's a property that any one of them might additionally possess?

jamesmckinna · 2025-08-18T14:41:35Z

src/Relation/Binary/Domain/Structures.agda

+    record IsScottContinuous (f : P.Carrier → Q.Carrier) (κ : Level) : Set (suc (κ ⊔ c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂))
+      where
+      field
+        preservelub : ∀ {I : Set κ} → ∀ {g : I → _} → ∀ lub → IsLub P g lub → IsLub Q (f ∘ g) (f lub)
+        isOrderHomomorphism : IsOrderHomomorphism P._≈_ Q._≈_ P._≤_ Q._≤_ f
+
+      open IsOrderHomomorphism isOrderHomomorphism public


This looks as though it better belongs under Relation.Binary.Domain.Morphism.Structures, defining, say IsContinuousHomomorphism (Scott feels optional here? unless you think that such a qualifier is specific to directed complete orders?), and with a field name ⋁-homo would be more consistent with existing cognate names under Algebra.Morphism.Structures.IsXHomomorphism?

See also: #2812 . Can the definition be simplified to exploit that:

preservesLub implies mono

mono implies cong in the presence of antisym

and hence that preservesLub suffices?

jamesmckinna · 2025-08-18T16:18:15Z

src/Relation/Binary/Definitions.agda

+SemiDirected : Rel A ℓ → (B → A) → Set _
+SemiDirected _≤_ f = ∀ i j → ∃[ k ] (f i ≤ f k × f j ≤ f k)


So... after thinking about this for quite a bit, would it make (better) sense to factorise this definition so that

SemiDirected refers only to the underlying relation, as: ∀ (x y : A) → ∃[ z ] (x ≤ z × y ≤ z)

given _≤_ : Rel A ℓ, and f : B → A we obtain an ordering _≤[ f ]_ on B by i ≤[ f ] k = f i ≤ f k (given by _≤_ on f using Function.Base._on_)

then the above definition is definitionally equal to SemiDirected _≤[ f ]_

UPDATED: see #2813

I'm stepping back from reviewing this PR.

JacquesCarette · 2025-08-22T18:52:26Z

I'm going to try to have an in-person discussion (with @TOTBWF and @gabriellisboaconegero ) early next week to try to hash things out.

The main thing to discuss will be the differences in design between "in Agda in general", stdlib-style and 1lab-style. I have definitely participated in designs for stdlib that I personally consider sub-optimal but they are consistent with the rest of stdlib. Reading the many comments, this seems to be what's going on here, a clash of styles. And a non-trivial one at that, as a stdlib-coherent set of definitions may well be sub-optimal wrt what can be done in Agda in a standalone library.

jmougeot and others added 12 commits May 26, 2025 19:07

Definitons of domain theory

4486fd0

1st review

34be6b0

whitespaces

502e288

@ review

63810b7

remove the file Padrightdraft

87d5f16

quick fix

51954b6

add using to importation

85192d0

add perserveLub in defintion

ceb39d6

fixwhitespace

2384bd3

{I} instead of I

b753478

remove file

1e41d41

Remove leastupperbound. Move directed family to more general files

a679d07

jamesmckinna previously requested changes Aug 14, 2025

View reviewed changes

This was referenced Aug 14, 2025

[Add] Initial files for Domain theory #2721

Closed

Orders without equivalence relations #2070

Closed

jamesmckinna reviewed Aug 18, 2025

View reviewed changes

This was referenced Aug 20, 2025

Predomains #2811

Closed

[ add ] Pointed extension of an ordering #2813

Open

gabriellisboaconegero mentioned this pull request Sep 11, 2025

Filters - alternative to the base of Domain theory #2829

Open

	isSemidirected : SemiDirected _≤_ f
	semiDirected : SemiDirected _≤_ f

	isUpperBound : UpperBound _≤_ f lub
	upperBound : UpperBound _≤_ f lub

	isLeast : ∀ y → UpperBound _≤_ f y → lub ≤ y
	minimal : ∀ y → UpperBound _≤_ f y → lub ≤ y

		SemiDirected : Rel A ℓ → (B → A) → Set _
		SemiDirected _≤_ f = ∀ i j → ∃[ k ] (f i ≤ f k × f j ≤ f k)

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

Are you sure you want to change the base?

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

Uh oh!

Conversation

gabriellisboaconegero commented Aug 13, 2025

Uh oh!

jamesmckinna left a comment • 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!

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!

TOTBWF Aug 18, 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!

Choose a reason for hiding this comment

Uh oh!

TOTBWF Aug 20, 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!

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!

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!

jamesmckinna Aug 14, 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!

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!

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!

jamesmckinna Aug 18, 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!

JacquesCarette commented Aug 22, 2025

Uh oh!

Uh oh!

jamesmckinna left a comment •

edited

Loading

TOTBWF Aug 18, 2025 •

edited

Loading

TOTBWF Aug 20, 2025 •

edited

Loading

jamesmckinna Aug 14, 2025 •

edited

Loading

jamesmckinna Aug 18, 2025 •

edited

Loading