Predomains

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
 -----------------------------
 
@@ -99,6 +104,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

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 (but: we drop the inhabitedness condition)
+
+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 _

src/Relation/Binary/Predomain/Definitions.agda

@@ -0,0 +1,47 @@
+------------------------------------------------------------------------
+-- 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 Level using (Level; _⊔_)
+open import Relation.Unary using (Pred)
+
+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 y = ∀ i → f i ≤ y
+
+------------------------------------------------------------------------
+-- 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    : x ≤ z → UpperBound f z → y ≤ z
+

src/Relation/Binary/Predomain/Morphism/Structures.agda

@@ -0,0 +1,42 @@
+------------------------------------------------------------------------
+-- 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 Function.Base using (_∘_)
+open import Level using (Level; suc; _⊔_)
+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 ⟧
+
+

src/Relation/Binary/Predomain/Structures.agda

@@ -0,0 +1,95 @@
+------------------------------------------------------------------------
+-- 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
+
+import Data.Empty.Polymorphic as Empty
+open import Function.Base using (_on_)
+open import Level using (Level; suc; _⊔_)
+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
+    x : A
+
+
+------------------------------------------------------------------------
+-- Directed-complete Preorders
+------------------------------------------------------------------------
+
+record IsDCPreorder {i} (_≲_ : Rel A ℓ′) : Set (a ⊔ ℓ ⊔ ℓ′ ⊔ suc i) where
+  field
+    isPreorder : IsPreorder _≲_
+    _≲⋁[_]_   : ∀ {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)
+
+
+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 ≤ᶠ⋁; ≲⋁-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
+
+  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