diff --git a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda
index 95c2236589822be13434eb7638884a0dd6ad43ed..29f7841b5feca84de8d6ad2f99eb9407dffd4bd5 100644
--- a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda
+++ b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda
@@ -66,17 +66,8 @@ record Model â„“ â„“' â„“'' : Type (â„“-suc (â„“-max â„“ (â„“-max â„“' â„“'')))
     -- now the dyn stuff
     -- a model of dyn/casts
     dyn : cat .ob
-    -- type precision
-    _⊑_ : (cat .ob) → (cat .ob) → Type ℓ''
-    isReflexive⊑  : ∀ {a} → a ⊑ a
-    isTransitive⊑ : ∀ {a b c} → a ⊑ b → b ⊑ c → a ⊑ c
-    isProp⊑ : ∀ {a b} → isProp (a ⊑ b)
-
-    -- monotonicity of type constructors
-    prod-is-monotone : ∀ {a a' b b'} → a ⊑ a' → b ⊑ b' → (a × b) ⊑ (a' × b')
-    parfun-is-monotone : ∀ {a a' b b'} → a ⊑ a' → b ⊑ b' → (a ⇀ b) ⊑ (a' ⇀ b')
-    inj-nat : nat ⊑ dyn
-    inj-arr : (dyn ⇀ dyn) ⊑ dyn
-
-    up : ∀ {a b} → a ⊑ b → cat [ a , b ]
-    dn : ∀ {a b} → a ⊑ b → cat [ b , T ⟅ a ⟆ ]
+
+    -- at this point we will model injection and projection as
+    -- arbitrary morphisms
+    inj : cat [ nat + (dyn ⇀ dyn) , dyn ]
+    prj : cat [ dyn , T ⟅ nat + (dyn ⇀ dyn) ⟆ ]