Projections

source/DomainTheory/Presentation/Presentation.lagda

@@ -11,7 +11,7 @@ open import UF.Subsingletons
 module DomainTheory.Presentation.Presentation
         (pt : propositional-truncations-exist)
         (fe : Fun-Ext)
-        (𝓤 𝓥 𝓦 : Universe)
+        {𝓤 𝓥 𝓦 : Universe}  -- TODO clear universe levels
        where
 
 open import UF.Powerset
@@ -26,39 +26,47 @@ module _
   (_≲_ : G → G → 𝓣 ̇)
   where
 
-  cover-set : 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⁺ ̇
-  cover-set = G → {I : 𝓥 ̇} → (I → G) → Ω 𝓦
+  Cover-set : 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⁺ ̇
+  Cover-set = G → {I : 𝓥 ̇} → (I → G) → Ω 𝓦
 
-  is-dcpo-presentation : cover-set → 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ̇
-  is-dcpo-presentation _◃_ = ≲-prop-valued × ≲-reflexive × ≲-transitive × cover-directed
+  is-dcpo-presentation : Cover-set → 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ̇
+  is-dcpo-presentation _◃_ = (≲-prop-valued × ≲-reflexive × ≲-transitive) × Cover-directed
     where
       ≲-prop-valued = {x y : G} → is-prop (x ≲ y)
       ≲-reflexive = {x : G} → x ≲ x
       ≲-transitive = {x y z : G} → x ≲ y → y ≲ z → x ≲ z
-      cover-directed = {x : G} {I : 𝓥 ̇} {U : I → G} → (x ◃ U) holds
+      Cover-directed = {x : G} {I : 𝓥 ̇} {U : I → G} → (x ◃ U) holds
         → is-directed _≲_ U
 
-  -- TODO: Define structure and projections
-  -- and characterize paths (better paths using powersets)
+DCPO-Presentation : {𝓣 : Universe} → (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣)⁺ ̇
+DCPO-Presentation {𝓣} = Σ G ꞉ 𝓤 ̇ , Σ _⊑_ ꞉ (G → G → 𝓣 ̇) ,
+  Σ _◃_ ꞉ (Cover-set G _⊑_) , (is-dcpo-presentation G _⊑_ _◃_)
 
-  module Interpretation
-    (_◃_ : cover-set)
-    (◃-is-dcpo-presentation : is-dcpo-presentation _◃_)
-    {𝓓 : DCPO {𝓤} {𝓣}}
-    where  -- Defines maps from a presentation into dcpos
+module _ (𝓖 : DCPO-Presentation {𝓣}) where
+  ⟨_⟩ₚ : 𝓤 ̇ -- We need a uniform way to refer to underlying sets
+  ⟨_⟩ₚ = 𝓖 .pr₁
 
-    private
-      U-is-directed : {x : G} {I : 𝓥 ̇} {U : I → G} → (x ◃ U) holds
-        → is-directed _≲_ U
-      U-is-directed = ◃-is-dcpo-presentation .pr₂ .pr₂ .pr₂
+  underlying-preorder = 𝓖 .pr₂ .pr₁
+
+  cover-set = 𝓖 .pr₂ .pr₂ .pr₁ -- better syntax?
+
+  cover-directed = 𝓖 .pr₂ .pr₂ .pr₂ .pr₂
+
+module Interpretation
+  (𝓖 : DCPO-Presentation {𝓣})
+  (𝓓 : DCPO {𝓤} {𝓣})
+  where  -- Defines maps from a presentation into dcpos
 
-      _≤_ = underlying-order 𝓓
+  private
+    _≤_ = underlying-order 𝓓
+    _≲_ = underlying-preorder 𝓖
+    _◃_ = cover-set 𝓖
 
-    preserves-covers : (f : G → ⟨ 𝓓 ⟩)
-      → ((x y : G) → x ≲ y → f x ⊑⟨ 𝓓 ⟩ f y)
-      → 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ̇
-    preserves-covers f m = {x : G} {I : 𝓥 ̇} {U : I → G}
-      → (c : (x ◃ U) holds)
-      → f x  ⊑⟨ 𝓓 ⟩  ∐ 𝓓 (image-is-directed _≲_ _≤_ m (U-is-directed c))
+  preserves-covers : (f : ⟨ 𝓖 ⟩ₚ → ⟨ 𝓓 ⟩)
+    → ((x y : ⟨ 𝓖 ⟩ₚ) → x ≲ y → f x ≤ f y)
+    → 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ̇
+  preserves-covers f m = {x : ⟨ 𝓖 ⟩ₚ} {I : 𝓥 ̇} {U : I → ⟨ 𝓖 ⟩ₚ}
+    → (c : (x ◃ U) holds)
+    → f x ≤ ∐ 𝓓 (image-is-directed _≲_ _≤_ m (cover-directed 𝓖 c))
 
 \end{code}