From 4486fd0108d05cceb9636d4e9a72d72ddfa67cf6 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Mon, 26 May 2025 19:07:22 -0400
Subject: [PATCH 01/11] Definitons of domain theory

---
 CHANGELOG.md                                |  4 ++
 src/Relation/Binary/Domain.agda             | 16 +++++
 src/Relation/Binary/Domain/Bundles.agda     | 53 +++++++++++++++++
 src/Relation/Binary/Domain/Definitions.agda | 28 +++++++++
 src/Relation/Binary/Domain/Structures.agda  | 66 +++++++++++++++++++++
 5 files changed, 167 insertions(+)
 create mode 100644 src/Relation/Binary/Domain.agda
 create mode 100644 src/Relation/Binary/Domain/Bundles.agda
 create mode 100644 src/Relation/Binary/Domain/Definitions.agda
 create mode 100644 src/Relation/Binary/Domain/Structures.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2959d3d6ce..4722c81ba2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -123,6 +123,10 @@ New modules
 
 * `Data.Sign.Show` to show a sign
 
+* Added a new domain theory section to the library under `Relation.Binary.Domain.*`:
+  - Introduced new modules and bundles for domain theory, including `DCPO`, `Lub`, and `ScottContinuous`.
+  - All files for domain theory are now available in `src/Relation/Binary/Domain/`.
+
 Additions to existing modules
 -----------------------------
 
diff --git a/src/Relation/Binary/Domain.agda b/src/Relation/Binary/Domain.agda
new file mode 100644
index 0000000000..812e74a601
--- /dev/null
+++ b/src/Relation/Binary/Domain.agda
@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Order-theoretic Domains
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain where
+
+------------------------------------------------------------------------
+-- Re-export various components of the Domain hierarchy
+
+open import Relation.Binary.Domain.Definitions public
+open import Relation.Binary.Domain.Structures public
+open import Relation.Binary.Domain.Bundles public
diff --git a/src/Relation/Binary/Domain/Bundles.agda b/src/Relation/Binary/Domain/Bundles.agda
new file mode 100644
index 0000000000..7b84781ee6
--- /dev/null
+++ b/src/Relation/Binary/Domain/Bundles.agda
@@ -0,0 +1,53 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Bundles for domain theory
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain.Bundles where
+
+open import Level using (Level; _⊔_; suc)
+open import Relation.Binary.Bundles using (Poset)
+open import Relation.Binary.Domain.Structures
+open import Relation.Binary.Domain.Definitions
+
+private
+  variable
+    o ℓ e o' ℓ' e' ℓ₂ : Level
+    Ix A B : Set o
+
+------------------------------------------------------------------------
+-- DCPOs
+------------------------------------------------------------------------
+
+record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  field
+    poset   : Poset c ℓ₁ ℓ₂
+    DcpoStr : IsDCPO poset
+
+  open Poset poset public
+  open IsDCPO DcpoStr public
+
+------------------------------------------------------------------------
+-- Scott-continuous functions
+------------------------------------------------------------------------
+
+record ScottContinuous {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} :
+  Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  field
+    f             : Poset.Carrier P → Poset.Carrier Q
+    Scottfunction : IsScottContinuous {P = P} {Q = Q} f
+
+------------------------------------------------------------------------
+-- Lubs
+------------------------------------------------------------------------
+
+record Lub {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Ix : Set c} (s : Ix → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+  private
+    module P = Poset P
+  field
+    lub           : P.Carrier
+    is-upperbound : ∀ i → P._≤_ (s i) lub
+    is-least      : ∀ y → (∀ i → P._≤_ (s i) y) → P._≤_ lub y
diff --git a/src/Relation/Binary/Domain/Definitions.agda b/src/Relation/Binary/Domain/Definitions.agda
new file mode 100644
index 0000000000..828553b6af
--- /dev/null
+++ b/src/Relation/Binary/Domain/Definitions.agda
@@ -0,0 +1,28 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions for domain theory
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain.Definitions where
+
+open import Data.Product using (∃-syntax; _×_; _,_)
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Bundles using (Poset)
+open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
+
+private
+  variable
+    c o ℓ e o' ℓ' e' ℓ₁ ℓ₂ : Level
+    Ix A B : Set o
+    P : Poset c ℓ e
+
+------------------------------------------------------------------------
+-- Directed families
+------------------------------------------------------------------------
+
+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))
+
diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda
new file mode 100644
index 0000000000..5d6d397181
--- /dev/null
+++ b/src/Relation/Binary/Domain/Structures.agda
@@ -0,0 +1,66 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Structures for domain theory
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain.Structures where
+
+open import Data.Product using (_×_; _,_)
+open import Data.Nat.Properties using (≤-trans)
+open import Function using (_∘_)
+open import Level using (Level; _⊔_; suc)
+open import Relation.Binary.Bundles using (Poset)
+open import Relation.Binary.Domain.Definitions
+open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
+
+private variable
+  o ℓ e o' ℓ' e' ℓ₂ : Level
+  Ix A B : Set o
+
+module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
+  open Poset P
+
+  record IsDirectedFamily {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+    no-eta-equality
+    field
+      elt : Ix
+      SemiDirected : IsSemidirectedFamily P s
+
+  record IsLub {Ix : Set c} (s : Ix → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      is-upperbound : ∀ i → s i ≤ lub
+      is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y
+
+  record IsDCPO : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+    field
+      ⋁ : ∀ {Ix : Set c}
+        → (s : Ix → Carrier)
+        → IsDirectedFamily s
+        → Carrier
+      ⋁-isLub : ∀ {Ix : Set c}
+        → (s : Ix → Carrier)
+        → (dir : IsDirectedFamily s)
+        → IsLub s (⋁ s dir)
+
+    module _ {Ix : Set c} {s : Ix → Carrier} {dir : IsDirectedFamily s} where
+      open IsLub (⋁-isLub s dir)
+        renaming (is-upperbound to ⋁-≤; is-least to ⋁-least)
+        public
+
+module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where
+
+  private
+    module P = Poset P
+    module Q = Poset Q
+
+  record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+    field
+      PreserveLub : ∀ {Ix : Set c} {s : Ix → P.Carrier}
+        → (dir : IsDirectedFamily P s)
+        → (lub : P.Carrier)
+        → IsLub P s lub
+        → IsLub Q (f ∘ s) (f lub)
+      PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y

From 34be6b0cba4904ef0bca2d06bd678c08c2a1bf98 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 3 Jun 2025 14:14:03 -0400
Subject: [PATCH 02/11]  1st review

---
 CHANGELOG.md                                |   2 +-
 src/Padrightpropertiesdraft.agda            | 109 ++++++++++++++++++++
 src/Relation/Binary/Domain/Bundles.agda     |  30 +++---
 src/Relation/Binary/Domain/Definitions.agda |  24 +++--
 src/Relation/Binary/Domain/Structures.agda  |  60 ++++++-----
 5 files changed, 176 insertions(+), 49 deletions(-)
 create mode 100644 src/Padrightpropertiesdraft.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4722c81ba2..055fbf6250 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -124,7 +124,7 @@ New modules
 * `Data.Sign.Show` to show a sign
 
 * Added a new domain theory section to the library under `Relation.Binary.Domain.*`:
-  - Introduced new modules and bundles for domain theory, including `DCPO`, `Lub`, and `ScottContinuous`.
+  - Introduced new modules and bundles for domain theory, including `DirectedCompletePartialOrder`, `Lub`, and `ScottContinuous`.
   - All files for domain theory are now available in `src/Relation/Binary/Domain/`.
 
 Additions to existing modules
diff --git a/src/Padrightpropertiesdraft.agda b/src/Padrightpropertiesdraft.agda
new file mode 100644
index 0000000000..b7649b48d8
--- /dev/null
+++ b/src/Padrightpropertiesdraft.agda
@@ -0,0 +1,109 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of padRight for Vec
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Padrightpropertiesdraft where
+
+open import Data.Fin.Base using (Fin; zero; suc; inject≤)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _∸_)
+open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m+n; m+n∸m≡n)
+open import Data.Vec.Base
+open import Data.Vec.Properties using (map-replicate; zipWith-replicate; padRight-trans)
+open import Function.Base using (_∘_; _$_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; cong; sym; trans; subst)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
+
+private
+  variable
+    a b c : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    m n p : ℕ
+
+
+------------------------------------------------------------------------
+-- Interaction with map
+
+padRight-map : ∀ (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) →
+               map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs)
+padRight-map f z≤n a [] = map-replicate f a _
+padRight-map f (s≤s m≤n) a (x ∷ xs) = cong (f x ∷_) (padRight-map f m≤n a xs)
+
+------------------------------------------------------------------------
+-- Interaction with lookup
+
+padRight-lookup : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) →
+                  lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
+padRight-lookup (s≤s m≤n) a (x ∷ xs) zero = refl
+padRight-lookup (s≤s m≤n) a (x ∷ xs) (suc i) = padRight-lookup m≤n a xs i
+
+------------------------------------------------------------------------
+-- Interaction with zipWith
+
+-- When both vectors have the same original length
+padRight-zipWith : ∀ (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B)
+                   (xs : Vec A m) (ys : Vec B m) →
+                   zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡
+                   padRight m≤n (f a b) (zipWith f xs ys)
+padRight-zipWith f z≤n a b [] [] = zipWith-replicate f a b
+padRight-zipWith f (s≤s m≤n) a b (x ∷ xs) (y ∷ ys) =
+  cong (f x y ∷_) (padRight-zipWith f m≤n a b xs ys)
+
+-- When vectors have different original lengths
+padRight-zipWith₁ : ∀ {p} (f : A → B → C) (m≤n : m ≤ n) (p≤m : p ≤ m)
+                    (a : A) (b : B) (xs : Vec A m) (ys : Vec B p) →
+                    zipWith f (padRight m≤n a xs) (padRight (≤-trans p≤m m≤n) b ys) ≡
+                    padRight m≤n (f a b) (zipWith f xs (padRight p≤m b ys))
+padRight-zipWith₁ {p} f m≤n p≤m a b xs ys =
+  trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys))
+        (padRight-zipWith f m≤n a b xs (padRight p≤m b ys))
+
+------------------------------------------------------------------------
+-- Interaction with take and drop
+
+padRight-take : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
+                take m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ xs
+padRight-take {m = zero} z≤n a [] refl = refl
+padRight-take {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl =
+  cong (x ∷_) (padRight-take {p = p} m≤n a xs refl)
+
+-- Helper lemma: commuting subst with drop
+subst-drop : ∀ {m n p : ℕ} {A : Set} (eq : n ≡ m + p) (xs : Vec A n) →
+             drop m (subst (Vec A) eq xs) ≡ subst (Vec A) (cong (_∸ m) eq) (drop m xs)
+subst-drop refl xs = refl
+
+-- Helper lemma: dropping from padded vector gives replicate  
+drop-padRight : ∀ {m n p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) →
+                n ≡ m + p → drop m (padRight m≤n a xs) ≡ replicate p a
+drop-padRight {m = zero} z≤n a [] refl = refl
+drop-padRight {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl =
+  drop-padRight {p = p} m≤n a xs refl
+
+padRight-drop : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
+                drop m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ replicate p a
+padRight-drop {p = p} m≤n a xs n≡m+p =
+  trans (subst-drop n≡m+p (padRight m≤n a xs))
+        (cong (subst (Vec A) (cong (_∸ _) n≡m+p)) (drop-padRight m≤n a xs n≡m+p))
+
+------------------------------------------------------------------------
+-- Interaction with updateAt
+
+padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) →
+                    updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
+                    padRight m≤n x (updateAt xs i f)
+padRight-updateAt (s≤s m≤n) (y ∷ xs) f zero x = refl
+padRight-updateAt (s≤s m≤n) (y ∷ xs) f (suc i) x =
+  cong (y ∷_) (padRight-updateAt m≤n xs f i x)
+
+
+
+
+
diff --git a/src/Relation/Binary/Domain/Bundles.agda b/src/Relation/Binary/Domain/Bundles.agda
index 7b84781ee6..6c103182d3 100644
--- a/src/Relation/Binary/Domain/Bundles.agda
+++ b/src/Relation/Binary/Domain/Bundles.agda
@@ -19,16 +19,22 @@ private
     Ix A B : Set o
 
 ------------------------------------------------------------------------
--- DCPOs
+-- Directed Complete Partial Orders
 ------------------------------------------------------------------------
 
-record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+record DirectedFamily {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {B : Set c} (f : B → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
   field
-    poset   : Poset c ℓ₁ ℓ₂
-    DcpoStr : IsDCPO poset
+    isDirectedFamily : IsDirectedFamily P f
+  
+  open IsDirectedFamily isDirectedFamily public
+
+record DirectedCompletePartialOrder (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  field
+    poset                             : Poset c ℓ₁ ℓ₂
+    isDirectedCompletePartialOrder    : IsDirectedCompletePartialOrder poset
 
   open Poset poset public
-  open IsDCPO DcpoStr public
+  open IsDirectedCompletePartialOrder isDirectedCompletePartialOrder public
 
 ------------------------------------------------------------------------
 -- Scott-continuous functions
@@ -37,17 +43,15 @@ record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) wher
 record ScottContinuous {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} :
   Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   field
-    f             : Poset.Carrier P → Poset.Carrier Q
-    Scottfunction : IsScottContinuous {P = P} {Q = Q} f
+    f                 : Poset.Carrier P → Poset.Carrier Q
+    isScottContinuous : IsScottContinuous {P = P} {Q = Q} f
 
 ------------------------------------------------------------------------
 -- Lubs
 ------------------------------------------------------------------------
 
-record Lub {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Ix : Set c} (s : Ix → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
-  private
-    module P = Poset P
+record Lub {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {B : Set c} (f : B → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+  open Poset P
   field
-    lub           : P.Carrier
-    is-upperbound : ∀ i → P._≤_ (s i) lub
-    is-least      : ∀ y → (∀ i → P._≤_ (s i) y) → P._≤_ lub y
+    lub   : Carrier
+    isLub : IsLub P f lub
diff --git a/src/Relation/Binary/Domain/Definitions.agda b/src/Relation/Binary/Domain/Definitions.agda
index 828553b6af..a3322e87e0 100644
--- a/src/Relation/Binary/Domain/Definitions.agda
+++ b/src/Relation/Binary/Domain/Definitions.agda
@@ -4,25 +4,35 @@
 -- Definitions for domain theory
 ------------------------------------------------------------------------
 
+
+
+
 {-# OPTIONS --cubical-compatible --safe #-}
 
 module Relation.Binary.Domain.Definitions where
 
 open import Data.Product using (∃-syntax; _×_; _,_)
 open import Level using (Level; _⊔_)
-open import Relation.Binary.Bundles using (Poset)
-open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
+open import Relation.Binary.Core using (Rel)
 
 private
   variable
-    c o ℓ e o' ℓ' e' ℓ₁ ℓ₂ : Level
-    Ix A B : Set o
-    P : Poset c ℓ e
+    a b ℓ : Level
+    A B : Set a
 
 ------------------------------------------------------------------------
 -- Directed families
 ------------------------------------------------------------------------
 
-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))
+-- 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 _
+semidirected _≤_ B f = ∀ i j → ∃[ k ] (f i ≤ f k × f j ≤ f k)
+
+------------------------------------------------------------------------
+-- Least upper bounds
+------------------------------------------------------------------------
 
+leastupperbound  : {A : Set a} → Rel A ℓ → (B : Set b) → (B → A) → A → Set _
+leastupperbound _≤_ B f lub = (∀ i → f i ≤ lub) × (∀ y → (∀ i → f i ≤ y) → lub ≤ y)
diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda
index 5d6d397181..dfbe85f3c6 100644
--- a/src/Relation/Binary/Domain/Structures.agda
+++ b/src/Relation/Binary/Domain/Structures.agda
@@ -8,46 +8,50 @@
 
 module Relation.Binary.Domain.Structures where
 
-open import Data.Product using (_×_; _,_)
-open import Data.Nat.Properties using (≤-trans)
+open import Data.Product using (_×_; _,_; proj₁; proj₂)
 open import Function using (_∘_)
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Bundles using (Poset)
 open import Relation.Binary.Domain.Definitions
-open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
 
 private variable
-  o ℓ e o' ℓ' e' ℓ₂ : Level
-  Ix A B : Set o
+  a b c ℓ ℓ₁ ℓ₂ : Level
+  A B : Set a
+
 
 module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
   open Poset P
 
-  record IsDirectedFamily {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
-    no-eta-equality
+  record IsLub {B : Set c} (f : B → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
     field
-      elt : Ix
-      SemiDirected : IsSemidirectedFamily P s
+      isLeastUpperBound : leastupperbound _≤_ B f lub
+      
+    isUpperBound : ∀ i → f i ≤ lub
+    isUpperBound = proj₁ isLeastUpperBound
+    
+    isLeast : ∀ y → (∀ i → f i ≤ y) → lub ≤ y  
+    isLeast = proj₂ isLeastUpperBound
 
-  record IsLub {Ix : Set c} (s : Ix → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+  record IsDirectedFamily {B : Set c} (f : B → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+    no-eta-equality
     field
-      is-upperbound : ∀ i → s i ≤ lub
-      is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y
+      elt : B
+      isSemidirected : semidirected _≤_ B f
 
-  record IsDCPO : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  record IsDirectedCompletePartialOrder : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     field
-      ⋁ : ∀ {Ix : Set c}
-        → (s : Ix → Carrier)
-        → IsDirectedFamily s
+      ⋁ : ∀ {B : Set c}
+        → (f : B → Carrier)
+        → IsDirectedFamily f
         → Carrier
-      ⋁-isLub : ∀ {Ix : Set c}
-        → (s : Ix → Carrier)
-        → (dir : IsDirectedFamily s)
-        → IsLub s (⋁ s dir)
+      ⋁-isLub : ∀ {B : Set c}
+        → (f : B → Carrier)
+        → (dir : IsDirectedFamily f)
+        → IsLub f (⋁ f dir)
 
-    module _ {Ix : Set c} {s : Ix → Carrier} {dir : IsDirectedFamily s} where
-      open IsLub (⋁-isLub s dir)
-        renaming (is-upperbound to ⋁-≤; is-least to ⋁-least)
+    module _ {B : Set c} {f : B → Carrier} {dir : IsDirectedFamily f} where
+      open IsLub (⋁-isLub f dir)
+        renaming (isUpperBound to ⋁-≤; isLeast to ⋁-least)
         public
 
 module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where
@@ -58,9 +62,9 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ
 
   record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     field
-      PreserveLub : ∀ {Ix : Set c} {s : Ix → P.Carrier}
-        → (dir : IsDirectedFamily P s)
+      PreserveLub : ∀ {B : Set c} {g : B → P.Carrier}
+        → (dir : IsDirectedFamily P g)
         → (lub : P.Carrier)
-        → IsLub P s lub
-        → IsLub Q (f ∘ s) (f lub)
-      PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y
+        → IsLub P g lub
+        → IsLub Q (f ∘ g) (f lub)
+      PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y
\ No newline at end of file

From 502e288a5b39a7c3e7707718a0f3b33804b33ea1 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 3 Jun 2025 14:17:30 -0400
Subject: [PATCH 03/11] whitespaces

---
 src/Padrightpropertiesdraft.agda           | 6 +-----
 src/Relation/Binary/Domain/Bundles.agda    | 2 +-
 src/Relation/Binary/Domain/Structures.agda | 8 ++++----
 3 files changed, 6 insertions(+), 10 deletions(-)

diff --git a/src/Padrightpropertiesdraft.agda b/src/Padrightpropertiesdraft.agda
index b7649b48d8..8fbb9e9f36 100644
--- a/src/Padrightpropertiesdraft.agda
+++ b/src/Padrightpropertiesdraft.agda
@@ -80,7 +80,7 @@ subst-drop : ∀ {m n p : ℕ} {A : Set} (eq : n ≡ m + p) (xs : Vec A n) →
              drop m (subst (Vec A) eq xs) ≡ subst (Vec A) (cong (_∸ m) eq) (drop m xs)
 subst-drop refl xs = refl
 
--- Helper lemma: dropping from padded vector gives replicate  
+-- Helper lemma: dropping from padded vector gives replicate
 drop-padRight : ∀ {m n p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) →
                 n ≡ m + p → drop m (padRight m≤n a xs) ≡ replicate p a
 drop-padRight {m = zero} z≤n a [] refl = refl
@@ -103,7 +103,3 @@ padRight-updateAt (s≤s m≤n) (y ∷ xs) f zero x = refl
 padRight-updateAt (s≤s m≤n) (y ∷ xs) f (suc i) x =
   cong (y ∷_) (padRight-updateAt m≤n xs f i x)
 
-
-
-
-
diff --git a/src/Relation/Binary/Domain/Bundles.agda b/src/Relation/Binary/Domain/Bundles.agda
index 6c103182d3..0d255b11f4 100644
--- a/src/Relation/Binary/Domain/Bundles.agda
+++ b/src/Relation/Binary/Domain/Bundles.agda
@@ -25,7 +25,7 @@ private
 record DirectedFamily {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {B : Set c} (f : B → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
   field
     isDirectedFamily : IsDirectedFamily P f
-  
+
   open IsDirectedFamily isDirectedFamily public
 
 record DirectedCompletePartialOrder (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda
index dfbe85f3c6..e6f73de0a6 100644
--- a/src/Relation/Binary/Domain/Structures.agda
+++ b/src/Relation/Binary/Domain/Structures.agda
@@ -25,11 +25,11 @@ module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
   record IsLub {B : Set c} (f : B → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isLeastUpperBound : leastupperbound _≤_ B f lub
-      
+
     isUpperBound : ∀ i → f i ≤ lub
     isUpperBound = proj₁ isLeastUpperBound
-    
-    isLeast : ∀ y → (∀ i → f i ≤ y) → lub ≤ y  
+
+    isLeast : ∀ y → (∀ i → f i ≤ y) → lub ≤ y
     isLeast = proj₂ isLeastUpperBound
 
   record IsDirectedFamily {B : Set c} (f : B → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -67,4 +67,4 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ
         → (lub : P.Carrier)
         → IsLub P g lub
         → IsLub Q (f ∘ g) (f lub)
-      PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y
\ No newline at end of file
+      PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y

From 63810b78d7f13bbd35fd4a5ed5c9c6b281314bba Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 3 Jun 2025 15:27:34 -0400
Subject: [PATCH 04/11] @ review

---
 src/Relation/Binary/Domain/Bundles.agda    | 14 +++++++++----
 src/Relation/Binary/Domain/Structures.agda | 23 +++++++++++++++-------
 2 files changed, 26 insertions(+), 11 deletions(-)

diff --git a/src/Relation/Binary/Domain/Bundles.agda b/src/Relation/Binary/Domain/Bundles.agda
index 0d255b11f4..d4557b000e 100644
--- a/src/Relation/Binary/Domain/Bundles.agda
+++ b/src/Relation/Binary/Domain/Bundles.agda
@@ -40,17 +40,23 @@ record DirectedCompletePartialOrder (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔
 -- Scott-continuous functions
 ------------------------------------------------------------------------
 
-record ScottContinuous {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} :
-  Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+record ScottContinuous
+  {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level}
+  (P : Poset c₁ ℓ₁₁ ℓ₁₂)
+  (Q : Poset c₂ ℓ₂₁ ℓ₂₂)
+  : Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where
   field
     f                 : Poset.Carrier P → Poset.Carrier Q
-    isScottContinuous : IsScottContinuous {P = P} {Q = Q} f
+    isScottContinuous : IsScottContinuous P Q f
+
+  open IsScottContinuous isScottContinuous public
 
 ------------------------------------------------------------------------
 -- Lubs
 ------------------------------------------------------------------------
 
-record Lub {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {B : Set c} (f : B → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+record Lub {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {B : Set c}
+           (f : B → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
   open Poset P
   field
     lub   : Carrier
diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda
index e6f73de0a6..36717e8189 100644
--- a/src/Relation/Binary/Domain/Structures.agda
+++ b/src/Relation/Binary/Domain/Structures.agda
@@ -22,7 +22,8 @@ private variable
 module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
   open Poset P
 
-  record IsLub {B : Set c} (f : B → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+  record IsLub {b : Level} {B : Set b} (f : B → Carrier)
+               (lub : Carrier) : Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isLeastUpperBound : leastupperbound _≤_ B f lub
 
@@ -32,10 +33,11 @@ module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
     isLeast : ∀ y → (∀ i → f i ≤ y) → lub ≤ y
     isLeast = proj₂ isLeastUpperBound
 
-  record IsDirectedFamily {B : Set c} (f : B → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+  record IsDirectedFamily {b : Level} {B : Set b} (f : B → Carrier)
+    : Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where
     no-eta-equality
     field
-      elt : B
+      elt           : B
       isSemidirected : semidirected _≤_ B f
 
   record IsDirectedCompletePartialOrder : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -54,17 +56,24 @@ module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
         renaming (isUpperBound to ⋁-≤; isLeast to ⋁-least)
         public
 
-module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where
+------------------------------------------------------------------------
+-- Scott‐continuous maps between two (possibly different‐universe) posets
+------------------------------------------------------------------------
+
+module _ {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level}
+         (P : Poset c₁ ℓ₁₁ ℓ₁₂)
+         (Q : Poset c₂ ℓ₂₁ ℓ₂₂) where
 
   private
     module P = Poset P
     module Q = Poset Q
 
-  record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  record IsScottContinuous (f : P.Carrier → Q.Carrier)
+    : Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where
     field
-      PreserveLub : ∀ {B : Set c} {g : B → P.Carrier}
+      preserveLub : ∀ {B : Set c₁} {g : B → P.Carrier}
         → (dir : IsDirectedFamily P g)
         → (lub : P.Carrier)
         → IsLub P g lub
         → IsLub Q (f ∘ g) (f lub)
-      PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y
+      preserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y

From 87d5f16ecf2276e1c7c68a02d66003b1871f4725 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Thu, 5 Jun 2025 16:15:02 -0400
Subject: [PATCH 05/11] remove the file Padrightdraft

---
 src/Padrightpropertiesdraft.agda | 105 -------------------------------
 1 file changed, 105 deletions(-)
 delete mode 100644 src/Padrightpropertiesdraft.agda

diff --git a/src/Padrightpropertiesdraft.agda b/src/Padrightpropertiesdraft.agda
deleted file mode 100644
index 8fbb9e9f36..0000000000
--- a/src/Padrightpropertiesdraft.agda
+++ /dev/null
@@ -1,105 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Properties of padRight for Vec
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-module Padrightpropertiesdraft where
-
-open import Data.Fin.Base using (Fin; zero; suc; inject≤)
-open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _∸_)
-open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m+n; m+n∸m≡n)
-open import Data.Vec.Base
-open import Data.Vec.Properties using (map-replicate; zipWith-replicate; padRight-trans)
-open import Function.Base using (_∘_; _$_)
-open import Level using (Level)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; cong; sym; trans; subst)
-open import Relation.Binary.PropositionalEquality.Properties
-  using (module ≡-Reasoning)
-
-private
-  variable
-    a b c : Level
-    A : Set a
-    B : Set b
-    C : Set c
-    m n p : ℕ
-
-
-------------------------------------------------------------------------
--- Interaction with map
-
-padRight-map : ∀ (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) →
-               map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs)
-padRight-map f z≤n a [] = map-replicate f a _
-padRight-map f (s≤s m≤n) a (x ∷ xs) = cong (f x ∷_) (padRight-map f m≤n a xs)
-
-------------------------------------------------------------------------
--- Interaction with lookup
-
-padRight-lookup : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) →
-                  lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
-padRight-lookup (s≤s m≤n) a (x ∷ xs) zero = refl
-padRight-lookup (s≤s m≤n) a (x ∷ xs) (suc i) = padRight-lookup m≤n a xs i
-
-------------------------------------------------------------------------
--- Interaction with zipWith
-
--- When both vectors have the same original length
-padRight-zipWith : ∀ (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B)
-                   (xs : Vec A m) (ys : Vec B m) →
-                   zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡
-                   padRight m≤n (f a b) (zipWith f xs ys)
-padRight-zipWith f z≤n a b [] [] = zipWith-replicate f a b
-padRight-zipWith f (s≤s m≤n) a b (x ∷ xs) (y ∷ ys) =
-  cong (f x y ∷_) (padRight-zipWith f m≤n a b xs ys)
-
--- When vectors have different original lengths
-padRight-zipWith₁ : ∀ {p} (f : A → B → C) (m≤n : m ≤ n) (p≤m : p ≤ m)
-                    (a : A) (b : B) (xs : Vec A m) (ys : Vec B p) →
-                    zipWith f (padRight m≤n a xs) (padRight (≤-trans p≤m m≤n) b ys) ≡
-                    padRight m≤n (f a b) (zipWith f xs (padRight p≤m b ys))
-padRight-zipWith₁ {p} f m≤n p≤m a b xs ys =
-  trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys))
-        (padRight-zipWith f m≤n a b xs (padRight p≤m b ys))
-
-------------------------------------------------------------------------
--- Interaction with take and drop
-
-padRight-take : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
-                take m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ xs
-padRight-take {m = zero} z≤n a [] refl = refl
-padRight-take {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl =
-  cong (x ∷_) (padRight-take {p = p} m≤n a xs refl)
-
--- Helper lemma: commuting subst with drop
-subst-drop : ∀ {m n p : ℕ} {A : Set} (eq : n ≡ m + p) (xs : Vec A n) →
-             drop m (subst (Vec A) eq xs) ≡ subst (Vec A) (cong (_∸ m) eq) (drop m xs)
-subst-drop refl xs = refl
-
--- Helper lemma: dropping from padded vector gives replicate
-drop-padRight : ∀ {m n p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) →
-                n ≡ m + p → drop m (padRight m≤n a xs) ≡ replicate p a
-drop-padRight {m = zero} z≤n a [] refl = refl
-drop-padRight {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl =
-  drop-padRight {p = p} m≤n a xs refl
-
-padRight-drop : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) →
-                drop m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ replicate p a
-padRight-drop {p = p} m≤n a xs n≡m+p =
-  trans (subst-drop n≡m+p (padRight m≤n a xs))
-        (cong (subst (Vec A) (cong (_∸ _) n≡m+p)) (drop-padRight m≤n a xs n≡m+p))
-
-------------------------------------------------------------------------
--- Interaction with updateAt
-
-padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) →
-                    updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
-                    padRight m≤n x (updateAt xs i f)
-padRight-updateAt (s≤s m≤n) (y ∷ xs) f zero x = refl
-padRight-updateAt (s≤s m≤n) (y ∷ xs) f (suc i) x =
-  cong (y ∷_) (padRight-updateAt m≤n xs f i x)
-

From 51954b6ed88ad1cce5e0588ae667b9e5acaff172 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Mon, 16 Jun 2025 14:31:27 -0400
Subject: [PATCH 06/11] quick fix

---
 src/Relation/Binary/Domain/Structures.agda | 18 +++++++++---------
 src/TestWord8Performance.agda              |  0
 2 files changed, 9 insertions(+), 9 deletions(-)
 create mode 100644 src/TestWord8Performance.agda

diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda
index 36717e8189..ee425593dc 100644
--- a/src/Relation/Binary/Domain/Structures.agda
+++ b/src/Relation/Binary/Domain/Structures.agda
@@ -33,8 +33,8 @@ module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
     isLeast : ∀ y → (∀ i → f i ≤ y) → lub ≤ y
     isLeast = proj₂ isLeastUpperBound
 
-  record IsDirectedFamily {b : Level} {B : Set b} (f : B → Carrier)
-    : Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where
+  record IsDirectedFamily {b : Level} {B : Set b} (f : B → Carrier) :
+                          Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where
     no-eta-equality
     field
       elt           : B
@@ -68,12 +68,12 @@ module _ {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level}
     module P = Poset P
     module Q = Poset Q
 
-  record IsScottContinuous (f : P.Carrier → Q.Carrier)
-    : Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where
+  record IsScottContinuous (f : P.Carrier → Q.Carrier) :
+                           Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where
     field
-      preserveLub : ∀ {B : Set c₁} {g : B → P.Carrier}
-        → (dir : IsDirectedFamily P g)
-        → (lub : P.Carrier)
-        → IsLub P g lub
-        → IsLub Q (f ∘ g) (f lub)
+      preserveLub : ∀ {B : Set c₁} {g : B → P.Carrier} →
+                    (dir : IsDirectedFamily P g) →
+                    (lub : P.Carrier) →
+                    IsLub P g lub →
+                    IsLub Q (f ∘ g) (f lub)
       preserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y
diff --git a/src/TestWord8Performance.agda b/src/TestWord8Performance.agda
new file mode 100644
index 0000000000..e69de29bb2

From 85192d0dd0ffc7e42a952bc87448ee0bf1bf8f8d Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Tue, 24 Jun 2025 14:11:43 -0400
Subject: [PATCH 07/11] add using to importation

---
 src/Relation/Binary/Domain/Bundles.agda    |  6 +++---
 src/Relation/Binary/Domain/Structures.agda | 15 ++++++++-------
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/Relation/Binary/Domain/Bundles.agda b/src/Relation/Binary/Domain/Bundles.agda
index d4557b000e..6f5c032bf5 100644
--- a/src/Relation/Binary/Domain/Bundles.agda
+++ b/src/Relation/Binary/Domain/Bundles.agda
@@ -11,7 +11,8 @@ module Relation.Binary.Domain.Bundles where
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Bundles using (Poset)
 open import Relation.Binary.Domain.Structures
-open import Relation.Binary.Domain.Definitions
+  using (IsDirectedFamily; IsDirectedCompletePartialOrder; IsScottContinuous
+        ; IsLub)
 
 private
   variable
@@ -43,8 +44,7 @@ record DirectedCompletePartialOrder (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔
 record ScottContinuous
   {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level}
   (P : Poset c₁ ℓ₁₁ ℓ₁₂)
-  (Q : Poset c₂ ℓ₂₁ ℓ₂₂)
-  : Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where
+  (Q : Poset c₂ ℓ₂₁ ℓ₂₂) : Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where
   field
     f                 : Poset.Carrier P → Poset.Carrier Q
     isScottContinuous : IsScottContinuous P Q f
diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda
index ee425593dc..0c1c56ac90 100644
--- a/src/Relation/Binary/Domain/Structures.agda
+++ b/src/Relation/Binary/Domain/Structures.agda
@@ -13,6 +13,7 @@ open import Function using (_∘_)
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Bundles using (Poset)
 open import Relation.Binary.Domain.Definitions
+  using (semidirected; leastupperbound)
 
 private variable
   a b c ℓ ℓ₁ ℓ₂ : Level
@@ -37,15 +38,15 @@ module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
                           Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where
     no-eta-equality
     field
-      elt           : B
+      elt            : B
       isSemidirected : semidirected _≤_ B f
 
   record IsDirectedCompletePartialOrder : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     field
-      ⋁ : ∀ {B : Set c}
-        → (f : B → Carrier)
-        → IsDirectedFamily f
-        → Carrier
+      ⋁ : ∀ {B : Set c} →
+        (f : B → Carrier) →
+        IsDirectedFamily f →
+        Carrier
       ⋁-isLub : ∀ {B : Set c}
         → (f : B → Carrier)
         → (dir : IsDirectedFamily f)
@@ -68,8 +69,8 @@ module _ {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level}
     module P = Poset P
     module Q = Poset Q
 
-  record IsScottContinuous (f : P.Carrier → Q.Carrier) :
-                           Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where
+  record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂))
+    where
     field
       preserveLub : ∀ {B : Set c₁} {g : B → P.Carrier} →
                     (dir : IsDirectedFamily P g) →

From ceb39d64c08099f99b0430973e9402227e50df6a Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Wed, 25 Jun 2025 14:55:25 -0400
Subject: [PATCH 08/11] add perserveLub in defintion

---
 src/Relation/Binary/Domain/Definitions.agda | 19 ++++++------
 src/Relation/Binary/Domain/Structures.agda  | 32 +++++++++------------
 2 files changed, 25 insertions(+), 26 deletions(-)

diff --git a/src/Relation/Binary/Domain/Definitions.agda b/src/Relation/Binary/Domain/Definitions.agda
index a3322e87e0..4af4b0dde7 100644
--- a/src/Relation/Binary/Domain/Definitions.agda
+++ b/src/Relation/Binary/Domain/Definitions.agda
@@ -12,21 +12,21 @@
 module Relation.Binary.Domain.Definitions where
 
 open import Data.Product using (∃-syntax; _×_; _,_)
-open import Level using (Level; _⊔_)
+open import Function using (_∘_)
+open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Core using (Rel)
 
 private
   variable
-    a b ℓ : Level
-    A B : Set a
+    a b i ℓ ℓ₁ ℓ₂ : Level
+    A : Set a
+    B : Set b
+    I : Set ℓ
 
 ------------------------------------------------------------------------
 -- Directed families
 ------------------------------------------------------------------------
 
--- 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 _
 semidirected _≤_ B f = ∀ i j → ∃[ k ] (f i ≤ f k × f j ≤ f k)
 
@@ -34,5 +34,8 @@ semidirected _≤_ B f = ∀ i j → ∃[ k ] (f i ≤ f k × f j ≤ f k)
 -- Least upper bounds
 ------------------------------------------------------------------------
 
-leastupperbound  : {A : Set a} → Rel A ℓ → (B : Set b) → (B → A) → A → Set _
-leastupperbound _≤_ B f lub = (∀ i → f i ≤ lub) × (∀ y → (∀ i → f i ≤ y) → lub ≤ y)
+leastupperbound  : {A : Set a} → Rel A ℓ → {B : Set b} → (g : B → A) → A → Set _
+leastupperbound _≤_ g lub = (∀ i → g i ≤ lub) × (∀ y → (∀ i → g i ≤ y) → lub ≤ y)
+
+preserveLubs : {A : Set a} {B : Set b } (≤₁ : Rel A ℓ₁) (≤₂ : Rel B ℓ₂) (f : A → B) → Set (suc (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂))
+preserveLubs ≤₁ ≤₂ f =  ∀ I → ∀ {g : I → _} → ∀ lub → leastupperbound ≤₁ g lub → leastupperbound ≤₂ (f ∘ g) (f lub)
\ No newline at end of file
diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda
index 0c1c56ac90..6e38ef1f63 100644
--- a/src/Relation/Binary/Domain/Structures.agda
+++ b/src/Relation/Binary/Domain/Structures.agda
@@ -13,20 +13,21 @@ open import Function using (_∘_)
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Bundles using (Poset)
 open import Relation.Binary.Domain.Definitions
-  using (semidirected; leastupperbound)
+  using (semidirected; leastupperbound; preserveLubs)
+open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
 
 private variable
-  a b c ℓ ℓ₁ ℓ₂ : Level
+  a b c c₁ c₂ ℓ ℓ₁ ℓ₂ ℓ₁₁ ℓ₁₂ ℓ₂₁ ℓ₂₂ : Level
   A B : Set a
 
 
-module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
+module _ (P : Poset c ℓ₁ ℓ₂) where
   open Poset P
 
   record IsLub {b : Level} {B : Set b} (f : B → Carrier)
                (lub : Carrier) : Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where
     field
-      isLeastUpperBound : leastupperbound _≤_ B f lub
+      isLeastUpperBound : leastupperbound _≤_ f lub
 
     isUpperBound : ∀ i → f i ≤ lub
     isUpperBound = proj₁ isLeastUpperBound
@@ -61,20 +62,15 @@ module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
 -- Scott‐continuous maps between two (possibly different‐universe) posets
 ------------------------------------------------------------------------
 
-module _ {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level}
-         (P : Poset c₁ ℓ₁₁ ℓ₁₂)
-         (Q : Poset c₂ ℓ₂₁ ℓ₂₂) where
-
-  private
+module _ (P : Poset c₁ ℓ₁₁ ℓ₁₂) (Q : Poset c₂ ℓ₂₁ ℓ₂₂) 
+  where 
     module P = Poset P
     module Q = Poset Q
 
-  record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂))
-    where
-    field
-      preserveLub : ∀ {B : Set c₁} {g : B → P.Carrier} →
-                    (dir : IsDirectedFamily P g) →
-                    (lub : P.Carrier) →
-                    IsLub P g lub →
-                    IsLub Q (f ∘ g) (f lub)
-      preserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y
+    record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂))
+      where
+      field
+        preservelub : preserveLubs P._≤_ Q._≤_ f
+        isOrderHomomorphism : IsOrderHomomorphism P._≈_ Q._≈_ P._≤_ Q._≤_ f
+
+      open IsOrderHomomorphism isOrderHomomorphism public

From 2384bd394ae6c56c7fad634ab03770639102b141 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Wed, 25 Jun 2025 14:55:53 -0400
Subject: [PATCH 09/11] fixwhitespace

---
 src/Relation/Binary/Domain/Definitions.agda | 2 +-
 src/Relation/Binary/Domain/Structures.agda  | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Relation/Binary/Domain/Definitions.agda b/src/Relation/Binary/Domain/Definitions.agda
index 4af4b0dde7..b019630ed7 100644
--- a/src/Relation/Binary/Domain/Definitions.agda
+++ b/src/Relation/Binary/Domain/Definitions.agda
@@ -38,4 +38,4 @@ leastupperbound  : {A : Set a} → Rel A ℓ → {B : Set b} → (g : B → A) 
 leastupperbound _≤_ g lub = (∀ i → g i ≤ lub) × (∀ y → (∀ i → g i ≤ y) → lub ≤ y)
 
 preserveLubs : {A : Set a} {B : Set b } (≤₁ : Rel A ℓ₁) (≤₂ : Rel B ℓ₂) (f : A → B) → Set (suc (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂))
-preserveLubs ≤₁ ≤₂ f =  ∀ I → ∀ {g : I → _} → ∀ lub → leastupperbound ≤₁ g lub → leastupperbound ≤₂ (f ∘ g) (f lub)
\ No newline at end of file
+preserveLubs ≤₁ ≤₂ f =  ∀ I → ∀ {g : I → _} → ∀ lub → leastupperbound ≤₁ g lub → leastupperbound ≤₂ (f ∘ g) (f lub)
diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda
index 6e38ef1f63..f97b6609f0 100644
--- a/src/Relation/Binary/Domain/Structures.agda
+++ b/src/Relation/Binary/Domain/Structures.agda
@@ -62,8 +62,8 @@ module _ (P : Poset c ℓ₁ ℓ₂) where
 -- Scott‐continuous maps between two (possibly different‐universe) posets
 ------------------------------------------------------------------------
 
-module _ (P : Poset c₁ ℓ₁₁ ℓ₁₂) (Q : Poset c₂ ℓ₂₁ ℓ₂₂) 
-  where 
+module _ (P : Poset c₁ ℓ₁₁ ℓ₁₂) (Q : Poset c₂ ℓ₂₁ ℓ₂₂)
+  where
     module P = Poset P
     module Q = Poset Q
 

From b7534781c870d9e3b6f82181534f84b66167bd2c Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Wed, 25 Jun 2025 14:56:54 -0400
Subject: [PATCH 10/11] {I} instead of I

---
 src/Relation/Binary/Domain/Definitions.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Relation/Binary/Domain/Definitions.agda b/src/Relation/Binary/Domain/Definitions.agda
index b019630ed7..df08a5917c 100644
--- a/src/Relation/Binary/Domain/Definitions.agda
+++ b/src/Relation/Binary/Domain/Definitions.agda
@@ -38,4 +38,4 @@ leastupperbound  : {A : Set a} → Rel A ℓ → {B : Set b} → (g : B → A) 
 leastupperbound _≤_ g lub = (∀ i → g i ≤ lub) × (∀ y → (∀ i → g i ≤ y) → lub ≤ y)
 
 preserveLubs : {A : Set a} {B : Set b } (≤₁ : Rel A ℓ₁) (≤₂ : Rel B ℓ₂) (f : A → B) → Set (suc (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂))
-preserveLubs ≤₁ ≤₂ f =  ∀ I → ∀ {g : I → _} → ∀ lub → leastupperbound ≤₁ g lub → leastupperbound ≤₂ (f ∘ g) (f lub)
+preserveLubs ≤₁ ≤₂ f =  ∀ {I} → ∀ {g : I → _} → ∀ lub → leastupperbound ≤₁ g lub → leastupperbound ≤₂ (f ∘ g) (f lub)
\ No newline at end of file

From 1e41d41add954d6d33e8488b7310d9ab9073a367 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Wed, 25 Jun 2025 15:04:40 -0400
Subject: [PATCH 11/11] remove file

---
 src/Relation/Binary/Domain/Definitions.agda | 2 +-
 src/TestWord8Performance.agda               | 0
 2 files changed, 1 insertion(+), 1 deletion(-)
 delete mode 100644 src/TestWord8Performance.agda

diff --git a/src/Relation/Binary/Domain/Definitions.agda b/src/Relation/Binary/Domain/Definitions.agda
index df08a5917c..b0b0a3e093 100644
--- a/src/Relation/Binary/Domain/Definitions.agda
+++ b/src/Relation/Binary/Domain/Definitions.agda
@@ -38,4 +38,4 @@ leastupperbound  : {A : Set a} → Rel A ℓ → {B : Set b} → (g : B → A) 
 leastupperbound _≤_ g lub = (∀ i → g i ≤ lub) × (∀ y → (∀ i → g i ≤ y) → lub ≤ y)
 
 preserveLubs : {A : Set a} {B : Set b } (≤₁ : Rel A ℓ₁) (≤₂ : Rel B ℓ₂) (f : A → B) → Set (suc (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂))
-preserveLubs ≤₁ ≤₂ f =  ∀ {I} → ∀ {g : I → _} → ∀ lub → leastupperbound ≤₁ g lub → leastupperbound ≤₂ (f ∘ g) (f lub)
\ No newline at end of file
+preserveLubs ≤₁ ≤₂ f =  ∀ {I} → ∀ {g : I → _} → ∀ lub → leastupperbound ≤₁ g lub → leastupperbound ≤₂ (f ∘ g) (f lub)
diff --git a/src/TestWord8Performance.agda b/src/TestWord8Performance.agda
deleted file mode 100644
index e69de29bb2..0000000000