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

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 `DirectedCompletePartialOrder`, `Lub`, and `ScottContinuous`.
+  - All files for domain theory are now available in `src/Relation/Binary/Domain/`.
+
 Additions to existing modules
 -----------------------------
 

src/Relation/Binary/Definitions.agda

@@ -139,6 +139,11 @@ Min R = Max (flip R)
 Minimum : Rel A ℓ → A → Set _
 Minimum = Min
 
+-- Directed families
+
+SemiDirected : Rel A ℓ → (B → A) → Set _
+SemiDirected _≤_ f = ∀ i j → ∃[ k ] (f i ≤ f k × f j ≤ f k)
+
 -- Definitions for apartness relations
 
 -- Note that Cotransitive's arguments are permuted with respect to Transitive's.

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

src/Relation/Binary/Domain/Bundles.agda

@@ -0,0 +1,66 @@
+------------------------------------------------------------------------
+-- 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.Structures using (IsDirectedFamily)
+open import Relation.Binary.Domain.Structures
+  using (IsDirectedCompletePartialOrder; IsScottContinuous
+        ; IsLub)
+
+private
+  variable
+    o ℓ e o' ℓ' e' ℓ₂ : Level
+    Ix A B : Set o
+
+------------------------------------------------------------------------
+-- Directed Complete Partial Orders
+------------------------------------------------------------------------
+
+record DirectedFamily {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {B : Set c} : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    f : B → Poset.Carrier P
+    isDirectedFamily : IsDirectedFamily (Poset._≈_ P) (Poset._≤_ 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 IsDirectedCompletePartialOrder isDirectedCompletePartialOrder public
+
+------------------------------------------------------------------------
+-- Scott-continuous functions
+------------------------------------------------------------------------
+
+record ScottContinuous
+  {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level}
+  (P : Poset c₁ ℓ₁₁ ℓ₁₂)
+  (Q : Poset c₂ ℓ₂₁ ℓ₂₂)
+  (κ : Level) : Set (suc (κ ⊔ c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where
+  field
+    f                 : Poset.Carrier P → Poset.Carrier Q
+    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
+  open Poset P
+  field
+    lub   : Carrier
+    isLub : IsLub P f lub

src/Relation/Binary/Domain/Definitions.agda

@@ -0,0 +1,31 @@
+------------------------------------------------------------------------
+-- 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 Function using (_∘_)
+open import Level using (Level; _⊔_; suc)
+open import Relation.Binary.Core using (Rel)
+
+private
+  variable
+    a b i ℓ ℓ₁ ℓ₂ : Level
+    A : Set a
+    B : Set b
+    I : Set ℓ
+
+------------------------------------------------------------------------
+-- Upper bound
+------------------------------------------------------------------------
+
+UpperBound : {A : Set a} → Rel A ℓ → {B : Set b} → (f : B → A) → A → Set _
+UpperBound _≤_ f x = ∀ i → f i ≤ x

src/Relation/Binary/Domain/Structures.agda

@@ -0,0 +1,64 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Structures for domain theory
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain.Structures where
+
+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.Structures using (IsDirectedFamily)
+open import Relation.Binary.Domain.Definitions using (UpperBound)
+open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
+
+private variable
+  a b c c₁ c₂ ℓ ℓ₁ ℓ₂ ℓ₁₁ ℓ₁₂ ℓ₂₁ ℓ₂₂ : Level
+  A B : Set a
+
+
+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
+      isUpperBound : UpperBound _≤_ f lub
+      isLeast : ∀ y → UpperBound _≤_ f y → lub ≤ y
+
+  record IsDirectedCompletePartialOrder : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+    field
+      ⋁ : ∀ {B : Set c} →
+        (f : B → Carrier) →
+        IsDirectedFamily _≈_ _≤_ f →
+        Carrier
+      ⋁-isLub : ∀ {B : Set c}
+        → (f : B → Carrier)
+        → (dir : IsDirectedFamily _≈_ _≤_ f)
+        → IsLub f (⋁ f dir)
+
+    module _ {B : Set c} {f : B → Carrier} {dir : IsDirectedFamily _≈_ _≤_ f} where
+      open IsLub (⋁-isLub f dir)
+        renaming (isUpperBound to ⋁-≤; isLeast to ⋁-least)
+        public
+
+------------------------------------------------------------------------
+-- Scott‐continuous maps between two (possibly different‐universe) posets
+------------------------------------------------------------------------
+
+module _ (P : Poset c₁ ℓ₁₁ ℓ₁₂) (Q : Poset c₂ ℓ₂₁ ℓ₂₂)
+  where
+    module P = Poset P
+    module Q = Poset Q
+
+    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

src/Relation/Binary/Structures.agda

@@ -317,6 +317,17 @@ record IsDenseLinearOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) wher
   open IsStrictTotalOrder isStrictTotalOrder public
 
 
+------------------------------------------------------------------------
+-- DirectedFamily
+------------------------------------------------------------------------
+
+record IsDirectedFamily {b : Level} {B : Set b} (_≤_ : Rel A ℓ₂) (f : B → A) :
+                        Set (a ⊔ b ⊔ ℓ₂) where
+  field
+    elt            : B
+    isSemidirected : SemiDirected _≤_ f
+
+
 ------------------------------------------------------------------------
 -- Apartness relations
 ------------------------------------------------------------------------