[Draft] working on dcpo presentations

source/DomainTheory/Basics/Exponential.lagda

@@ -197,7 +197,7 @@ DCPO-∘-is-continuous₁ 𝓓 𝓔 𝓔' f I α δ =
      β : I → ⟨ 𝓓 ⟹ᵈᶜᵖᵒ 𝓔' ⟩
      β i = DCPO-∘ 𝓓 𝓔 𝓔' f (α i)
      ε : is-Directed (𝓓 ⟹ᵈᶜᵖᵒ 𝓔') β
-     ε = image-is-directed (𝓔 ⟹ᵈᶜᵖᵒ 𝓔') (𝓓 ⟹ᵈᶜᵖᵒ 𝓔') {DCPO-∘ 𝓓 𝓔 𝓔' f}
+     ε = image-is-Directed (𝓔 ⟹ᵈᶜᵖᵒ 𝓔') (𝓓 ⟹ᵈᶜᵖᵒ 𝓔') {DCPO-∘ 𝓓 𝓔 𝓔' f}
           (DCPO-∘-is-monotone₁ 𝓓 𝓔 𝓔' f) {I} {α} δ
      γ : DCPO-∘ 𝓓 𝓔 𝓔' f (∐ (𝓔 ⟹ᵈᶜᵖᵒ 𝓔') {I} {α} δ) ＝ ∐ (𝓓 ⟹ᵈᶜᵖᵒ 𝓔') {I} {β} ε
      γ = to-continuous-function-＝ 𝓓 𝓔' ψ
@@ -229,7 +229,7 @@ DCPO-∘-is-continuous₂ 𝓓 𝓔 𝓔' g I α δ =
     β : I → ⟨ 𝓓 ⟹ᵈᶜᵖᵒ 𝓔' ⟩
     β i = DCPO-∘ 𝓓 𝓔 𝓔' (α i) g
     ε : is-Directed (𝓓 ⟹ᵈᶜᵖᵒ 𝓔') β
-    ε = image-is-directed (𝓓 ⟹ᵈᶜᵖᵒ 𝓔) (𝓓 ⟹ᵈᶜᵖᵒ 𝓔') {λ f → DCPO-∘ 𝓓 𝓔 𝓔' f g}
+    ε = image-is-Directed (𝓓 ⟹ᵈᶜᵖᵒ 𝓔) (𝓓 ⟹ᵈᶜᵖᵒ 𝓔') {λ f → DCPO-∘ 𝓓 𝓔 𝓔' f g}
          (DCPO-∘-is-monotone₂ 𝓓 𝓔 𝓔' g) {I} {α} δ
     γ : DCPO-∘ 𝓓 𝓔 𝓔' (∐ (𝓓 ⟹ᵈᶜᵖᵒ 𝓔) {I} {α} δ) g ＝ ∐ (𝓓 ⟹ᵈᶜᵖᵒ 𝓔') {I} {β} ε
     γ = to-continuous-function-＝ 𝓓 𝓔' ψ

source/DomainTheory/Basics/Miscelanea.lagda

@@ -98,34 +98,43 @@ Lemmas for establishing Scott continuity of maps between dcpos.
 
 \begin{code}
 
-image-is-directed : (𝓓 : DCPO {𝓤} {𝓣}) (𝓔 : DCPO {𝓤'} {𝓣'})
+image-is-directed : {D : 𝓤 ̇} {E : 𝓤' ̇}
+  → (_⊑_ : D → D → 𝓣 ̇ ) (_≤_ : E → E → 𝓣' ̇ )
+  → {f : D → E} → ((x y : D) → x ⊑ y → f x ≤ f y)
+  → {I : 𝓥 ̇ } → {α : I → D}
+  → is-directed _⊑_ α
+  → is-directed _≤_ (f ∘ α)
+image-is-directed _⊑_ _≤_ {f} m {I} {α} δ =
+ inhabited-if-directed _⊑_ α δ , γ
+  where
+   γ : is-semidirected _≤_ (f ∘ α)
+   γ i j = ∥∥-functor (λ (k , u , v) → k , m (α i) (α k) u , m (α j) (α k) v)
+     (semidirected-if-directed _⊑_ α δ i j)
+
+image-is-Directed : (𝓓 : DCPO {𝓤} {𝓣}) (𝓔 : DCPO {𝓤'} {𝓣'})
                     {f : ⟨ 𝓓 ⟩ → ⟨ 𝓔 ⟩}
                   → is-monotone 𝓓 𝓔 f
                   → {I : 𝓥 ̇ }
                   → {α : I → ⟨ 𝓓 ⟩}
                   → is-Directed 𝓓 α
                   → is-Directed 𝓔 (f ∘ α)
-image-is-directed 𝓓 𝓔 {f} m {I} {α} δ =
- inhabited-if-Directed 𝓓 α δ , γ
-  where
-   γ : is-semidirected (underlying-order 𝓔) (f ∘ α)
-   γ i j = ∥∥-functor (λ (k , u , v) → k , m (α i) (α k) u , m (α j) (α k) v)
-                      (semidirected-if-Directed 𝓓 α δ i j)
+image-is-Directed 𝓓 𝓔 m δ =
+ image-is-directed (underlying-order 𝓓) (underlying-order 𝓔) m δ
 
 continuity-criterion : (𝓓 : DCPO {𝓤} {𝓣}) (𝓔 : DCPO {𝓤'} {𝓣'})
                        (f : ⟨ 𝓓 ⟩ → ⟨ 𝓔 ⟩)
                      → (m : is-monotone 𝓓 𝓔 f)
                      → ((I : 𝓥 ̇ )
                         (α : I → ⟨ 𝓓 ⟩)
                         (δ : is-Directed 𝓓 α)
-                     → f (∐ 𝓓 δ) ⊑⟨ 𝓔 ⟩ ∐ 𝓔 (image-is-directed 𝓓 𝓔 m δ))
+                     → f (∐ 𝓓 δ) ⊑⟨ 𝓔 ⟩ ∐ 𝓔 (image-is-Directed 𝓓 𝓔 m δ))
                      → is-continuous 𝓓 𝓔 f
 continuity-criterion 𝓓 𝓔 f m e I α δ = ub , lb-of-ubs
  where
   ub : (i : I) → f (α i) ⊑⟨ 𝓔 ⟩ f (∐ 𝓓 δ)
   ub i = m (α i) (∐ 𝓓 δ) (∐-is-upperbound 𝓓 δ i)
   ε : is-Directed 𝓔 (f ∘ α)
-  ε = image-is-directed 𝓓 𝓔 m δ
+  ε = image-is-Directed 𝓓 𝓔 m δ
   lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order 𝓔)
               (f (∐ 𝓓 δ)) (f ∘ α)
   lb-of-ubs y u = f (∐ 𝓓 δ) ⊑⟨ 𝓔 ⟩[ e I α δ  ]
@@ -180,7 +189,7 @@ image-is-directed' : (𝓓 : DCPO {𝓤} {𝓣}) (𝓔 : DCPO {𝓤'} {𝓣'})
                      (f : DCPO[ 𝓓 , 𝓔 ]) {I : 𝓥 ̇} {α : I → ⟨ 𝓓 ⟩}
                    → is-Directed 𝓓 α
                    → is-Directed 𝓔 ([ 𝓓 , 𝓔 ]⟨ f ⟩ ∘ α)
-image-is-directed' 𝓓 𝓔 f {I} {α} δ = image-is-directed 𝓓 𝓔 m δ
+image-is-directed' 𝓓 𝓔 f {I} {α} δ = image-is-Directed 𝓓 𝓔 m δ
  where
   m : is-monotone 𝓓 𝓔 [ 𝓓 , 𝓔 ]⟨ f ⟩
   m = monotone-if-continuous 𝓓 𝓔 f
@@ -245,9 +254,9 @@ id-is-continuous : (𝓓 : DCPO {𝓤} {𝓣}) → is-continuous 𝓓 𝓓 id
 id-is-continuous 𝓓 = continuity-criterion 𝓓 𝓓 id (id-is-monotone 𝓓) γ
  where
   γ : (I : 𝓥 ̇) (α : I → ⟨ 𝓓 ⟩) (δ : is-Directed 𝓓 α)
-    → ∐ 𝓓 δ ⊑⟨ 𝓓 ⟩ ∐ 𝓓 (image-is-directed 𝓓 𝓓 (λ x y l → l) δ)
+    → ∐ 𝓓 δ ⊑⟨ 𝓓 ⟩ ∐ 𝓓 (image-is-Directed 𝓓 𝓓 (λ x y l → l) δ)
   γ I α δ = ＝-to-⊑ 𝓓 (∐-independent-of-directedness-witness 𝓓
-             δ (image-is-directed 𝓓 𝓓 (λ x y l → l) δ))
+             δ (image-is-Directed 𝓓 𝓓 (λ x y l → l) δ))
 
 ∘-is-continuous : (𝓓 : DCPO {𝓤} {𝓣}) (𝓔 : DCPO {𝓤'} {𝓣'}) (𝓔' : DCPO {𝓦} {𝓦'})
                   (f : ⟨ 𝓓 ⟩ → ⟨ 𝓔 ⟩) (g : ⟨ 𝓔 ⟩ → ⟨ 𝓔' ⟩)
@@ -263,14 +272,14 @@ id-is-continuous 𝓓 = continuity-criterion 𝓓 𝓓 id (id-is-monotone 𝓓)
   m : is-monotone 𝓓 𝓔' (g ∘ f)
   m x y l = mg (f x) (f y) (mf x y l)
   ψ : (I : 𝓥 ̇) (α : I → ⟨ 𝓓 ⟩) (δ : is-Directed 𝓓 α)
-    → g (f (∐ 𝓓 δ)) ⊑⟨ 𝓔' ⟩ ∐ 𝓔' (image-is-directed 𝓓 𝓔' m δ)
+    → g (f (∐ 𝓓 δ)) ⊑⟨ 𝓔' ⟩ ∐ 𝓔' (image-is-Directed 𝓓 𝓔' m δ)
   ψ I α δ = g (f (∐ 𝓓 δ)) ⊑⟨ 𝓔' ⟩[ l₁ ]
             g (∐ 𝓔 εf)    ⊑⟨ 𝓔' ⟩[ l₂ ]
             ∐ 𝓔' εg       ⊑⟨ 𝓔' ⟩[ l₃ ]
             ∐ 𝓔' ε        ∎⟨ 𝓔' ⟩
    where
     ε : is-Directed 𝓔' (g ∘ f ∘ α)
-    ε = image-is-directed 𝓓 𝓔' m δ
+    ε = image-is-Directed 𝓓 𝓔' m δ
     εf : is-Directed 𝓔 (f ∘ α)
     εf = image-is-directed' 𝓓 𝓔 (f , cf) δ
     εg : is-Directed 𝓔' (g ∘ f ∘ α)

source/DomainTheory/Lifting/LiftingDcpo.lagda

@@ -240,14 +240,14 @@ dcpo.
    where
     γ : (I : 𝓥 ̇) (α : I → ⟨ 𝓛-DCPO ⟩) (δ : is-Directed 𝓛-DCPO α)
       → f̃ (∐ 𝓛-DCPO {I} {α} δ) ⊑⟪ 𝓔 ⟫
-        ∐ (𝓔 ⁻) (image-is-directed 𝓛-DCPO (𝓔 ⁻) f̃-is-monotone {I} {α} δ)
+        ∐ (𝓔 ⁻) (image-is-Directed 𝓛-DCPO (𝓔 ⁻) f̃-is-monotone {I} {α} δ)
     γ I α δ = ∐ˢˢ-is-lowerbound-of-upperbounds 𝓔 (f ∘ value s)
                (being-defined-is-prop s) (∐ (𝓔 ⁻) ε) lem
      where
       s : ⟨ 𝓛-DCPO ⟩
       s = ∐ 𝓛-DCPO {I} {α} δ
       ε : is-Directed (𝓔 ⁻) (f̃ ∘ α)
-      ε = image-is-directed 𝓛-DCPO (𝓔 ⁻) f̃-is-monotone {I} {α} δ
+      ε = image-is-Directed 𝓛-DCPO (𝓔 ⁻) f̃-is-monotone {I} {α} δ
       lem : (q : is-defined s) → f (value s q) ⊑⟪ 𝓔 ⟫ ∐ (𝓔 ⁻) ε
       lem q = f (value s q) ⊑⟪ 𝓔 ⟫[ ⦅1⦆ ]
               f (∐ 𝓓 δ')    ⊑⟪ 𝓔 ⟫[ ⦅2⦆ ]

source/DomainTheory/Presentation/C-Ideal.lagda

@@ -0,0 +1,125 @@
+
+
+\begin{code}
+{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}
+open import MLTT.Spartan hiding (J)
+
+open import UF.FunExt
+open import UF.PropTrunc
+open import UF.Subsingletons
+open import UF.Subsingletons-FunExt
+
+module DomainTheory.Presentation.C-Ideal
+  (pt : propositional-truncations-exist)
+  (fe : Fun-Ext)
+  {𝓤 𝓣 𝓥 𝓦 : Universe}
+ where
+
+open import UF.Powerset
+open PropositionalTruncation pt
+open import UF.ImageAndSurjection pt
+open import Posets.Poset fe
+open PosetAxioms
+open import Posets.FreeSupLattice pt
+
+open import DomainTheory.Basics.Dcpo pt fe 𝓥
+open import DomainTheory.Basics.Miscelanea pt fe 𝓥
+open import DomainTheory.Presentation.Presentation pt fe {𝓤} {𝓣} {𝓥} {𝓦}
+
+
+-- TODO put this at the right place
+Conjunction : (I : 𝓤' ̇) → (I → Ω 𝓥') → Ω (𝓤' ⊔ 𝓥')
+pr₁ (Conjunction I ps) = ∀ i → ps i holds
+pr₂ (Conjunction I ps) = Π-is-prop fe λ _ → holds-is-prop (ps _)
+
+syntax Conjunction I (λ i → p) = ⋀ i ꞉ I , p
+
+module C-Ideal
+  (G : 𝓤 ̇)
+  (_≲_ : G → G → 𝓣 ̇)
+  (_◃_ : Cover-set G _≲_)
+ where
+
+  is-C-ideal : (G → Ω 𝓣') → 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ⊔ 𝓣' ̇
+  is-C-ideal ℑ = downward-closed × cover-closed
+   where
+    downward-closed = ∀ x y → x ≲ y
+      → x ∈ ℑ → y ∈ ℑ
+    cover-closed = ∀ I x (U : I → G) → (x ◃ U) holds
+      → (∀ y → y ∈image U → y ∈ ℑ)
+      → x ∈ ℑ
+
+  being-C-ideal-is-prop : (ℑ : G → Ω 𝓣') → is-prop (is-C-ideal ℑ)
+  being-C-ideal-is-prop ℑ =
+   ×-is-prop
+    (Π₄-is-prop fe λ _ _ _ _ → ∈-is-prop ℑ _)
+    (Π₅-is-prop fe λ _ _ _ _ _ → ∈-is-prop ℑ _)
+
+  intersection-is-C-ideal
+   : {I : 𝓥' ̇} (ℑs : I → G → Ω 𝓣')
+   → (∀ i → is-C-ideal (ℑs i))
+   → is-C-ideal λ g → ⋀ i ꞉ _ , ℑs i g
+  intersection-is-C-ideal ℑs ιs = dc , cc
+   where
+    dc = λ x y x≲y x∈ℑs i → pr₁ (ιs i) x y x≲y (x∈ℑs i)
+    cc = λ J g U g◃U c i → pr₂ (ιs i) J g U g◃U λ g' g'∈U → c g' g'∈U i
+
+  C-Idl : ∀ 𝓣' → 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ⊔ 𝓣' ⁺ ̇
+  C-Idl 𝓣' = Σ (is-C-ideal {𝓣' = 𝓣'})
+
+  module _ {𝓣' : Universe} where
+   carrier : C-Idl 𝓣' → G → Ω 𝓣'
+   carrier (ℑ , _) = ℑ
+
+   C-ideality : (𝓘 : C-Idl 𝓣') → is-C-ideal (carrier 𝓘)
+   C-ideality (_ , ι) = ι
+
+   _⊑_ : C-Idl 𝓣' → C-Idl 𝓣' → 𝓤 ⊔ 𝓣' ̇
+   (ℑ , ℑ-is-ideal) ⊑ (𝔍 , 𝔍-is-ideal) = ℑ ⊆ 𝔍
+
+  -- The impredicatively generated C-ideal from a set
+  Generated : ∀ 𝓣' → (G → Ω 𝓥') → C-Idl (𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ⊔ 𝓥' ⊔ 𝓣' ⁺)
+  Generated 𝓣' S = (λ g → ⋀ ((ℑ , _) , _) ꞉  -- Too messy
+   (Σ (ℑ , _) ꞉ C-Idl 𝓣' , S ⊆ ℑ), ℑ g) ,
+   intersection-is-C-ideal (pr₁ ∘ pr₁) (pr₂ ∘ pr₁)
+
+  Generated-contains : (S : G → Ω 𝓥') → S ⊆ carrier (Generated 𝓣' S)
+  Generated-contains S g g∈S ((ℑ , ι), S⊆ℑ) = S⊆ℑ g g∈S
+
+  -- Universal property
+  private module SL = SupLattice
+
+  -- C-Ideals form a suplattice
+  -- set assumptions not included yet
+  C-Idl-SupLattice : ∀ 𝓣' 𝓦' → SupLattice 𝓦' _ _
+  SL.L (C-Idl-SupLattice 𝓣' 𝓦') =
+   C-Idl (𝓤 ⊔ 𝓣 ⊔ (𝓥 ⁺) ⊔ 𝓦 ⊔ (𝓣' ⁺) ⊔ 𝓦')
+
+  SL.L-is-set (C-Idl-SupLattice 𝓣' 𝓦') =
+   {!!}
+
+  SL._⊑_ (C-Idl-SupLattice 𝓣' 𝓦') (ℑ , ι) (𝔍 , υ) =
+   ℑ ⊆ 𝔍
+
+  SL.⊑-is-prop-valued (C-Idl-SupLattice 𝓣' 𝓦') =
+   {!!}
+
+  SL.⊑-is-reflexive (C-Idl-SupLattice 𝓣' 𝓦') _ _ =
+   id
+
+  SL.⊑-is-transitive (C-Idl-SupLattice 𝓣' 𝓦') _ _ _ ℑ⊆𝔍 𝔍⊆𝔎 u i∈ℑ =
+   𝔍⊆𝔎 u (ℑ⊆𝔍 u i∈ℑ)
+
+  SL.⊑-is-antisymmetric (C-Idl-SupLattice 𝓣' 𝓦') =
+   {!!}
+
+  SL.⋁ (C-Idl-SupLattice 𝓣' 𝓦') ℑs =
+   Generated 𝓣' λ g →
+   (∃ i ꞉ _ , g ∈ carrier (ℑs i)) , ∃-is-prop
+
+  SL.⋁-is-upperbound (C-Idl-SupLattice 𝓣' 𝓦') =
+   {!!}
+
+  SL.⋁-is-lowerbound-of-upperbounds (C-Idl-SupLattice 𝓣' 𝓦') =
+   {!!}
+\end{code}

source/DomainTheory/Presentation/Type.lagda

@@ -0,0 +1,77 @@
+(...)
+
+\begin{code}
+{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}
+open import MLTT.Spartan hiding (J)
+
+open import UF.FunExt
+open import UF.PropTrunc
+open import UF.Subsingletons
+
+module DomainTheory.Presentation.Type
+  (pt : propositional-truncations-exist)
+  (fe : Fun-Ext)
+  {𝓤 𝓣 𝓥 𝓦 : Universe}
+  -- 𝓤 : the universe of the underlying set
+  -- 𝓣 : the universe of the preorder
+  -- 𝓥 : the universe of the indices of directed sets
+  -- 𝓦 : the universe of covering sets
+ where
+
+open import UF.Powerset
+open import Posets.Poset fe
+open PosetAxioms
+
+open import DomainTheory.Basics.Dcpo pt fe 𝓥
+open import DomainTheory.Basics.Miscelanea pt fe 𝓥
+
+module _
+  (G : 𝓤 ̇)  -- Generators
+  (_≲_ : G → G → 𝓣 ̇)
+  where
+
+  Cover-set : 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⁺ ̇ -- This one has spurious assumptions
+  Cover-set = G → {I : 𝓥 ̇} → (I → G) → Ω 𝓦
+
+  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 → is-directed _≲_ U
+
+DCPO-Presentation : (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣)⁺ ̇
+DCPO-Presentation =
+ Σ G ꞉ 𝓤 ̇ ,
+ Σ _⊑_ ꞉ (G → G → 𝓣 ̇) ,
+ Σ _◃_ ꞉ (Cover-set G _⊑_) ,
+ (is-dcpo-presentation G _⊑_ _◃_)
+
+module _ (𝓖 : DCPO-Presentation) where
+ ⟨_⟩ₚ : 𝓤 ̇ -- We need a uniform way to refer to underlying sets
+ ⟨_⟩ₚ = 𝓖 .pr₁
+
+ underlying-preorder = 𝓖 .pr₂ .pr₁
+
+ cover-set = 𝓖 .pr₂ .pr₂ .pr₁ -- better syntax?
+
+ cover-directed = 𝓖 .pr₂ .pr₂ .pr₂ .pr₂
+
+-- Defines maps from a presentation into dcpos
+module Interpretation (𝓖 : DCPO-Presentation) (𝓓 : DCPO {𝓤} {𝓣}) where
+ private
+  _≤_ = underlying-order 𝓓
+  _≲_ = underlying-preorder 𝓖
+  _◃_ = cover-set 𝓖
+
+ 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}

source/Posets/FreeSupLattice.lagda

@@ -28,7 +28,7 @@ and syntax for reasoning about the order ⊑.
 
 \begin{code}
 
-record SupLattice (𝓥 𝓤 𝓣 : Universe) : 𝓤ω where
+record SupLattice (𝓥 𝓤 𝓣 : Universe) : 𝓥 ⁺ ⊔ 𝓤 ⁺ ⊔ 𝓣 ⁺ ̇ where
   constructor
     lattice
   field