diff --git a/source/DomainTheory/Basics/Exponential.lagda b/source/DomainTheory/Basics/Exponential.lagda
index 89f664e3c..2aea8e020 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 21aead04b..92af33865 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
@@ -244,10 +253,10 @@ id-is-monotone 𝓓 x y l = l
 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) δ)
+  γ : (I : 𝓥 ̇ ) (α : I → ⟨ 𝓓 ⟩) (δ : is-Directed 𝓓 α)
+    → ∐ 𝓓 δ ⊑⟨ 𝓓 ⟩ ∐ 𝓓 (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 : ⟨ 𝓔 ⟩ → ⟨ 𝓔' ⟩)
@@ -262,15 +271,15 @@ id-is-continuous 𝓓 = continuity-criterion 𝓓 𝓓 id (id-is-monotone 𝓓)
   mg = monotone-if-continuous 𝓔 𝓔' (g , cg)
   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 δ)
+  ψ : (I : 𝓥 ̇ ) (α : I → ⟨ 𝓓 ⟩) (δ : is-Directed 𝓓 α)
+    → 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 0bb0fd711..baa6e11a3 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⦆ ]
diff --git a/source/DomainTheory/Presentation/C-Ideal.lagda b/source/DomainTheory/Presentation/C-Ideal.lagda
new file mode 100644
index 000000000..d550cae9e
--- /dev/null
+++ b/source/DomainTheory/Presentation/C-Ideal.lagda
@@ -0,0 +1,174 @@
+
+
+\begin{code}
+{-# 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
+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
+open import Posets.Poset fe
+open PosetAxioms
+open import Posets.FreeSupLattice pt using (SupLattice)
+
+open import DomainTheory.Basics.Dcpo pt fe 𝓥
+open import DomainTheory.Basics.Miscelanea pt fe 𝓥
+open import DomainTheory.Presentation.Type 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
+      → y ∈ ℑ → x ∈ ℑ
+    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 𝓣' → 𝓤 ⊔ 𝓣' ̇
+   (ℑ , _) ⊑ (𝔍 , _) = ℑ ⊆ 𝔍
+
+  -- 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 (𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⊔ 𝓣 ⊔ 𝓥' ⊔ 𝓣' ⁺)
+  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
+  -- 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 𝓣' 𝓦') _ 𝔍 =
+   Π₂-is-prop fe λ g _ → holds-is-prop (carrier 𝔍 g)
+
+  SL.⊑-is-reflexive (C-Idl-SupLattice 𝓣' 𝓦') _ _ =
+   id
+
+  SL.⊑-is-transitive (C-Idl-SupLattice 𝓣' 𝓦') _ _ _ ℑ⊆𝔍 𝔍⊆𝔎 u i∈ℑ =
+   𝔍⊆𝔎 u (ℑ⊆𝔍 u i∈ℑ)
+
+  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 i g g∈Ii ((𝔍 , _ , _) , ℑ⊆𝔍) =
+   ℑ⊆𝔍 g ∣ i , g∈Ii ∣
+
+  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
+
+  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
+
+    -- 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}
diff --git a/source/DomainTheory/Presentation/Type.lagda b/source/DomainTheory/Presentation/Type.lagda
new file mode 100644
index 000000000..9ad0ab2bb
--- /dev/null
+++ b/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}
diff --git a/source/Posets/Closure.lagda b/source/Posets/Closure.lagda
new file mode 100644
index 000000000..534afcaf1
--- /dev/null
+++ b/source/Posets/Closure.lagda
@@ -0,0 +1,60 @@
+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.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
+
+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}
+
+
+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
+ private module 𝕃 = SupLattice 𝕃
+ open Closure 𝕃._⊑_
+
+ module SupLattice-Closure
+  {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
+
+
+\end{code}
diff --git a/source/Posets/FreeSupLattice.lagda b/source/Posets/FreeSupLattice.lagda
index 57d6bb6c3..d6a38faf1 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
diff --git a/source/Posets/JoinSemiLattices.lagda b/source/Posets/JoinSemiLattices.lagda
index ed3f373e6..6164c6b4f 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
new file mode 100644
index 000000000..657ff33ce
--- /dev/null
+++ b/source/Posets/KuratowskiClosure.lagda
@@ -0,0 +1,36 @@
+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.PropTrunc
+open import UF.Subsingletons
+open import UF.Subsingletons-FunExt
+
+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 pt
+
+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}
diff --git a/source/Posets/Poset.lagda b/source/Posets/Poset.lagda
index 847bad27f..3cecf20d2 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}