diff --git a/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/Constructions.agda b/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/Constructions.agda
new file mode 100644
index 0000000000000000000000000000000000000000..33a8a034a829a30ddf797e4386312dc0173bd6a8
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/Constructions.agda
@@ -0,0 +1,40 @@
+{-# OPTIONS --guarded --rewriting #-}
+
+
+module Semantics.Concrete.DoublePoset.Constructions where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Structure
+
+
+open import Semantics.Concrete.DoublePoset.Base
+open import Semantics.Concrete.DoublePoset.Morphism
+
+open import Common.Later
+
+private
+  variable
+    â„“ â„“' : Level
+    â„“X â„“'X â„“''X : Level
+    â„“Y â„“'Y â„“''Y : Level
+
+    X : DoublePoset â„“X â„“'X â„“''X
+    Y : DoublePoset â„“Y â„“'Y â„“''Y
+
+
+-- Constructions not involving later
+
+
+-- Contructions involving later
+module ClockedConstructions (k : Clock) where
+
+  private
+    â–¹_ : Type â„“ -> Type â„“
+    â–¹ A = â–¹_,_ k A
+
+    -- Theta for double posets
+    --DPâ–¸ : ?
+    --DPâ–¸ = ?
+
+