diff --git a/formalizations/guarded-cubical/Semantics/Concrete/DynNew.agda b/formalizations/guarded-cubical/Semantics/Concrete/DynNew.agda
new file mode 100644
index 0000000000000000000000000000000000000000..da210598f7012b88cf323705ea9dae1550dd90df
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Concrete/DynNew.agda
@@ -0,0 +1,202 @@
+{-# OPTIONS --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+{-# OPTIONS --lossy-unification #-}
+
+
+
+open import Common.Later
+
+module Semantics.Concrete.DynNew (k : Clock) where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Univalence
+
+open import Cubical.Relation.Binary
+open import Cubical.Data.Nat renaming (ℕ to Nat)
+open import Cubical.Data.Sum
+open import Cubical.Data.Unit
+open import Cubical.Data.Empty
+
+open import Common.LaterProperties
+--open import Common.Preorder.Base
+--open import Common.Preorder.Monotone
+--open import Common.Preorder.Constructions
+open import Semantics.Lift k
+-- open import Semantics.Concrete.LiftPreorder k
+
+open import Cubical.Relation.Binary.Poset
+open import Common.Poset.Convenience
+open import Common.Poset.Constructions
+open import Common.Poset.Monotone
+open import Semantics.MonotoneCombinators
+
+open import Semantics.LockStepErrorOrdering k
+
+open BinaryRelation
+open LiftPoset
+open ClockedCombinators k
+
+private
+ variable
+ ℓ ℓ' : Level
+
+ ▹_ : Type ℓ → Type ℓ
+ ▹_ A = ▹_,_ k A
+
+
+-- Can have type Poset ℓ ℓ
+DynP' : (D : ▹ Poset ℓ-zero ℓ-zero) -> Poset ℓ-zero ℓ-zero
+DynP' D = ℕ ⊎p (▸' k (λ t → D t ==> 𝕃 (D t)))
+
+DynP : Poset ℓ-zero ℓ-zero
+DynP = fix DynP'
+
+unfold-DynP : DynP ≡ DynP' (next DynP)
+unfold-DynP = fix-eq DynP'
+
+unfold-⟨DynP⟩ : ⟨ DynP ⟩ ≡ ⟨ DynP' (next DynP) ⟩
+unfold-⟨DynP⟩ = λ i → ⟨ unfold-DynP i ⟩
+
+DynP-Sum : DynP ≡ ℕ ⊎p ((▸'' k) (DynP ==> 𝕃 DynP))
+DynP-Sum = unfold-DynP
+
+
+
+InjNat : ⟨ ℕ ==> DynP ⟩
+InjNat = mCompU (mTransport (sym DynP-Sum)) σ1
+
+InjArr : ⟨ (DynP ==> 𝕃 DynP) ==> DynP ⟩
+InjArr = mCompU (mTransport (sym DynP-Sum)) (mCompU σ2 Next)
+
+ProjNat : ⟨ DynP ==> 𝕃 ℕ ⟩
+ProjNat = mCompU (Case' mRet (K _ ℧)) (mTransport DynP-Sum)
+
+ProjArr : ⟨ DynP ==> 𝕃 (DynP ==> 𝕃 DynP) ⟩
+ProjArr = {!!}
+
+
+
+
+{-
+
+
+data Dyn' (D : ▹ Poset ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
+ nat : Nat -> Dyn' D
+ fun : ▸ (λ t → MonFun (D t) (𝕃 (D t))) -> Dyn' D
+
+Dyn'-iso : (D : ▹ Poset ℓ ℓ') -> Iso (Dyn' D) (Nat ⊎ (▸ (λ t → MonFun (D t) (𝕃 (D t)))))
+Dyn'-iso D = iso
+ (λ { (nat n) → inl n ; (fun f~) → inr f~})
+ (λ { (inl n) → nat n ; (inr f~) → fun f~})
+ (λ { (inl n) → refl ; (inr f~) → refl})
+ (λ { (nat x) → refl ; (fun x) → refl})
+
+
+DynP' :
+ (D : ▹ Poset ℓ-zero ℓ-zero) -> Poset ℓ-zero ℓ-zero
+DynP' D = Dyn' D ,
+ posetstr order
+ (isposet isSetDynP' dyn-ord-prop dyn-ord-refl dyn-ord-trans dyn-ord-antisym)
+ where
+ order : Dyn' D → Dyn' D → Type
+ order (nat n) (nat m) = (n ≡ m)
+ order (fun f~) (fun g~) = ▸ λ t → (f~ t) ≤mon (g~ t)
+ order _ _ = ⊥
+
+ isSetDynP' : isSet (Dyn' D)
+ isSetDynP' = isSetRetract
+ (Iso.fun (Dyn'-iso D)) (Iso.inv (Dyn'-iso D)) (Iso.leftInv (Dyn'-iso D))
+ (isSet⊎ isSetℕ (isSet▸ λ t -> MonFunIsSet))
+
+ dyn-ord-refl : isRefl order
+ dyn-ord-refl (nat n) = refl
+ dyn-ord-refl (fun f~) = λ t → ≤mon-refl (f~ t)
+
+ dyn-ord-prop : isPropValued order
+ dyn-ord-prop (nat n) (nat m) = isSetℕ n m
+ dyn-ord-prop (fun f~) (fun g~) = isProp▸ (λ t -> ≤mon-prop (f~ t) (g~ t))
+
+ dyn-ord-trans : isTrans order
+ dyn-ord-trans (nat n1) (nat n2) (nat n3) n1≡n2 n2≡n3 =
+ n1≡n2 ∙ n2≡n3
+ dyn-ord-trans (fun f1~) (fun f2~) (fun f3~) H1 H2 =
+ λ t → ≤mon-trans (f1~ t) (f2~ t) (f3~ t) (H1 t) (H2 t)
+
+ dyn-ord-antisym : isAntisym order
+ dyn-ord-antisym (nat n) (nat m) n≡m m≡n = cong nat n≡m
+ dyn-ord-antisym (fun f~) (fun g~) d≤d' d'≤d =
+ cong fun (eq▸ f~ g~ λ t -> ≤mon-antisym (f~ t) (g~ t) (d≤d' t) (d'≤d t))
+
+
+DynP : Poset ℓ-zero ℓ-zero
+DynP = fix DynP'
+
+unfold-DynP : DynP ≡ DynP' (next DynP)
+unfold-DynP = fix-eq DynP'
+
+unfold-⟨DynP⟩ : ⟨ DynP ⟩ ≡ ⟨ DynP' (next DynP) ⟩
+unfold-⟨DynP⟩ = λ i → ⟨ unfold-DynP i ⟩
+
+unfold-DynP-rel : PathP (λ i -> {!lift (unfold-⟨DynP⟩ i)!}) (rel DynP) (rel (DynP' (next DynP)))
+unfold-DynP-rel = {!!}
+
+
+-- Converting from the underlying set of DynP' to the underlying
+-- set of DynP
+DynP'→DynP : ⟨ DynP' (next DynP) ⟩ -> ⟨ DynP ⟩
+DynP'→DynP d = transport (sym (λ i -> ⟨ unfold-DynP i ⟩)) d
+
+DynP→DynP' : ⟨ DynP ⟩ -> ⟨ DynP' (next DynP) ⟩
+DynP→DynP' d = transport (λ i → ⟨ unfold-DynP i ⟩) d
+
+
+rel-DynP'→rel-DynP : ∀ d1 d2 ->
+ rel (DynP' (next DynP)) d1 d2 ->
+ rel DynP (DynP'→DynP d1) (DynP'→DynP d2)
+rel-DynP'→rel-DynP d1 d2 d1≤d2 = transport
+ (λ i → rel (unfold-DynP (~ i))
+ (transport-filler (λ j → ⟨ unfold-DynP (~ j) ⟩) d1 i)
+ (transport-filler (λ j → ⟨ unfold-DynP (~ j) ⟩) d2 i))
+ d1≤d2
+
+rel-DynP→rel-DynP' : ∀ d1 d2 ->
+ rel DynP d1 d2 ->
+ rel (DynP' (next DynP)) (DynP→DynP' d1) (DynP→DynP' d2)
+rel-DynP→rel-DynP' d1 d2 d1≤d2 = transport
+ (λ i → rel (unfold-DynP i)
+ (transport-filler (λ j -> ⟨ unfold-DynP j ⟩) d1 i)
+ (transport-filler (λ j -> ⟨ unfold-DynP j ⟩) d2 i))
+ d1≤d2
+
+DynP-equiv : PosetEquiv DynP (DynP' (next DynP))
+DynP-equiv = pathToEquiv unfold-⟨DynP⟩ ,
+ makeIsPosetEquiv (pathToEquiv unfold-⟨DynP⟩)
+ (λ d1 d2 d1≤d2 -> rel-DynP→rel-DynP' d1 d2 d1≤d2)
+ (λ d1 d2 d1≤d2 -> {!rel-DynP'→rel-DynP d1 d2 d1≤d2!})
+
+
+
+
+
+InjNat : ⟨ ℕ ==> DynP ⟩
+InjNat = record {
+ f = λ n -> DynP'→DynP (nat n) ;
+ isMon = λ {n} {m} n≡m ->
+ rel-DynP'→rel-DynP (nat n) (nat m) n≡m }
+
+
+InjArr : ⟨ (DynP ==> 𝕃 DynP) ==> DynP ⟩
+InjArr = record {
+ f = λ f -> DynP'→DynP (fun (next f)) ;
+ isMon = λ {f1} {f2} f1≤f2 ->
+ rel-DynP'→rel-DynP (fun (next f1)) (fun (next f2)) λ t -> f1≤f2 }
+
+
+-}