[Add] Initial files for Domain theory

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/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,63 @@
+------------------------------------------------------------------------
+-- 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
+  using (IsDirectedFamily; 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} (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
+  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₂ ℓ₂₁ ℓ₂₂) : 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,41 @@
+------------------------------------------------------------------------
+-- 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 ℓ
+
+------------------------------------------------------------------------
+-- Directed families
+------------------------------------------------------------------------
+
+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} → (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)

src/Relation/Binary/Domain/Structures.agda

@@ -0,0 +1,76 @@
+------------------------------------------------------------------------
+-- 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.Domain.Definitions
+  using (semidirected; leastupperbound; preserveLubs)
+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
+      isLeastUpperBound : leastupperbound _≤_ f lub
+
+    isUpperBound : ∀ i → f i ≤ lub
+    isUpperBound = proj₁ isLeastUpperBound
+
+    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
+    no-eta-equality
+    field
+      elt            : B
+      isSemidirected : semidirected _≤_ B f
+
+  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) : Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂))
+      where
+      field
+        preservelub : preserveLubs P._≤_ Q._≤_ f
+        isOrderHomomorphism : IsOrderHomomorphism P._≈_ Q._≈_ P._≤_ Q._≤_ f
+
+      open IsOrderHomomorphism isOrderHomomorphism public