comments

Author: jmougeot

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
 -----------------------------
 

src/Relation/Binary/Domain/Bundles.agda

@@ -4,41 +4,56 @@
 -- 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
-module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
-  open Poset P
+private
+  variable
+    o ℓ e o' ℓ' e' ℓ₂ : Level
+    Ix A B : Set o
 
-  record Lub {Ix : Set c} (s : Ix → Carrier)  : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
-    constructor mkLub
-    field
-      lub : Carrier
-      is-upperbound : ∀ i → s i ≤ lub
-      is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y
+------------------------------------------------------------------------
+-- DCPOs
+------------------------------------------------------------------------
 
-  record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
-    field
-      poset    : Poset c ℓ₁ ℓ₂
-      DcpoStr  : IsDCPO poset
+record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  field
+    poset   : Poset c ℓ₁ ℓ₂
+    DcpoStr : IsDCPO poset
 
-    open Poset poset public
-    open IsDCPO DcpoStr public
+  open Poset poset public
+  open IsDCPO DcpoStr public
+
+------------------------------------------------------------------------
+-- Scott-continuous functions
+------------------------------------------------------------------------
 
-module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where
+module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) (Q : Poset c ℓ₁ ℓ₂) where
   private
     module P = Poset P
     module Q = Poset Q
 
-  -- record ScottContinuous : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
-  --   field
-  --     Function : (f : P.Carrier → Q.Carrier)
-  --     Scottfunciton : IsScottContinuous f
+  record ScottContinuous : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+    field
+      f             : P.Carrier → Q.Carrier
+      Scottfunction : IsScottContinuous {P = P} {Q = Q} f
+
+------------------------------------------------------------------------
+-- Lubs
+------------------------------------------------------------------------
 
+module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
+  open Poset P
+
+  record Lub {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+    constructor mkLub
+    field
+      lub           : Carrier
+      is-upperbound : ∀ i → s i ≤ lub
+      is-least      : ∀ y → (∀ i → s i ≤ y) → lub ≤ y

src/Relation/Binary/Domain/Definitions.agda

@@ -4,24 +4,32 @@
 -- 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
+private
+  variable
+    c o ℓ e o' ℓ' e' ℓ₁ ℓ₂ : Level
+    Ix A B : Set o
+    P : Poset c ℓ e
+
+------------------------------------------------------------------------
+-- Monotonicity
+------------------------------------------------------------------------
 
-module _ where
-  IsMonotone : (P : Poset o ℓ e) → (Q : Poset o' ℓ' e') → (f : Poset.Carrier P → Poset.Carrier Q) → Set (o ⊔ ℓ ⊔ e ⊔ ℓ' ⊔ e')
-  IsMonotone P Q f = IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f
+IsMonotone : (P : Poset o ℓ e) → (Q : Poset o' ℓ' e') → (f : Poset.Carrier P → Poset.Carrier Q) → Set (o ⊔ ℓ ⊔ e ⊔ ℓ' ⊔ e')
+IsMonotone P Q f = IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f
+
+------------------------------------------------------------------------
+-- Directed families
+------------------------------------------------------------------------
 
-module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
-  open Poset P
-  IsSemidirectedFamily : ∀ {Ix : Set c} → (s : Ix → Carrier) → Set _
-  IsSemidirectedFamily s = ∀ i j → ∃[ k ] (s i ≤ s k × 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))
 

src/Relation/Binary/Domain/Structures.agda

@@ -4,6 +4,8 @@
 -- Structures for domain theory
 ------------------------------------------------------------------------
 
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module Relation.Binary.Domain.Structures where
 
 open import Data.Product using (_×_; _,_)

src/Relation/Binary/Properties/Domain.agda

@@ -11,17 +11,16 @@ open import Level using (Level; Lift; lift)
 open import Function using (_∘_; id)
 open import Data.Product using (_,_)
 open import Data.Bool using (Bool; true; false; if_then_else_)
-open import Relation.Binary.Domain.Definitions
+open import Relation.Binary.Domain.Bundles using (DCPO)
+open import Relation.Binary.Domain.Definitions using (IsMonotone)
 open import Relation.Binary.Domain.Structures
-open import Relation.Binary.Domain.Bundles
+  using (IsDirectedFamily; IsDCPO; IsLub; IsScottContinuous)
 open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
 
-
 private variable
   c ℓ₁ ℓ₂ o ℓ : Level
   Ix A B : Set o
 
-
 module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} {D : DCPO P c ℓ₁ ℓ₂ } where
   private
     module D = DCPO D