A simpler definition of Dyn?

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 {

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