From b3d1a805c82a722c82d0280fdb3dc9e011680318 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 19 Aug 2025 19:25:00 +0100
Subject: [PATCH 1/6] add: definition of `Directed` order

---
 CHANGELOG.md                         | 5 +++++
 src/Relation/Binary/Definitions.agda | 5 +++++
 2 files changed, 10 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 081dda5b66..18c7183b20 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -99,6 +99,11 @@ Additions to existing modules
                     updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ padRight m≤n x (updateAt xs i f)
   ```
 
+* In `Relation.Binary.Definitions`
+  ```agda
+  Directed _≤_ = ∀ x y → ∃[ z ] x ≤ z × y ≤ z
+  ```
+
 * In `Relation.Nullary.Negation.Core`
   ```agda
   ¬¬-η : A → ¬ ¬ A
diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda
index 80b9e5ff44..2e20790d10 100644
--- a/src/Relation/Binary/Definitions.agda
+++ b/src/Relation/Binary/Definitions.agda
@@ -96,6 +96,11 @@ Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)
 Dense : Rel A ℓ → Set _
 Dense _<_ = ∀ {x y} → x < y → ∃[ z ] x < z × z < y
 
+-- Directedness
+
+Directed : Rel A ℓ → Set _
+Directed _≤_ = ∀ x y → ∃[ z ] x ≤ z × y ≤ z
+
 -- Generalised connex - at least one of the two relations holds.
 
 Connex : REL A B ℓ₁ → REL B A ℓ₂ → Set _

From b90eefbf3860d53d36d9d6a28fc6e56ea574356f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 19 Aug 2025 19:28:27 +0100
Subject: [PATCH 2/6] add: basics for `Predomain`s

---
 .../Binary/Predomain/Definitions.agda         | 42 +++++++++++
 .../Binary/Predomain/Morphism/Structures.agda | 46 ++++++++++++
 src/Relation/Binary/Predomain/Structures.agda | 74 +++++++++++++++++++
 3 files changed, 162 insertions(+)
 create mode 100644 src/Relation/Binary/Predomain/Definitions.agda
 create mode 100644 src/Relation/Binary/Predomain/Morphism/Structures.agda
 create mode 100644 src/Relation/Binary/Predomain/Structures.agda

diff --git a/src/Relation/Binary/Predomain/Definitions.agda b/src/Relation/Binary/Predomain/Definitions.agda
new file mode 100644
index 0000000000..aced218b9c
--- /dev/null
+++ b/src/Relation/Binary/Predomain/Definitions.agda
@@ -0,0 +1,42 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions for domain theory
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Relation.Binary.Predomain.Definitions
+  {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where
+
+open import Data.Product using (∃-syntax; _×_; _,_)
+open import Function using (_∘_)
+open import Level using (Level; _⊔_)
+open import Relation.Unary using (Pred)
+
+private
+  variable
+    i : Level
+    I : Set i
+
+
+------------------------------------------------------------------------
+-- Upper bound
+------------------------------------------------------------------------
+
+UpperBound : (f : I → A) → Pred A _
+UpperBound f x = ∀ i → f i ≤ x
+
+------------------------------------------------------------------------
+-- Minimal upper bound above a given element
+------------------------------------------------------------------------
+
+record MinimalUpperBoundAbove
+  {I : Set i} (f : I → A) (x y : A) : Set (a ⊔ i ⊔ ℓ) where
+  field
+    lowerBound : x ≤ y
+    upperBound : UpperBound {I = I} f y
+    minimal    : ∀ {z} → x ≤ z → UpperBound f z → y ≤ z
+    
diff --git a/src/Relation/Binary/Predomain/Morphism/Structures.agda b/src/Relation/Binary/Predomain/Morphism/Structures.agda
new file mode 100644
index 0000000000..9827e6c755
--- /dev/null
+++ b/src/Relation/Binary/Predomain/Morphism/Structures.agda
@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Order morphisms
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Relation.Binary.Predomain.Morphism.Structures
+  {a b} {A : Set a} {B : Set b}
+  where
+
+open import Data.Product.Base using (_,_)
+open import Function.Base using (_∘_)
+open import Function.Definitions using (Injective; Surjective; Bijective)
+open import Level using (Level; suc; _⊔_)
+
+open import Relation.Binary.Morphism.Definitions A B
+open import Relation.Binary.Morphism.Structures
+open import Relation.Binary.Predomain.Definitions
+open import Relation.Binary.Predomain.Structures
+
+private
+  variable
+    i ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
+    I : Set i
+    x y : A
+    f : I → A
+
+
+------------------------------------------------------------------------
+-- Scott continuous maps
+------------------------------------------------------------------------
+
+record IsContinuousHomomorphism i (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
+                                (_≲₁_ : Rel A ℓ₃) (_≲₂_ : Rel B ℓ₄)
+                                (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄ ⊔ suc i)
+                                where
+  field
+    isOrderHomomorphism : IsOrderHomomorphism _≈₁_ _≈₂_ _≲₁_ _≲₂_ ⟦_⟧
+    ⋁-homo : MinimalUpperBoundAbove _≲₁_ {i = i} {I = I} f x y →
+              MinimalUpperBoundAbove _≲₂_ (⟦_⟧ ∘ f) ⟦ x ⟧ ⟦ y ⟧
+
+
diff --git a/src/Relation/Binary/Predomain/Structures.agda b/src/Relation/Binary/Predomain/Structures.agda
new file mode 100644
index 0000000000..d4fc1fb451
--- /dev/null
+++ b/src/Relation/Binary/Predomain/Structures.agda
@@ -0,0 +1,74 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Structures for homogeneous binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via `Relation.Binary`.
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core
+
+module Relation.Binary.Predomain.Structures
+  {a ℓ} {A : Set a} -- The underlying set
+  (_≈_ : Rel A ℓ)   -- The underlying equality relation
+  where
+
+open import Data.Product.Base using (proj₁; proj₂; _,_)
+open import Function.Base using (_on_)
+open import Level using (Level; suc; _⊔_)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+open import Relation.Binary.Consequences
+  using (tri⇒dec≈; tri⇒dec<; trans∧irr⇒asym)
+open import Relation.Binary.Definitions
+open import Relation.Binary.Predomain.Definitions
+
+open import Relation.Binary.Structures _≈_
+  using (IsPreorder; IsPartialOrder)
+
+private
+  variable
+    i ℓ′ : Level
+    I : Set i
+
+
+------------------------------------------------------------------------
+-- Directed-complete Preorders
+------------------------------------------------------------------------
+
+record IsDCPreorder {i} (_≲_ : Rel A ℓ′) : Set (a ⊔ ℓ ⊔ ℓ′ ⊔ suc i) where
+  field
+    isPreorder : IsPreorder _≲_
+    _≲⋁[_]_   : ∀ {I : Set i} → A → (f : I → A) → Directed (_≲_ on f) → A
+    ≲⋁-isMub  : ∀ {I : Set i} (x : A) (f : I → A) (d : Directed (_≲_ on f)) →
+                MinimalUpperBoundAbove _≲_ f x (x ≲⋁[ f ] d)
+
+  module _ {I : Set i} {x : A} {f : I → A} {d : Directed (_≲_ on f)} where
+
+    open MinimalUpperBoundAbove (≲⋁-isMub x f d) public
+      renaming (lowerBound to ≲⋁; upperBound to ≲ᶠ⋁; minimal to ⋁-minimal)
+
+
+record IsDCPartialOrder {i} (_≤_ : Rel A ℓ′) : Set (a ⊔ ℓ ⊔ ℓ′ ⊔ suc i) where
+  field
+    isDCPreorder : IsDCPreorder {i = i} _≤_
+    antisym      : Antisymmetric _≈_ _≤_
+
+  open IsDCPreorder isDCPreorder public
+    renaming (_≲⋁[_]_ to _≤⋁[_]_; ≲⋁-isMub to ≤⋁-isMub
+             ; ≲⋁ to ≤⋁; ≲ᶠ⋁ to ≤ᶠ⋁)
+
+  isPartialOrder : IsPartialOrder _≤_
+  isPartialOrder = record { isPreorder = isPreorder ; antisym = antisym }
+
+
+
+record IsDomain {i} (_≤_ : Rel A ℓ′) : Set (a ⊔ ℓ ⊔ ℓ′ ⊔ suc i) where
+  field
+    isDCPartialOrder : IsDCPartialOrder {i = i} _≤_
+    ⊥ : A
+    ⊥-minimal : ∀ x → ⊥ ≤ x
+
+  open IsDCPartialOrder isDCPartialOrder public

From 383a92c32b0ead8701d29873ccc939caec53de3b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 19 Aug 2025 19:35:37 +0100
Subject: [PATCH 3/6] add: new modules

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 18c7183b20..4f9c8ac79c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -48,6 +48,11 @@ New modules
 
 * `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.
 
+* Domain theory basics:
+  - `Relation.Binary.Predomain.Definitions`
+  - `Relation.Binary.Predomain.Structures`
+  - `Relation.Binary.Predomain.Morphism.Structures`
+
 Additions to existing modules
 -----------------------------
 

From 790c9964d947a47e078245668808e6ea7815fdaf Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 19 Aug 2025 22:03:28 +0100
Subject: [PATCH 4/6] [ add ] `Domain`s in terms of `Predomains`

---
 src/Relation/Binary/Predomain/Structures.agda | 34 ++++++++++++++++---
 1 file changed, 30 insertions(+), 4 deletions(-)

diff --git a/src/Relation/Binary/Predomain/Structures.agda b/src/Relation/Binary/Predomain/Structures.agda
index d4fc1fb451..8042eb3ab8 100644
--- a/src/Relation/Binary/Predomain/Structures.agda
+++ b/src/Relation/Binary/Predomain/Structures.agda
@@ -15,6 +15,7 @@ module Relation.Binary.Predomain.Structures
   (_≈_ : Rel A ℓ)   -- The underlying equality relation
   where
 
+import Data.Empty.Polymorphic as Empty
 open import Data.Product.Base using (proj₁; proj₂; _,_)
 open import Function.Base using (_on_)
 open import Level using (Level; suc; _⊔_)
@@ -32,6 +33,7 @@ private
   variable
     i ℓ′ : Level
     I : Set i
+    x : A
 
 
 ------------------------------------------------------------------------
@@ -41,14 +43,14 @@ private
 record IsDCPreorder {i} (_≲_ : Rel A ℓ′) : Set (a ⊔ ℓ ⊔ ℓ′ ⊔ suc i) where
   field
     isPreorder : IsPreorder _≲_
-    _≲⋁[_]_   : ∀ {I : Set i} → A → (f : I → A) → Directed (_≲_ on f) → A
+    _≲⋁[_]_   : ∀ {I : Set i} (x : A) (f : I → A) → Directed (_≲_ on f) → A
     ≲⋁-isMub  : ∀ {I : Set i} (x : A) (f : I → A) (d : Directed (_≲_ on f)) →
                 MinimalUpperBoundAbove _≲_ f x (x ≲⋁[ f ] d)
 
   module _ {I : Set i} {x : A} {f : I → A} {d : Directed (_≲_ on f)} where
 
     open MinimalUpperBoundAbove (≲⋁-isMub x f d) public
-      renaming (lowerBound to ≲⋁; upperBound to ≲ᶠ⋁; minimal to ⋁-minimal)
+      renaming (lowerBound to ≲⋁; upperBound to ≲ᶠ⋁; minimal to ≲⋁-minimal)
 
 
 record IsDCPartialOrder {i} (_≤_ : Rel A ℓ′) : Set (a ⊔ ℓ ⊔ ℓ′ ⊔ suc i) where
@@ -58,17 +60,41 @@ record IsDCPartialOrder {i} (_≤_ : Rel A ℓ′) : Set (a ⊔ ℓ ⊔ ℓ′ 
 
   open IsDCPreorder isDCPreorder public
     renaming (_≲⋁[_]_ to _≤⋁[_]_; ≲⋁-isMub to ≤⋁-isMub
-             ; ≲⋁ to ≤⋁; ≲ᶠ⋁ to ≤ᶠ⋁)
+             ; ≲⋁ to ≤⋁; ≲ᶠ⋁ to ≤ᶠ⋁; ≲⋁-minimal to ≤⋁-minimal)
 
   isPartialOrder : IsPartialOrder _≤_
   isPartialOrder = record { isPreorder = isPreorder ; antisym = antisym }
 
+  open IsPartialOrder isPartialOrder public
+    hiding (antisym)
+
+  _≤⋁[∅] : A → A
+  x ≤⋁[∅] = _≤⋁[_]_ {I = Empty.⊥ {i}} x (λ()) λ()
+
+  x≤⋁[∅]≈x : (x ≤⋁[∅]) ≈ x
+  x≤⋁[∅]≈x = antisym (≤⋁-minimal refl λ()) ≤⋁
 
 
 record IsDomain {i} (_≤_ : Rel A ℓ′) : Set (a ⊔ ℓ ⊔ ℓ′ ⊔ suc i) where
   field
     isDCPartialOrder : IsDCPartialOrder {i = i} _≤_
     ⊥ : A
-    ⊥-minimal : ∀ x → ⊥ ≤ x
+    ⊥-minimal : ∀ {x} → ⊥ ≤ x
 
   open IsDCPartialOrder isDCPartialOrder public
+
+  ⊥-least : ∀ {x} → x ≤ ⊥ → x ≈ ⊥
+  ⊥-least x≤⊥ = antisym x≤⊥ ⊥-minimal
+
+  ⋁[∅] : A
+  ⋁[∅] = ⊥ ≤⋁[∅]
+  
+  ⋁[∅]≈⊥ : ⋁[∅] ≈ ⊥
+  ⋁[∅]≈⊥ = x≤⋁[∅]≈x
+
+  ⋁[_]_ : ∀ {I : Set i} (f : I → A) → Directed (_≤_ on f) → A
+  ⋁[_]_ = ⊥ ≤⋁[_]_
+
+  ⋁-minimal : ∀ {I : Set i} {f : I → A} {d :  Directed (_≤_ on f)} {z} →
+               UpperBound _≤_ f z → (⋁[ f ] d) ≤ z
+  ⋁-minimal = ≤⋁-minimal ⊥-minimal

From 9ed2b2ace1b9a080c31fc0245e835b9626513544 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 20 Aug 2025 07:44:37 +0100
Subject: [PATCH 5/6] [ add ] tidy up `Domain`s in terms of `Predomains`

---
 src/Relation/Binary/Definitions.agda                   | 2 +-
 src/Relation/Binary/Predomain/Definitions.agda         | 2 --
 src/Relation/Binary/Predomain/Morphism/Structures.agda | 4 ----
 src/Relation/Binary/Predomain/Structures.agda          | 5 -----
 4 files changed, 1 insertion(+), 12 deletions(-)

diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda
index 2e20790d10..ad86037346 100644
--- a/src/Relation/Binary/Definitions.agda
+++ b/src/Relation/Binary/Definitions.agda
@@ -96,7 +96,7 @@ Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)
 Dense : Rel A ℓ → Set _
 Dense _<_ = ∀ {x y} → x < y → ∃[ z ] x < z × z < y
 
--- Directedness
+-- Directedness (but: we drop the inhabitedness condition)
 
 Directed : Rel A ℓ → Set _
 Directed _≤_ = ∀ x y → ∃[ z ] x ≤ z × y ≤ z
diff --git a/src/Relation/Binary/Predomain/Definitions.agda b/src/Relation/Binary/Predomain/Definitions.agda
index aced218b9c..1eff6f49f3 100644
--- a/src/Relation/Binary/Predomain/Definitions.agda
+++ b/src/Relation/Binary/Predomain/Definitions.agda
@@ -11,8 +11,6 @@ open import Relation.Binary.Core using (Rel)
 module Relation.Binary.Predomain.Definitions
   {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where
 
-open import Data.Product using (∃-syntax; _×_; _,_)
-open import Function using (_∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred)
 
diff --git a/src/Relation/Binary/Predomain/Morphism/Structures.agda b/src/Relation/Binary/Predomain/Morphism/Structures.agda
index 9827e6c755..c1c559700d 100644
--- a/src/Relation/Binary/Predomain/Morphism/Structures.agda
+++ b/src/Relation/Binary/Predomain/Morphism/Structures.agda
@@ -12,12 +12,8 @@ module Relation.Binary.Predomain.Morphism.Structures
   {a b} {A : Set a} {B : Set b}
   where
 
-open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘_)
-open import Function.Definitions using (Injective; Surjective; Bijective)
 open import Level using (Level; suc; _⊔_)
-
-open import Relation.Binary.Morphism.Definitions A B
 open import Relation.Binary.Morphism.Structures
 open import Relation.Binary.Predomain.Definitions
 open import Relation.Binary.Predomain.Structures
diff --git a/src/Relation/Binary/Predomain/Structures.agda b/src/Relation/Binary/Predomain/Structures.agda
index 8042eb3ab8..af575b0b5c 100644
--- a/src/Relation/Binary/Predomain/Structures.agda
+++ b/src/Relation/Binary/Predomain/Structures.agda
@@ -16,13 +16,8 @@ module Relation.Binary.Predomain.Structures
   where
 
 import Data.Empty.Polymorphic as Empty
-open import Data.Product.Base using (proj₁; proj₂; _,_)
 open import Function.Base using (_on_)
 open import Level using (Level; suc; _⊔_)
-open import Relation.Nullary.Negation.Core using (¬_)
-open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Binary.Consequences
-  using (tri⇒dec≈; tri⇒dec<; trans∧irr⇒asym)
 open import Relation.Binary.Definitions
 open import Relation.Binary.Predomain.Definitions
 

From e6ab1699705d8ff297b54e31f92d5be211f92be5 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 20 Aug 2025 14:37:33 +0100
Subject: [PATCH 6/6] add: `LowerBound`

---
 src/Relation/Binary/Predomain/Definitions.agda | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/Relation/Binary/Predomain/Definitions.agda b/src/Relation/Binary/Predomain/Definitions.agda
index 1eff6f49f3..06d20fdb55 100644
--- a/src/Relation/Binary/Predomain/Definitions.agda
+++ b/src/Relation/Binary/Predomain/Definitions.agda
@@ -18,14 +18,21 @@ private
   variable
     i : Level
     I : Set i
+    z : A
 
+------------------------------------------------------------------------
+-- Lower bound
+------------------------------------------------------------------------
+
+LowerBound : (f : I → A) → Pred A _
+LowerBound f x = ∀ i → x ≤ f i
 
 ------------------------------------------------------------------------
 -- Upper bound
 ------------------------------------------------------------------------
 
 UpperBound : (f : I → A) → Pred A _
-UpperBound f x = ∀ i → f i ≤ x
+UpperBound f y = ∀ i → f i ≤ y
 
 ------------------------------------------------------------------------
 -- Minimal upper bound above a given element
@@ -36,5 +43,5 @@ record MinimalUpperBoundAbove
   field
     lowerBound : x ≤ y
     upperBound : UpperBound {I = I} f y
-    minimal    : ∀ {z} → x ≤ z → UpperBound f z → y ≤ z
+    minimal    : x ≤ z → UpperBound f z → y ≤ z