From 15bcc35bd161d26f7fc1d7c62e99a8b673c7f884 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Thu, 23 Feb 2023 14:31:11 +0800
Subject: [PATCH 01/27] Preliminary definition of dcpo presentations

---
 .../Presentation/Presentation.lagda           | 40 +++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 source/DomainTheory/Presentation/Presentation.lagda

diff --git a/source/DomainTheory/Presentation/Presentation.lagda b/source/DomainTheory/Presentation/Presentation.lagda
new file mode 100644
index 000000000..f159bc618
--- /dev/null
+++ b/source/DomainTheory/Presentation/Presentation.lagda
@@ -0,0 +1,40 @@
+(...)
+
+\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.Presentation
+        (pt : propositional-truncations-exist)
+        (fe : Fun-Ext)
+        (𝓤 𝓥 𝓦 : Universe)
+       where
+
+open import UF.Powerset
+open import Posets.Poset fe
+open PosetAxioms
+
+open import DomainTheory.Basics.Dcpo pt fe 𝓥
+
+module _
+  (G : 𝓤 ̇)  -- Generators
+  (_≲_ : G → G → 𝓣 ̇)
+  where
+
+  cover-set : 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⁺ ̇
+  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
+
+\end{code}

From 1e194b9ca0c94297420b75d5bb2ae0e739de86f3 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 24 Feb 2023 10:37:37 +0800
Subject: [PATCH 02/27] Interpretation

---
 .../Presentation/Presentation.lagda           | 22 +++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/source/DomainTheory/Presentation/Presentation.lagda b/source/DomainTheory/Presentation/Presentation.lagda
index f159bc618..8695df7d3 100644
--- a/source/DomainTheory/Presentation/Presentation.lagda
+++ b/source/DomainTheory/Presentation/Presentation.lagda
@@ -19,6 +19,7 @@ open import Posets.Poset fe
 open PosetAxioms
 
 open import DomainTheory.Basics.Dcpo pt fe 𝓥
+open import DomainTheory.Basics.Miscelanea pt fe 𝓥
 
 module _
   (G : 𝓤 ̇)  -- Generators
@@ -37,4 +38,25 @@ module _
       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)
+
+  module Interpretation
+    (_◃_ : cover-set)
+    (◃-is-dcpo-presentation : is-dcpo-presentation _◃_)
+    {D : DCPO {𝓤} {𝓣}}
+    where  -- Defines maps from a presentation into dcpos
+
+    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₂
+
+    preserves-covers : (f : G → ⟨ D ⟩)
+      → ({x y : G} → x ≲ y → f x ⊑⟨ D ⟩ f y)
+      → 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ̇
+    preserves-covers f m = {x : G} {I : 𝓥 ̇} {U : I → G}
+      → (c : (x ◃ U) holds)
+      → f x ⊑⟨ D ⟩ ∐ D {! U-is-directed c  !}
+
 \end{code}

From 89788c57cd96b33aaea6c75889fd526b08e590b3 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 24 Feb 2023 10:52:36 +0800
Subject: [PATCH 03/27] Refactor `image-is-directed`

---
 source/DomainTheory/Basics/Exponential.lagda  |  4 +-
 source/DomainTheory/Basics/Miscelanea.lagda   | 37 ++++++++++++-------
 source/DomainTheory/Lifting/LiftingDcpo.lagda |  4 +-
 3 files changed, 27 insertions(+), 18 deletions(-)

diff --git a/source/DomainTheory/Basics/Exponential.lagda b/source/DomainTheory/Basics/Exponential.lagda
index 8ee831b03..924e2c695 100644
--- a/source/DomainTheory/Basics/Exponential.lagda
+++ b/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-＝ 𝓓 𝓔' ψ
diff --git a/source/DomainTheory/Basics/Miscelanea.lagda b/source/DomainTheory/Basics/Miscelanea.lagda
index 15e4f3f2a..e090ca833 100644
--- a/source/DomainTheory/Basics/Miscelanea.lagda
+++ b/source/DomainTheory/Basics/Miscelanea.lagda
@@ -98,19 +98,28 @@ 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 : ⟨ 𝓓 ⟩ → ⟨ 𝓔 ⟩)
@@ -118,14 +127,14 @@ continuity-criterion : (𝓓 : DCPO {𝓤} {𝓣}) (𝓔 : DCPO {𝓤'} {𝓣'})
                      → ((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 ∘ α)
diff --git a/source/DomainTheory/Lifting/LiftingDcpo.lagda b/source/DomainTheory/Lifting/LiftingDcpo.lagda
index 52ff4b72d..f2c0c87c1 100644
--- a/source/DomainTheory/Lifting/LiftingDcpo.lagda
+++ b/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⦆ ]

From 8942871ffc20085a504cdaa519b77c7b259f2621 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 24 Feb 2023 11:04:54 +0800
Subject: [PATCH 04/27] Define cover preserving map

---
 source/DomainTheory/Presentation/Presentation.lagda | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/source/DomainTheory/Presentation/Presentation.lagda b/source/DomainTheory/Presentation/Presentation.lagda
index 8695df7d3..e0805294e 100644
--- a/source/DomainTheory/Presentation/Presentation.lagda
+++ b/source/DomainTheory/Presentation/Presentation.lagda
@@ -44,7 +44,7 @@ module _
   module Interpretation
     (_◃_ : cover-set)
     (◃-is-dcpo-presentation : is-dcpo-presentation _◃_)
-    {D : DCPO {𝓤} {𝓣}}
+    {𝓓 : DCPO {𝓤} {𝓣}}
     where  -- Defines maps from a presentation into dcpos
 
     private
@@ -52,11 +52,13 @@ module _
         → is-directed _≲_ U
       U-is-directed = ◃-is-dcpo-presentation .pr₂ .pr₂ .pr₂
 
-    preserves-covers : (f : G → ⟨ D ⟩)
-      → ({x y : G} → x ≲ y → f x ⊑⟨ D ⟩ f y)
+      _≤_ = underlying-order 𝓓
+
+    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 ⊑⟨ D ⟩ ∐ D {! U-is-directed c  !}
+      → f x  ⊑⟨ 𝓓 ⟩  ∐ 𝓓 (image-is-directed _≲_ _≤_ m (U-is-directed c))
 
 \end{code}

From 0d84848105476b7fa904ca91fc5619bea85d370c Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 24 Feb 2023 13:09:02 +0800
Subject: [PATCH 05/27] Projections

---
 .../Presentation/Presentation.lagda           | 56 +++++++++++--------
 1 file changed, 32 insertions(+), 24 deletions(-)

diff --git a/source/DomainTheory/Presentation/Presentation.lagda b/source/DomainTheory/Presentation/Presentation.lagda
index e0805294e..a3c5f6a79 100644
--- a/source/DomainTheory/Presentation/Presentation.lagda
+++ b/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}

From da91febe5637cac91b4d3b2693195f1ad82ff255 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 24 Feb 2023 17:08:48 +0800
Subject: [PATCH 06/27] C-Ideals

---
 .../DomainTheory/Presentation/C-Ideal.lagda   | 48 +++++++++++++++++++
 1 file changed, 48 insertions(+)
 create mode 100644 source/DomainTheory/Presentation/C-Ideal.lagda

diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
new file mode 100644
index 000000000..07c838556
--- /dev/null
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -0,0 +1,48 @@
+
+
+\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 import UF.ImageAndSurjection pt
+open import Posets.Poset fe
+open PosetAxioms
+
+open import DomainTheory.Basics.Dcpo pt fe 𝓥
+open import DomainTheory.Basics.Miscelanea pt fe 𝓥
+open import DomainTheory.Presentation.Presentation pt fe {𝓤} {𝓥} {𝓦}
+
+module C-Ideal
+  (G : 𝓤 ̇)
+  (_≲_ : G → G → 𝓣 ̇)
+  (_◃_ : Cover-set G _≲_)
+  (ℑ : G → Ω 𝓣')
+  where
+
+  is-C-ideal : 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ⊔ 𝓣' ̇
+  is-C-ideal = downward-closed × cover-closed
+    where
+      downward-closed = ∀ x y → x ≲ y
+        → ℑ x holds → ℑ y holds
+      cover-closed = ∀ I x (U : I → G) → (x ◃ U) holds
+        → (∀ y → y ∈image U → ℑ y holds)
+        → ℑ x holds
+
+  being-C-ideal-is-prop : is-prop is-C-ideal
+  being-C-ideal-is-prop = ×-is-prop
+    (Π₄-is-prop fe λ _ _ _ _ → holds-is-prop (ℑ _))
+    (Π₅-is-prop fe λ _ _ _ _ _ → holds-is-prop (ℑ _))
+
+\end{code}

From 49d9265923bcc2285455933f371608c4e0933539 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 24 Feb 2023 17:35:50 +0800
Subject: [PATCH 07/27] =?UTF-8?q?Use=20=E2=88=88?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 source/DomainTheory/Presentation/C-Ideal.lagda | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
index 07c838556..c6d8f490c 100644
--- a/source/DomainTheory/Presentation/C-Ideal.lagda
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -35,14 +35,14 @@ module C-Ideal
   is-C-ideal = downward-closed × cover-closed
     where
       downward-closed = ∀ x y → x ≲ y
-        → ℑ x holds → ℑ y holds
+        → x ∈ ℑ → y ∈ ℑ
       cover-closed = ∀ I x (U : I → G) → (x ◃ U) holds
-        → (∀ y → y ∈image U → ℑ y holds)
-        → ℑ x holds
+        → (∀ y → y ∈image U → y ∈ ℑ)
+        → x ∈ ℑ
 
   being-C-ideal-is-prop : is-prop is-C-ideal
   being-C-ideal-is-prop = ×-is-prop
-    (Π₄-is-prop fe λ _ _ _ _ → holds-is-prop (ℑ _))
-    (Π₅-is-prop fe λ _ _ _ _ _ → holds-is-prop (ℑ _))
+    (Π₄-is-prop fe λ _ _ _ _ → ∈-is-prop ℑ _)
+    (Π₅-is-prop fe λ _ _ _ _ _ → ∈-is-prop ℑ _)
 
 \end{code}

From 3b323ccbfb4ef984bca160a2a8bd86ff7fd33d06 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 24 Feb 2023 17:44:36 +0800
Subject: [PATCH 08/27] Start to define C-Idl

---
 .../DomainTheory/Presentation/C-Ideal.lagda   | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
index c6d8f490c..035028a89 100644
--- a/source/DomainTheory/Presentation/C-Ideal.lagda
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -24,7 +24,7 @@ open import DomainTheory.Basics.Dcpo pt fe 𝓥
 open import DomainTheory.Basics.Miscelanea pt fe 𝓥
 open import DomainTheory.Presentation.Presentation pt fe {𝓤} {𝓥} {𝓦}
 
-module C-Ideal
+module C-Ideal {𝓣'}
   (G : 𝓤 ̇)
   (_≲_ : G → G → 𝓣 ̇)
   (_◃_ : Cover-set G _≲_)
@@ -45,4 +45,21 @@ module C-Ideal
     (Π₄-is-prop fe λ _ _ _ _ → ∈-is-prop ℑ _)
     (Π₅-is-prop fe λ _ _ _ _ _ → ∈-is-prop ℑ _)
 
+module _ {𝓣'}
+  (G : 𝓤 ̇)
+  (_≲_ : G → G → 𝓣 ̇)
+  (_◃_ : Cover-set G _≲_) where
+  open C-Ideal {𝓣' = 𝓣'} G _≲_ _◃_
+
+  C-Idl = Σ is-C-ideal
+
+  carrier : C-Idl → G → Ω 𝓣'
+  carrier (ℑ , _) = ℑ
+
+  C-ideality : (𝓘 : C-Idl) → is-C-ideal (carrier 𝓘)
+  C-ideality (_ , i) = i
+
+  _⊑_ : C-Idl → C-Idl → 𝓤 ⊔ 𝓣' ̇
+  (ℑ , ℑ-is-ideal) ⊑ (𝔍 , 𝔍-is-ideal) = ℑ ⊆ 𝔍
+
 \end{code}

From 30934f32448a90850d8cc48f2baf161345b51ce1 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 24 Feb 2023 22:54:06 +0800
Subject: [PATCH 09/27] Impredicative ideal generation

---
 .../DomainTheory/Presentation/C-Ideal.lagda   | 75 ++++++++++++-------
 1 file changed, 48 insertions(+), 27 deletions(-)

diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
index 035028a89..1d1d13b40 100644
--- a/source/DomainTheory/Presentation/C-Ideal.lagda
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -24,42 +24,63 @@ open import DomainTheory.Basics.Dcpo pt fe 𝓥
 open import DomainTheory.Basics.Miscelanea pt fe 𝓥
 open import DomainTheory.Presentation.Presentation pt fe {𝓤} {𝓥} {𝓦}
 
-module C-Ideal {𝓣'}
+
+-- TODO put this at the right place
+Conjunction : (I : 𝓣' ̇) → (I → Ω 𝓣) → Ω (𝓣 ⊔ 𝓣')
+Conjunction I ps = (∀ i → ps i holds) , Π-is-prop fe λ _ → holds-is-prop (ps _)
+
+syntax Conjunction I (λ i → p) = ⋀ i ꞉ I , p
+
+module C-Ideal
   (G : 𝓤 ̇)
   (_≲_ : G → G → 𝓣 ̇)
   (_◃_ : Cover-set G _≲_)
-  (ℑ : G → Ω 𝓣')
-  where
-
-  is-C-ideal : 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ⊔ 𝓣' ̇
-  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 : is-prop is-C-ideal
-  being-C-ideal-is-prop = ×-is-prop
+ 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 ℑ _)
 
-module _ {𝓣'}
-  (G : 𝓤 ̇)
-  (_≲_ : G → G → 𝓣 ̇)
-  (_◃_ : Cover-set G _≲_) where
-  open C-Ideal {𝓣' = 𝓣'} G _≲_ _◃_
+  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 = Σ is-C-ideal
+    _⊑_ : C-Idl 𝓣' → C-Idl 𝓣' → 𝓤 ⊔ 𝓣' ̇
+    (ℑ , ℑ-is-ideal) ⊑ (𝔍 , 𝔍-is-ideal) = ℑ ⊆ 𝔍
 
-  carrier : C-Idl → G → Ω 𝓣'
-  carrier (ℑ , _) = ℑ
+  -- The impredicatively generated C-ideal from a set
+  Generated : (𝓣' : Universe) → (G → Ω 𝓥') → C-Idl (𝓤 ⊔ (𝓥 ⁺) ⊔ 𝓦 ⊔ 𝓣 ⊔ 𝓥' ⊔ (𝓣' ⁺))
+  Generated 𝓣' S = (λ g → ⋀ ((ℑ , _) , _) ꞉  -- Too messy
+    (Σ (ℑ , _) ꞉ C-Idl 𝓣' , S ⊆ ℑ), ℑ g) ,
+    intersection-is-C-ideal (pr₁ ∘ pr₁) (pr₂ ∘ pr₁)
 
-  C-ideality : (𝓘 : C-Idl) → is-C-ideal (carrier 𝓘)
-  C-ideality (_ , i) = i
+  Generated-contains : (S : G → Ω 𝓥') → S ⊆ carrier (Generated 𝓣' S)
+  Generated-contains S g g∈S ((ℑ , ι), S⊆ℑ) = S⊆ℑ g g∈S
 
-  _⊑_ : C-Idl → C-Idl → 𝓤 ⊔ 𝓣' ̇
-  (ℑ , ℑ-is-ideal) ⊑ (𝔍 , 𝔍-is-ideal) = ℑ ⊆ 𝔍
+  -- Universal property
 
 \end{code}

From cb5d45c77e3111099a001a056a58ffd4641cf50a Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 24 Feb 2023 23:55:53 +0800
Subject: [PATCH 10/27] Sort out universe levels

---
 source/DomainTheory/Presentation/C-Ideal.lagda   |  8 ++++----
 .../DomainTheory/Presentation/Presentation.lagda | 16 ++++++++++------
 2 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
index 1d1d13b40..291797793 100644
--- a/source/DomainTheory/Presentation/C-Ideal.lagda
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -12,7 +12,7 @@ open import UF.Subsingletons-FunExt
 module DomainTheory.Presentation.C-Ideal
         (pt : propositional-truncations-exist)
         (fe : Fun-Ext)
-        {𝓤 𝓥 𝓦 : Universe}
+        {𝓤 𝓣 𝓥 𝓦 : Universe}
        where
 
 open import UF.Powerset
@@ -22,11 +22,11 @@ open PosetAxioms
 
 open import DomainTheory.Basics.Dcpo pt fe 𝓥
 open import DomainTheory.Basics.Miscelanea pt fe 𝓥
-open import DomainTheory.Presentation.Presentation pt fe {𝓤} {𝓥} {𝓦}
+open import DomainTheory.Presentation.Presentation pt fe {𝓤} {𝓣} {𝓥} {𝓦}
 
 
 -- TODO put this at the right place
-Conjunction : (I : 𝓣' ̇) → (I → Ω 𝓣) → Ω (𝓣 ⊔ 𝓣')
+Conjunction : (I : 𝓤' ̇) → (I → Ω 𝓥') → Ω (𝓤' ⊔ 𝓥')
 Conjunction I ps = (∀ i → ps i holds) , Π-is-prop fe λ _ → holds-is-prop (ps _)
 
 syntax Conjunction I (λ i → p) = ⋀ i ꞉ I , p
@@ -73,7 +73,7 @@ module C-Ideal
     (ℑ , ℑ-is-ideal) ⊑ (𝔍 , 𝔍-is-ideal) = ℑ ⊆ 𝔍
 
   -- The impredicatively generated C-ideal from a set
-  Generated : (𝓣' : Universe) → (G → Ω 𝓥') → C-Idl (𝓤 ⊔ (𝓥 ⁺) ⊔ 𝓦 ⊔ 𝓣 ⊔ 𝓥' ⊔ (𝓣' ⁺))
+  Generated : ∀ 𝓣' → (G → Ω 𝓥') → C-Idl (𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ⊔ 𝓥' ⊔ 𝓣' ⁺)
   Generated 𝓣' S = (λ g → ⋀ ((ℑ , _) , _) ꞉  -- Too messy
     (Σ (ℑ , _) ꞉ C-Idl 𝓣' , S ⊆ ℑ), ℑ g) ,
     intersection-is-C-ideal (pr₁ ∘ pr₁) (pr₂ ∘ pr₁)
diff --git a/source/DomainTheory/Presentation/Presentation.lagda b/source/DomainTheory/Presentation/Presentation.lagda
index a3c5f6a79..61672e9e7 100644
--- a/source/DomainTheory/Presentation/Presentation.lagda
+++ b/source/DomainTheory/Presentation/Presentation.lagda
@@ -11,7 +11,11 @@ open import UF.Subsingletons
 module DomainTheory.Presentation.Presentation
         (pt : propositional-truncations-exist)
         (fe : Fun-Ext)
-        {𝓤 𝓥 𝓦 : Universe}  -- TODO clear universe levels
+        {𝓤 𝓣 𝓥 𝓦 : 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
@@ -26,7 +30,7 @@ module _
   (_≲_ : G → G → 𝓣 ̇)
   where
 
-  Cover-set : 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⁺ ̇
+  Cover-set : 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⁺ ̇ -- This one has spurious assumptions
   Cover-set = G → {I : 𝓥 ̇} → (I → G) → Ω 𝓦
 
   is-dcpo-presentation : Cover-set → 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ̇
@@ -38,11 +42,11 @@ module _
       Cover-directed = {x : G} {I : 𝓥 ̇} {U : I → G} → (x ◃ U) holds
         → is-directed _≲_ U
 
-DCPO-Presentation : {𝓣 : Universe} → (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣)⁺ ̇
-DCPO-Presentation {𝓣} = Σ G ꞉ 𝓤 ̇ , Σ _⊑_ ꞉ (G → G → 𝓣 ̇) ,
+DCPO-Presentation : (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣)⁺ ̇
+DCPO-Presentation = Σ G ꞉ 𝓤 ̇ , Σ _⊑_ ꞉ (G → G → 𝓣 ̇) ,
   Σ _◃_ ꞉ (Cover-set G _⊑_) , (is-dcpo-presentation G _⊑_ _◃_)
 
-module _ (𝓖 : DCPO-Presentation {𝓣}) where
+module _ (𝓖 : DCPO-Presentation) where
   ⟨_⟩ₚ : 𝓤 ̇ -- We need a uniform way to refer to underlying sets
   ⟨_⟩ₚ = 𝓖 .pr₁
 
@@ -53,7 +57,7 @@ module _ (𝓖 : DCPO-Presentation {𝓣}) where
   cover-directed = 𝓖 .pr₂ .pr₂ .pr₂ .pr₂
 
 module Interpretation
-  (𝓖 : DCPO-Presentation {𝓣})
+  (𝓖 : DCPO-Presentation)
   (𝓓 : DCPO {𝓤} {𝓣})
   where  -- Defines maps from a presentation into dcpos
 

From 1b0095437aa0871d0a4c8d6fc65d7fcb22549ba5 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Sat, 25 Feb 2023 16:29:26 +0800
Subject: [PATCH 11/27] WIP Suplattics of C-Ideals

---
 .../DomainTheory/Presentation/C-Ideal.lagda   | 19 +++++++++++++++++++
 source/Posets/FreeSupLattice.lagda            |  2 +-
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
index 291797793..e3a431f26 100644
--- a/source/DomainTheory/Presentation/C-Ideal.lagda
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -16,9 +16,11 @@ module DomainTheory.Presentation.C-Ideal
        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 𝓥
@@ -83,4 +85,21 @@ module C-Ideal
 
   -- Universal property
 
+  -- C-Ideals form a suplattice
+  -- set assumptions not included yet
+  C-Idl-SupLattice : ∀ 𝓣' 𝓦' → SupLattice 𝓦' _ _
+  C-Idl-SupLattice 𝓣' 𝓦' = record {
+      L = C-Idl (𝓤 ⊔ 𝓣 ⊔ (𝓥 ⁺) ⊔ 𝓦 ⊔ (𝓣' ⁺) ⊔ 𝓦') ;
+      L-is-set = _ ;
+      _⊑_ = λ (ℑ , ι) (𝔍 , υ) → ℑ ⊆ 𝔍 ;
+      ⊑-is-prop-valued = _ ;
+      ⊑-is-reflexive = λ _ _ → id ;
+      ⊑-is-transitive = λ _ _ _ ℑ⊆𝔍 𝔍⊆𝔎 u i∈ℑ → 𝔍⊆𝔎 u (ℑ⊆𝔍 u i∈ℑ) ;
+      ⊑-is-antisymmetric = {!   !} ;
+      ⋁ = λ ℑs → Generated 𝓣' λ g →
+        (∃ i ꞉ _ , g ∈ carrier (ℑs i)) , ∃-is-prop ;
+      ⋁-is-upperbound = {!   !} ;
+      ⋁-is-lowerbound-of-upperbounds = {!   !}
+    }
+
 \end{code}
diff --git a/source/Posets/FreeSupLattice.lagda b/source/Posets/FreeSupLattice.lagda
index c5f1f3c1e..7903debb1 100644
--- a/source/Posets/FreeSupLattice.lagda
+++ b/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

From 5137639ee9568718f1e8ca884bb48172b13340f3 Mon Sep 17 00:00:00 2001
From: Jon Sterling <jon@jonmsterling.com>
Date: Sat, 25 Feb 2023 12:19:06 -0500
Subject: [PATCH 12/27] formatting: DomainTheory.Basics.Miscelanea

Only regularizing the formatting of the code we are adding; this file
needs attention/cleanup in a separate PR.
---
 source/DomainTheory/Basics/Miscelanea.lagda | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/source/DomainTheory/Basics/Miscelanea.lagda b/source/DomainTheory/Basics/Miscelanea.lagda
index e090ca833..d3b42c398 100644
--- a/source/DomainTheory/Basics/Miscelanea.lagda
+++ b/source/DomainTheory/Basics/Miscelanea.lagda
@@ -105,11 +105,11 @@ image-is-directed : {D : 𝓤 ̇} {E : 𝓤' ̇}
   → 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)
+ 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 : ⟨ 𝓓 ⟩ → ⟨ 𝓔 ⟩}
@@ -119,7 +119,7 @@ image-is-Directed : (𝓓 : DCPO {𝓤} {𝓣}) (𝓔 : DCPO {𝓤'} {𝓣'})
                   → is-Directed 𝓓 α
                   → is-Directed 𝓔 (f ∘ α)
 image-is-Directed 𝓓 𝓔 m δ =
-  image-is-directed (underlying-order 𝓓) (underlying-order 𝓔) m δ
+ image-is-directed (underlying-order 𝓓) (underlying-order 𝓔) m δ
 
 continuity-criterion : (𝓓 : DCPO {𝓤} {𝓣}) (𝓔 : DCPO {𝓤'} {𝓣'})
                        (f : ⟨ 𝓓 ⟩ → ⟨ 𝓔 ⟩)

From b0e5f90b1269eb8dc934921be4ac29408a508052 Mon Sep 17 00:00:00 2001
From: Jon Sterling <jon@jonmsterling.com>
Date: Sat, 25 Feb 2023 12:26:21 -0500
Subject: [PATCH 13/27] formatting: DomainTheory.Presentation.C-Ideal

---
 .../DomainTheory/Presentation/C-Ideal.lagda   | 80 ++++++++++++-------
 1 file changed, 50 insertions(+), 30 deletions(-)

diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
index e3a431f26..47f2d9019 100644
--- a/source/DomainTheory/Presentation/C-Ideal.lagda
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -10,10 +10,10 @@ open import UF.Subsingletons
 open import UF.Subsingletons-FunExt
 
 module DomainTheory.Presentation.C-Ideal
-        (pt : propositional-truncations-exist)
-        (fe : Fun-Ext)
-        {𝓤 𝓣 𝓥 𝓦 : Universe}
-       where
+  (pt : propositional-truncations-exist)
+  (fe : Fun-Ext)
+  {𝓤 𝓣 𝓥 𝓦 : Universe}
+ where
 
 open import UF.Powerset
 open PropositionalTruncation pt
@@ -29,7 +29,8 @@ open import DomainTheory.Presentation.Presentation pt fe {𝓤} {𝓣} {𝓥} {
 
 -- TODO put this at the right place
 Conjunction : (I : 𝓤' ̇) → (I → Ω 𝓥') → Ω (𝓤' ⊔ 𝓥')
-Conjunction I ps = (∀ i → ps i holds) , Π-is-prop fe λ _ → holds-is-prop (ps _)
+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
 
@@ -49,13 +50,15 @@ module C-Ideal
       → x ∈ ℑ
 
   being-C-ideal-is-prop : (ℑ : G → Ω 𝓣') → is-prop (is-C-ideal ℑ)
-  being-C-ideal-is-prop ℑ = ×-is-prop
+  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
+   : {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)
@@ -65,41 +68,58 @@ module C-Ideal
   C-Idl 𝓣' = Σ (is-C-ideal {𝓣' = 𝓣'})
 
   module _ {𝓣' : Universe} where
-    carrier : C-Idl 𝓣' → G → Ω 𝓣'
-    carrier (ℑ , _) = ℑ
+   carrier : C-Idl 𝓣' → G → Ω 𝓣'
+   carrier (ℑ , _) = ℑ
 
-    C-ideality : (𝓘 : C-Idl 𝓣') → is-C-ideal (carrier 𝓘)
-    C-ideality (_ , ι) = ι
+   C-ideality : (𝓘 : C-Idl 𝓣') → is-C-ideal (carrier 𝓘)
+   C-ideality (_ , ι) = ι
 
-    _⊑_ : C-Idl 𝓣' → C-Idl 𝓣' → 𝓤 ⊔ 𝓣' ̇
-    (ℑ , ℑ-is-ideal) ⊑ (𝔍 , 𝔍-is-ideal) = ℑ ⊆ 𝔍
+   _⊑_ : 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₁)
+   (Σ (ℑ , _) ꞉ 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 𝓦' _ _
-  C-Idl-SupLattice 𝓣' 𝓦' = record {
-      L = C-Idl (𝓤 ⊔ 𝓣 ⊔ (𝓥 ⁺) ⊔ 𝓦 ⊔ (𝓣' ⁺) ⊔ 𝓦') ;
-      L-is-set = _ ;
-      _⊑_ = λ (ℑ , ι) (𝔍 , υ) → ℑ ⊆ 𝔍 ;
-      ⊑-is-prop-valued = _ ;
-      ⊑-is-reflexive = λ _ _ → id ;
-      ⊑-is-transitive = λ _ _ _ ℑ⊆𝔍 𝔍⊆𝔎 u i∈ℑ → 𝔍⊆𝔎 u (ℑ⊆𝔍 u i∈ℑ) ;
-      ⊑-is-antisymmetric = {!   !} ;
-      ⋁ = λ ℑs → Generated 𝓣' λ g →
-        (∃ i ꞉ _ , g ∈ carrier (ℑs i)) , ∃-is-prop ;
-      ⋁-is-upperbound = {!   !} ;
-      ⋁-is-lowerbound-of-upperbounds = {!   !}
-    }
+  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}

From 1962bfc80f8b988b8fe9734abb9a263332c6e9a6 Mon Sep 17 00:00:00 2001
From: Jon Sterling <jon@jonmsterling.com>
Date: Sat, 25 Feb 2023 12:28:28 -0500
Subject: [PATCH 14/27] formatting: DomainTheory.Presentation.Presentation

---
 .../Presentation/Presentation.lagda           | 83 ++++++++++---------
 1 file changed, 42 insertions(+), 41 deletions(-)

diff --git a/source/DomainTheory/Presentation/Presentation.lagda b/source/DomainTheory/Presentation/Presentation.lagda
index 61672e9e7..8941ccf39 100644
--- a/source/DomainTheory/Presentation/Presentation.lagda
+++ b/source/DomainTheory/Presentation/Presentation.lagda
@@ -9,14 +9,14 @@ open import UF.PropTrunc
 open import UF.Subsingletons
 
 module DomainTheory.Presentation.Presentation
-        (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
+  (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
@@ -35,42 +35,43 @@ module _
 
   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
+   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 _⊑_ _◃_)
+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₂
-
-module Interpretation
-  (𝓖 : DCPO-Presentation)
-  (𝓓 : DCPO {𝓤} {𝓣})
-  where  -- Defines maps from a presentation into dcpos
-
-  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))
+ ⟨_⟩ₚ : 𝓤 ̇ -- 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}

From dfe0d79c2dcad0fe962a1fb9bd4179190fef3556 Mon Sep 17 00:00:00 2001
From: Jon Sterling <jon@jonmsterling.com>
Date: Sat, 25 Feb 2023 12:29:05 -0500
Subject: [PATCH 15/27] rename DomainTheory.Presentation.Presentation =>
 DomainTheory.Presentation.Type

---
 .../DomainTheory/Presentation/{Presentation.lagda => Type.lagda}  | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename source/DomainTheory/Presentation/{Presentation.lagda => Type.lagda} (100%)

diff --git a/source/DomainTheory/Presentation/Presentation.lagda b/source/DomainTheory/Presentation/Type.lagda
similarity index 100%
rename from source/DomainTheory/Presentation/Presentation.lagda
rename to source/DomainTheory/Presentation/Type.lagda

From 5bc599601c457f53ae6a5fe15892bc366139d1a6 Mon Sep 17 00:00:00 2001
From: Jon Sterling <jon@jonmsterling.com>
Date: Sat, 25 Feb 2023 12:32:13 -0500
Subject: [PATCH 16/27] fix my mistake (unfinished rename)

---
 source/DomainTheory/Presentation/Type.lagda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/source/DomainTheory/Presentation/Type.lagda b/source/DomainTheory/Presentation/Type.lagda
index 8941ccf39..9ad0ab2bb 100644
--- a/source/DomainTheory/Presentation/Type.lagda
+++ b/source/DomainTheory/Presentation/Type.lagda
@@ -8,7 +8,7 @@ open import UF.FunExt
 open import UF.PropTrunc
 open import UF.Subsingletons
 
-module DomainTheory.Presentation.Presentation
+module DomainTheory.Presentation.Type
   (pt : propositional-truncations-exist)
   (fe : Fun-Ext)
   {𝓤 𝓣 𝓥 𝓦 : Universe}

From 5065a2e61b1b4cd90622d725c51a7ab8f15a4384 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Tue, 28 Feb 2023 21:39:15 +0800
Subject: [PATCH 17/27] Define monotonicity

---
 source/Posets/Poset.lagda | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/source/Posets/Poset.lagda b/source/Posets/Poset.lagda
index ca68abf9c..caee815e0 100644
--- a/source/Posets/Poset.lagda
+++ b/source/Posets/Poset.lagda
@@ -69,3 +69,24 @@ Added 25 August 2022, but added elsewhere in TypeTopology much earlier (June
   posets-are-sets = type-with-prop-valued-refl-antisym-rel-is-set _⊑_
 
 \end{code}
+
+Defines monotone functions.
+
+\begin{code}
+
+ module MonotoneAxioms  -- TODO find occurences of monotonicity and refactor
+         {D : 𝓤 ̇ }
+         (_⊑_ : D → D → 𝓣 ̇ )
+         {E : 𝓤' ̇ }
+         (_≼_ : E → E → 𝓣' ̇ )
+         (f : D → E)
+        where
+
+  is-monotone = ∀ x y → x ⊑ y → f x ≼ f y
+
+  open PosetAxioms _≼_
+
+  being-monotone-is-prop : is-prop-valued → is-prop is-monotone
+  being-monotone-is-prop p = Π₃-is-prop fe λ _ _ _ → p _ _
+
+\end{code}

From d43a6b56ed59243b2a98444cde371a63553eb64c Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Tue, 28 Feb 2023 22:36:00 +0800
Subject: [PATCH 18/27] Closure

---
 source/Posets/Closure.lagda           | 38 +++++++++++++++++++++++++++
 source/Posets/KuratowskiClosure.lagda | 19 ++++++++++++++
 2 files changed, 57 insertions(+)
 create mode 100644 source/Posets/Closure.lagda
 create mode 100644 source/Posets/KuratowskiClosure.lagda

diff --git a/source/Posets/Closure.lagda b/source/Posets/Closure.lagda
new file mode 100644
index 000000000..fdbdb7047
--- /dev/null
+++ b/source/Posets/Closure.lagda
@@ -0,0 +1,38 @@
+We define closure operators on a poset as a monotone increasing function 𝑓
+such that 𝑓(𝑥) ≥ 𝑥 and 𝑓(𝑓(𝑥)) = 𝑓(𝑥).
+
+\begin{code}
+
+{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}
+
+open import MLTT.Spartan
+open import UF.FunExt
+
+open import UF.Subsingletons
+open import UF.Subsingletons-FunExt
+
+module Posets.Closure
+        (fe : Fun-Ext)
+       where
+open import Posets.Poset fe
+
+module Closure
+        {D : 𝓤 ̇ }
+        (_⊑_ : D → D → 𝓣 ̇ )
+        (f : D → D)
+       where
+  closure-η = ∀ x → x ⊑ f x
+  closure-μ = ∀ x → f (f x) ⊑ f x
+
+  open PosetAxioms _⊑_  -- TODO bundle more things
+
+  idempotent
+    : closure-η
+    → closure-μ
+    → is-antisymmetric
+    → ∀ x → f (f x) ＝ f x
+  idempotent η μ a x = a _ _ (μ _) (η _)
+
+
+\end{code}
+
diff --git a/source/Posets/KuratowskiClosure.lagda b/source/Posets/KuratowskiClosure.lagda
new file mode 100644
index 000000000..b74a02629
--- /dev/null
+++ b/source/Posets/KuratowskiClosure.lagda
@@ -0,0 +1,19 @@
+A Kuratowski closure operator is a closure operator that preserves joins.
+
+\begin{code}
+
+{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}
+
+open import MLTT.Spartan
+open import UF.FunExt
+
+open import UF.Subsingletons
+open import UF.Subsingletons-FunExt
+
+module Posets.KuratowskiClosure
+        (fe : Fun-Ext)
+       where
+open import Posets.Poset fe
+open import Posets.Closure fe
+
+\end{code}

From 9eedad1b36c7bf43aab4c85acb1d0198fcd7b9f4 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Wed, 1 Mar 2023 13:22:48 +0800
Subject: [PATCH 19/27] Kuratowski closure

---
 source/Posets/JoinSemiLattices.lagda  |  2 +-
 source/Posets/KuratowskiClosure.lagda | 16 ++++++++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/source/Posets/JoinSemiLattices.lagda b/source/Posets/JoinSemiLattices.lagda
index 7344c2b40..c9131de99 100644
--- a/source/Posets/JoinSemiLattices.lagda
+++ b/source/Posets/JoinSemiLattices.lagda
@@ -16,7 +16,7 @@ open import Fin.Type
 
 open import UF.Subsingletons
 
-record JoinSemiLattice (𝓥 𝓣 : Universe) : 𝓤ω where
+record JoinSemiLattice (𝓥 𝓣 : Universe) : 𝓣 ⁺ ⊔ 𝓥 ⁺ ̇ where
   field
     L : 𝓥 ̇
     L-is-set : is-set L
diff --git a/source/Posets/KuratowskiClosure.lagda b/source/Posets/KuratowskiClosure.lagda
index b74a02629..82f7e67ff 100644
--- a/source/Posets/KuratowskiClosure.lagda
+++ b/source/Posets/KuratowskiClosure.lagda
@@ -10,10 +10,26 @@ open import UF.FunExt
 open import UF.Subsingletons
 open import UF.Subsingletons-FunExt
 
+open import Posets.JoinSemiLattices
+
 module Posets.KuratowskiClosure
         (fe : Fun-Ext)
        where
 open import Posets.Poset fe
 open import Posets.Closure fe
 
+module _ (D : JoinSemiLattice 𝓥 𝓣) where
+  open JoinSemiLattice D
+  open MonotoneAxioms _⊑_ _⊑_
+  open Closure _⊑_
+
+  kuratowski-closure-axioms : (L → L) → _
+  kuratowski-closure-axioms f
+    = is-monotone f
+    × (closure-η f × closure-μ f)
+    × (preserves-⊥ × preserves-∨)
+   where
+    preserves-⊥ = f ⊥ ＝ ⊥
+    preserves-∨ = ∀ x y → f (x ∨ y) ＝ f x ∨ f y
+
 \end{code}

From 8d22030e1c81b90c1c62714780a26c038aab0b08 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 10 Mar 2023 14:08:48 +0800
Subject: [PATCH 20/27] WIP suplattice closure

---
 source/Posets/Closure.lagda | 24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/source/Posets/Closure.lagda b/source/Posets/Closure.lagda
index fdbdb7047..8432f4a41 100644
--- a/source/Posets/Closure.lagda
+++ b/source/Posets/Closure.lagda
@@ -7,12 +7,13 @@ such that 𝑓(𝑥) ≥ 𝑥 and 𝑓(𝑓(𝑥)) = 𝑓(𝑥).
 
 open import MLTT.Spartan
 open import UF.FunExt
-
+open import UF.PropTrunc
 open import UF.Subsingletons
 open import UF.Subsingletons-FunExt
 
 module Posets.Closure
         (fe : Fun-Ext)
+        (pt : propositional-truncations-exist)
        where
 open import Posets.Poset fe
 
@@ -32,7 +33,26 @@ module Closure
     → is-antisymmetric
     → ∀ x → f (f x) ＝ f x
   idempotent η μ a x = a _ _ (μ _) (η _)
+\end{code}
 
 
-\end{code}
+If we have a closure operator on a suplattice, then the image is
+also a suplattice.
+
+\begin{code}
+open import Posets.FreeSupLattice pt
+-- TODO we don't want the "free" part, factor the definition out
+module _ (𝕃 : SupLattice 𝓤 𝓥 𝓦) where
+ open SupLattice 𝕃
+ open Closure _⊑_
+
+ module SupLattice-Closure
+  (f : L → L)
+  (f-is-monotone : ∀ x y → x ⊑ y → f x ⊑ f y)
+  (f-closure-η : closure-η f)
+  (f-closure-μ : closure-μ f) where
 
+  -- To avoid using UA early, image should be
+  -- defined using the universal property
+
+\end{code}

From 605b3165a6746560fe6c7824ca73fe0a07506bff Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 10 Mar 2023 14:23:17 +0800
Subject: [PATCH 21/27] WIP suplattice closure

---
 source/Posets/Closure.lagda | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/source/Posets/Closure.lagda b/source/Posets/Closure.lagda
index 8432f4a41..9b6c22011 100644
--- a/source/Posets/Closure.lagda
+++ b/source/Posets/Closure.lagda
@@ -43,16 +43,18 @@ also a suplattice.
 open import Posets.FreeSupLattice pt
 -- TODO we don't want the "free" part, factor the definition out
 module _ (𝕃 : SupLattice 𝓤 𝓥 𝓦) where
- open SupLattice 𝕃
- open Closure _⊑_
+ module 𝕃 = SupLattice 𝕃
+ open Closure 𝕃._⊑_
 
  module SupLattice-Closure
-  (f : L → L)
-  (f-is-monotone : ∀ x y → x ⊑ y → f x ⊑ f y)
-  (f-closure-η : closure-η f)
-  (f-closure-μ : closure-μ f) where
+  {D : 𝓤 ̇ }
+  (_⊑_ : D → D → 𝓣 ̇ )
+  (f : 𝕃.L → D)
+  (f-is-monotone : ∀ x y → x 𝕃.⊑ y → f x ⊑ f y)
+  (ι : D → 𝕃.L)
+  (ι-is-monotome : ∀ x y → x ⊑ y → ι x 𝕃.⊑ ι y)
+  (ι∘f-closure-η : closure-η (ι ∘ f))
+  (ι∘f-closure-μ : closure-μ (ι ∘ f)) where
 
-  -- To avoid using UA early, image should be
-  -- defined using the universal property
 
 \end{code}

From ed9c6f79b2d8bcd6ae607c193d41e3ff29f42679 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 10 Mar 2023 14:25:14 +0800
Subject: [PATCH 22/27] Fix

---
 source/Posets/Closure.lagda           | 2 +-
 source/Posets/KuratowskiClosure.lagda | 5 +++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/source/Posets/Closure.lagda b/source/Posets/Closure.lagda
index 9b6c22011..534afcaf1 100644
--- a/source/Posets/Closure.lagda
+++ b/source/Posets/Closure.lagda
@@ -43,7 +43,7 @@ also a suplattice.
 open import Posets.FreeSupLattice pt
 -- TODO we don't want the "free" part, factor the definition out
 module _ (𝕃 : SupLattice 𝓤 𝓥 𝓦) where
- module 𝕃 = SupLattice 𝕃
+ private module 𝕃 = SupLattice 𝕃
  open Closure 𝕃._⊑_
 
  module SupLattice-Closure
diff --git a/source/Posets/KuratowskiClosure.lagda b/source/Posets/KuratowskiClosure.lagda
index 82f7e67ff..657ff33ce 100644
--- a/source/Posets/KuratowskiClosure.lagda
+++ b/source/Posets/KuratowskiClosure.lagda
@@ -6,7 +6,7 @@ A Kuratowski closure operator is a closure operator that preserves joins.
 
 open import MLTT.Spartan
 open import UF.FunExt
-
+open import UF.PropTrunc
 open import UF.Subsingletons
 open import UF.Subsingletons-FunExt
 
@@ -14,9 +14,10 @@ open import Posets.JoinSemiLattices
 
 module Posets.KuratowskiClosure
         (fe : Fun-Ext)
+        (pt : propositional-truncations-exist)
        where
 open import Posets.Poset fe
-open import Posets.Closure fe
+open import Posets.Closure fe pt
 
 module _ (D : JoinSemiLattice 𝓥 𝓣) where
   open JoinSemiLattice D

From ada0ae31e3f24c1ffd6306031dcb0fc650fecec1 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Fri, 10 Mar 2023 14:54:21 +0800
Subject: [PATCH 23/27] We don't need set assumptions!

---
 source/DomainTheory/Presentation/C-Ideal.lagda | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
index 47f2d9019..43422b450 100644
--- a/source/DomainTheory/Presentation/C-Ideal.lagda
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -12,9 +12,11 @@ open import UF.Subsingletons-FunExt
 module DomainTheory.Presentation.C-Ideal
   (pt : propositional-truncations-exist)
   (fe : Fun-Ext)
+  (pe : Prop-Ext)
   {𝓤 𝓣 𝓥 𝓦 : Universe}
  where
 
+open import UF.Retracts
 open import UF.Powerset
 open PropositionalTruncation pt
 open import UF.ImageAndSurjection pt
@@ -24,7 +26,7 @@ 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 {𝓤} {𝓣} {𝓥} {𝓦}
+open import DomainTheory.Presentation.Type pt fe {𝓤} {𝓣} {𝓥} {𝓦}
 
 
 -- TODO put this at the right place
@@ -90,19 +92,20 @@ module C-Ideal
   private module SL = SupLattice
 
   -- C-Ideals form a suplattice
-  -- set assumptions not included yet
+  -- TODO clean up fe and pe assumptions
   C-Idl-SupLattice : ∀ 𝓣' 𝓦' → SupLattice 𝓦' _ _
   SL.L (C-Idl-SupLattice 𝓣' 𝓦') =
    C-Idl (𝓤 ⊔ 𝓣 ⊔ (𝓥 ⁺) ⊔ 𝓦 ⊔ (𝓣' ⁺) ⊔ 𝓦')
 
   SL.L-is-set (C-Idl-SupLattice 𝓣' 𝓦') =
-   {!!}
+   Σ-is-set (Π-is-set fe λ _ → Ω-is-set fe pe) λ ℑ →
+    props-are-sets (being-C-ideal-is-prop ℑ)
 
   SL._⊑_ (C-Idl-SupLattice 𝓣' 𝓦') (ℑ , ι) (𝔍 , υ) =
    ℑ ⊆ 𝔍
 
-  SL.⊑-is-prop-valued (C-Idl-SupLattice 𝓣' 𝓦') =
-   {!!}
+  SL.⊑-is-prop-valued (C-Idl-SupLattice 𝓣' 𝓦') _ 𝔍 =
+   Π₂-is-prop fe λ g _ → holds-is-prop (carrier 𝔍 g)
 
   SL.⊑-is-reflexive (C-Idl-SupLattice 𝓣' 𝓦') _ _ =
    id
@@ -117,8 +120,8 @@ module C-Ideal
    Generated 𝓣' λ g →
    (∃ i ꞉ _ , g ∈ carrier (ℑs i)) , ∃-is-prop
 
-  SL.⋁-is-upperbound (C-Idl-SupLattice 𝓣' 𝓦') =
-   {!!}
+  SL.⋁-is-upperbound (C-Idl-SupLattice 𝓣' 𝓦') ℑ i g g∈ℑi ((𝔍 , _ , _) , ℑ'⊆𝔍) =
+   ℑ'⊆𝔍 g ∣ i , g∈ℑi ∣
 
   SL.⋁-is-lowerbound-of-upperbounds (C-Idl-SupLattice 𝓣' 𝓦') =
    {!!}

From 4673b63f2bd16827ccceb10263f9ba9d84dcf1f0 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Sun, 19 Mar 2023 19:07:27 +0800
Subject: [PATCH 24/27] Fill in some holes

---
 .../DomainTheory/Presentation/C-Ideal.lagda   | 23 +++++++++++++------
 1 file changed, 16 insertions(+), 7 deletions(-)

diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
index 43422b450..dca911ced 100644
--- a/source/DomainTheory/Presentation/C-Ideal.lagda
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -4,6 +4,7 @@
 {-# OPTIONS --without-K --exact-split --safe --auto-inline #-}
 open import MLTT.Spartan hiding (J)
 
+open import UF.Base
 open import UF.FunExt
 open import UF.PropTrunc
 open import UF.Subsingletons
@@ -77,7 +78,12 @@ module C-Ideal
    C-ideality (_ , ι) = ι
 
    _⊑_ : C-Idl 𝓣' → C-Idl 𝓣' → 𝓤 ⊔ 𝓣' ̇
-   (ℑ , ℑ-is-ideal) ⊑ (𝔍 , 𝔍-is-ideal) = ℑ ⊆ 𝔍
+   (ℑ , _) ⊑ (𝔍 , _) = ℑ ⊆ 𝔍
+
+  -- Characterize the equality of C-ideals
+  to-C-ideal-＝ : (I J : C-Idl 𝓣') → carrier I ＝ carrier J → I ＝ J
+  to-C-ideal-＝ (ℑ , _) (𝔍 , υ) p = to-Σ-＝
+   (p , being-C-ideal-is-prop 𝔍 _ _)
 
   -- The impredicatively generated C-ideal from a set
   Generated : ∀ 𝓣' → (G → Ω 𝓥') → C-Idl (𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ⊔ 𝓥' ⊔ 𝓣' ⁺)
@@ -113,16 +119,19 @@ module C-Ideal
   SL.⊑-is-transitive (C-Idl-SupLattice 𝓣' 𝓦') _ _ _ ℑ⊆𝔍 𝔍⊆𝔎 u i∈ℑ =
    𝔍⊆𝔎 u (ℑ⊆𝔍 u i∈ℑ)
 
-  SL.⊑-is-antisymmetric (C-Idl-SupLattice 𝓣' 𝓦') =
-   {!!}
+  SL.⊑-is-antisymmetric (C-Idl-SupLattice 𝓣' 𝓦') (ℑ , ι) (𝔍 , υ) ℑ⊆𝔍 𝔍⊆ℑ =
+   to-C-ideal-＝ _ _ (dfunext fe (λ g → to-Σ-＝
+    (pe (pr₂ (ℑ g)) (pr₂ (𝔍 g)) (ℑ⊆𝔍 g) (𝔍⊆ℑ g) ,
+     being-prop-is-prop fe _ _)))
+      -- This needs to-Ω-＝ somewhere in the library
 
   SL.⋁ (C-Idl-SupLattice 𝓣' 𝓦') ℑs =
    Generated 𝓣' λ g →
    (∃ i ꞉ _ , g ∈ carrier (ℑs i)) , ∃-is-prop
 
-  SL.⋁-is-upperbound (C-Idl-SupLattice 𝓣' 𝓦') ℑ i g g∈ℑi ((𝔍 , _ , _) , ℑ'⊆𝔍) =
-   ℑ'⊆𝔍 g ∣ i , g∈ℑi ∣
+  SL.⋁-is-upperbound (C-Idl-SupLattice 𝓣' 𝓦') I i g g∈Ii ((𝔍 , _ , _) , ℑ⊆𝔍) =
+   ℑ⊆𝔍 g ∣ i , g∈Ii ∣
 
-  SL.⋁-is-lowerbound-of-upperbounds (C-Idl-SupLattice 𝓣' 𝓦') =
-   {!!}
+  SL.⋁-is-lowerbound-of-upperbounds (C-Idl-SupLattice 𝓣' 𝓦') = {!   !}
+    -- This is not correct for universe reasons
 \end{code}

From d0989b716eec5629a07af847f4e6948240bc014c Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Wed, 12 Apr 2023 19:11:16 +0800
Subject: [PATCH 25/27] Expose the resizing

---
 source/DomainTheory/Presentation/C-Ideal.lagda | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
index dca911ced..e5e2cd993 100644
--- a/source/DomainTheory/Presentation/C-Ideal.lagda
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -132,6 +132,19 @@ module C-Ideal
   SL.⋁-is-upperbound (C-Idl-SupLattice 𝓣' 𝓦') I i g g∈Ii ((𝔍 , _ , _) , ℑ⊆𝔍) =
    ℑ⊆𝔍 g ∣ i , g∈Ii ∣
 
-  SL.⋁-is-lowerbound-of-upperbounds (C-Idl-SupLattice 𝓣' 𝓦') = {!   !}
-    -- This is not correct for universe reasons
+  SL.⋁-is-lowerbound-of-upperbounds (C-Idl-SupLattice 𝓣' 𝓦')
+    I (𝔍 , υ) Ii⊆𝔍 g g∈SupI = 𝔍'→𝔍 g (g∈SupI ((𝔍' , υ') ,
+      λ g → ∥∥-rec (holds-is-prop (𝔍' g)) λ (i , e) → 𝔍→𝔍' g (Ii⊆𝔍 i g e)))
+      where
+        𝔍' : G → Ω 𝓣'
+        𝔍' = {!   !}  -- requires resizing
+
+        𝔍'→𝔍 : ∀ g → 𝔍' g holds → 𝔍 g holds
+        𝔍'→𝔍 = {!   !}
+
+        𝔍→𝔍' : ∀ g → 𝔍 g holds → 𝔍' g holds
+        𝔍→𝔍' = {!   !}
+
+        υ' : is-C-ideal 𝔍'
+        υ' = {!   !}  -- deducible from propositional equivalence
 \end{code}

From 40f2df13ff87b2ecd0c55dc2fb10ba5d5d57152c Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Tue, 18 Jul 2023 18:08:38 +0800
Subject: [PATCH 26/27] Singleton map

---
 source/DomainTheory/Presentation/C-Ideal.lagda | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
index e5e2cd993..a7d8dd3d0 100644
--- a/source/DomainTheory/Presentation/C-Ideal.lagda
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -23,7 +23,7 @@ open PropositionalTruncation pt
 open import UF.ImageAndSurjection pt
 open import Posets.Poset fe
 open PosetAxioms
-open import Posets.FreeSupLattice pt
+open import Posets.FreeSupLattice pt using (SupLattice)
 
 open import DomainTheory.Basics.Dcpo pt fe 𝓥
 open import DomainTheory.Basics.Miscelanea pt fe 𝓥
@@ -39,6 +39,7 @@ syntax Conjunction I (λ i → p) = ⋀ i ꞉ I , p
 
 module C-Ideal
   (G : 𝓤 ̇)
+  (G-is-set : is-set G)
   (_≲_ : G → G → 𝓣 ̇)
   (_◃_ : Cover-set G _≲_)
  where
@@ -147,4 +148,12 @@ module C-Ideal
 
         υ' : is-C-ideal 𝔍'
         υ' = {!   !}  -- deducible from propositional equivalence
+
+  -- The map from G to C-Idl
+  η : G → C-Idl (𝓤 ⊔ 𝓣 ⊔ (𝓥 ⁺) ⊔ 𝓦 ⊔ (𝓣' ⁺))
+  η {𝓣' = 𝓣'} g = Generated {𝓥' = 𝓤} 𝓣' λ g' → (g ＝ g') , G-is-set
+
+  -- Every map from G to a suplattice S preserving covers
+  -- factors uniquely through C-Idl
+
 \end{code}

From c4f34949d603ed5b4dbdd44178425589eb361ab5 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <2300936257@qq.com>
Date: Wed, 19 Jul 2023 00:56:47 +0800
Subject: [PATCH 27/27] eta is monotone

---
 .../DomainTheory/Presentation/C-Ideal.lagda   | 29 ++++++++++++++-----
 1 file changed, 22 insertions(+), 7 deletions(-)

diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
index a7d8dd3d0..d550cae9e 100644
--- a/source/DomainTheory/Presentation/C-Ideal.lagda
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -39,7 +39,6 @@ syntax Conjunction I (λ i → p) = ⋀ i ꞉ I , p
 
 module C-Ideal
   (G : 𝓤 ̇)
-  (G-is-set : is-set G)
   (_≲_ : G → G → 𝓣 ̇)
   (_◃_ : Cover-set G _≲_)
  where
@@ -48,7 +47,7 @@ module C-Ideal
   is-C-ideal ℑ = downward-closed × cover-closed
    where
     downward-closed = ∀ x y → x ≲ y
-      → x ∈ ℑ → y ∈ ℑ
+      → y ∈ ℑ → x ∈ ℑ
     cover-closed = ∀ I x (U : I → G) → (x ◃ U) holds
       → (∀ y → y ∈image U → y ∈ ℑ)
       → x ∈ ℑ
@@ -149,11 +148,27 @@ module C-Ideal
         υ' : is-C-ideal 𝔍'
         υ' = {!   !}  -- deducible from propositional equivalence
 
-  -- The map from G to C-Idl
-  η : G → C-Idl (𝓤 ⊔ 𝓣 ⊔ (𝓥 ⁺) ⊔ 𝓦 ⊔ (𝓣' ⁺))
-  η {𝓣' = 𝓣'} g = Generated {𝓥' = 𝓤} 𝓣' λ g' → (g ＝ g') , G-is-set
+  module _ (G-is-set : is-set G) where
+    -- The map from G to C-Idl
+    η : ∀ 𝓣' → G → C-Idl (𝓤 ⊔ 𝓣 ⊔ (𝓥 ⁺) ⊔ 𝓦 ⊔ (𝓣' ⁺))
+    η 𝓣' g = Generated 𝓣' λ g' → (g ＝ g') , G-is-set
 
-  -- Every map from G to a suplattice S preserving covers
-  -- factors uniquely through C-Idl
+    -- it is monotone
+    η-is-monotone : ∀ g g' → g ≲ g'
+      → carrier (η 𝓣' g) ⊆ carrier (η 𝓣' g')
+    η-is-monotone {𝓣' = 𝓣'} g g' g≲g' h h∈ηg ((𝔍 , υ) , ⟨g'⟩⊆𝔍)
+      = h∈ηg ((𝔍 , υ) , λ { .g refl → g∈𝔍 })
+      where
+        g'∈𝔍 : g' ∈ 𝔍
+        g'∈𝔍 = ⟨g'⟩⊆𝔍 g' refl
+
+        g∈𝔍 : g ∈ 𝔍
+        g∈𝔍 = υ .pr₁ g g' g≲g' g'∈𝔍
+
+    -- it preserves covers
+    open Interpretation
+
+    -- Every monotone map from G to a suplattice S preserving covers
+    -- factors uniquely through η
 
 \end{code}