diff --git a/formalizations/guarded-cubical/ErrorDomains.agda b/formalizations/guarded-cubical/ErrorDomains.agda
index 9377ebc7a7a7602b9e6a033a4a5ace50c5eef807..c6a98b74c4bdb7a4af137d181839f515d1281cc0 100644
--- a/formalizations/guarded-cubical/ErrorDomains.agda
+++ b/formalizations/guarded-cubical/ErrorDomains.agda
@@ -348,17 +348,20 @@ data Dyn' (D : â–¹ Type) : Type where
   nat : â„• -> Dyn' D
   arr : ▸ (λ t → D t -> L℧ (D t)) -> Dyn' D
 
+-- Would this Dyn be better?
+data Dyn'' (D : â–¹ Type) : Type where
+  nat : â„• -> Dyn'' D
+  arr : (▸ D -> L℧ (Dyn'' D)) -> Dyn'' D
+
 Dyn : Type
 Dyn = fix Dyn'
 
-
 -- Embedding-projection pairs
 record EP (A B : Set) : Set where
   field
     emb  : A -> B
     proj : B -> L℧ A
 
-
 -- E-P Pair for a type with itself
 EP-id : (A : Type) -> EP A A
 EP-id A = record {
diff --git a/formalizations/guarded-cubical/Later.agda b/formalizations/guarded-cubical/Later.agda
index dba75afd3a0586e47d0286776b69d62033db9a75..9e2368c0d82897741283add29566d98c46663037 100644
--- a/formalizations/guarded-cubical/Later.agda
+++ b/formalizations/guarded-cubical/Later.agda
@@ -31,10 +31,10 @@ private
     k : Clock
 
 ▹_,_ : Clock → Set l → Set l
-▹ k , A = (@tick x : Tick k) → A
+▹ k , A = (@tick t : Tick k) → A
 
 ▸_ : ▹ k , Set l → Set l
-▸ A = (@tick x : Tick _) → A x
+▸ A = (@tick t : Tick _) → A t
 
 next : A → ▹ k , A
 next x _ = x