diff --git a/formalizations/guarded-cubical/Results/Delay.agda b/formalizations/guarded-cubical/Results/Delay.agda
deleted file mode 100644
index a2f1f1acc6d4df5bbb39504e635c7ea076035759..0000000000000000000000000000000000000000
--- a/formalizations/guarded-cubical/Results/Delay.agda
+++ /dev/null
@@ -1,513 +0,0 @@
-{-# OPTIONS --cubical --rewriting --guarded #-}
-{-# OPTIONS --guardedness #-}
-{-# OPTIONS -W noUnsupportedIndexedMatch #-}
-
- -- to allow opening this module in other files while there are still holes
-{-# OPTIONS --allow-unsolved-metas #-}
-
-
-open import Common.Later
-open import Common.Common
-
-module Results.Delay where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Function
-open import Cubical.Data.Sum
-open import Cubical.Data.Unit renaming (Unit to ⊤)
-open import Cubical.Data.Sigma
-open import Cubical.Data.Nat renaming (ℕ to Nat) hiding (_·_ ; _^_)
-open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Structure
-open import Cubical.Data.Empty as ⊥
-open import Cubical.Relation.Nullary
-open import Cubical.Foundations.Path
-open import Cubical.Relation.Binary.Poset
-
-import Cubical.Data.Equality as Eq
-
-open import Semantics.Predomains
-open import Semantics.StrongBisimulation
-open import Semantics.Lift
-
-open import Results.IntensionalAdequacy
-
-open import Cubical.Foundations.HLevels
-
-
-private
-  variable
-    â„“ : Level
-    X : Type â„“
-
-
-record Delay (Res : Type â„“) : Type â„“
-
-data State (Res : Type â„“) : Type â„“ where
-  done : Res -> State Res  -- should rename result to done
-  running : Delay Res -> State Res
-  -- squash : isSet (State Res)
-
-record Delay Res where
-  coinductive
-  field view : State Res
-
-
-open Delay public
-
-
-delayUnit : State X → Delay X
-view (delayUnit s) = s
-
--- The delay that returns the given value of type X in one step.
-doneD : X -> Delay X
-doneD x = delayUnit (done x)
-
-
--- Given a delay d, returns the delay d' that takes runs for one step
--- and then behaves as d.
-stepD : Delay X -> Delay X
-stepD d = delayUnit (running d)
-
-_↓_#_ : Delay X -> X -> Nat -> Type
-d ↓ x # n = {!!}
-
-
--- Given a delay d, return a function on nats n that,
--- when d ≡ running ^ n (done x), maps n to x and every other number to undefined
-toFun : Delay X -> (Nat -> (X ⊎ Unit))
-toFun d zero with view d
-... | done x = inl x
-... | running x = inr _
-toFun d (suc n) with view d
-... | done x = inr _
-... | running d' = toFun d' n
-
--- Given a function f on nats, return a delay that runs for n0 steps and returns x,
--- where n0 is the smallest nat such that f n0 = inl x
-fromFun : {X : Type ℓ} -> (Nat -> (X ⊎ Unit)) -> Delay X
-fromFun {X = X} f .view with f 0
-... | inl x = done x
-... | inr _ = running (fromFun (f ∘ suc))
-
-retrFun : (d : Delay X) -> fromFun (toFun d) ≡ d
-retrFun d i .view with d .view in eq
-... | done x = done x
-... | running d' = running (goal _ eq i)
-  where
-    goal : ∀ s -> s Eq.≡ running d' -> fromFun (toFun (delayUnit s) ∘ suc) ≡ d'
-    goal .(running d') Eq.refl = retrFun d'
-
-   
-isSetDelay : isSet X -> isSet (Delay X)
-isSetDelay H = isSetRetract toFun fromFun retrFun (isSetΠ λ _ -> isSet⊎ H isSetUnit)
-
-
-isSetDelay' : ∀ {ℓ : Level} -> {X : Type ℓ} → isSet X → isSet (Delay X)
-isSetDelay' {X = X} p = isSetRetract f g h (isSetΠ λ n → isSet⊎ p isSetUnit)
-    where
-      -- f : Delay X → (Nat → X ⊎ Unit)
-      -- f d zero with d .view
-      -- ... | done x = inl x
-      -- ... | running x = {!inr tt!}
-      -- f d (suc n) with d .view
-      -- ... | done x = inr tt
-      -- ... | running d' = f d' n
-      
-      f : Delay X → (Nat → X ⊎ Unit)
-      f d n with d .view
---      f d n       | done x  = inl x
-      f d zero    | done x = inl x
-      f d (suc n) | done x = inr tt
-      f d zero    | running _ = inr tt
-      f d (suc n) | running d' = f d' n
-
-      g : (Nat → X ⊎ Unit) → Delay X
-      g f .view with f zero
-      ... | inl x  = done x
-      ... | inr tt = running (g λ n → f (suc n))
-
-      h : (d : Delay X) → g (f d) ≡ d
-      h d i .view with d .view
-      ... | done x  = done x
-      ... | running d' = running (h d' i)
-
-
-
-data Result (X : Type) : Type where
-  value : X -> Result X
-  error : Result X
-
-ResToSum : Result X -> X ⊎ Unit
-ResToSum (value x) = inl x
-ResToSum error = inr tt
-
-SumToRes : X ⊎ Unit -> Result X
-SumToRes (inl x) = value x
-SumToRes (inr tt) = error
-
-result-retr : (x : Result X) → SumToRes (ResToSum x) ≡ x
-result-retr (value x) = refl
-result-retr error = refl
-
-isSetResult : isSet X -> isSet (Result X)
-isSetResult H = isSetRetract ResToSum SumToRes result-retr (isSet⊎ H isSetUnit)
-
-_^? : Type -> Type
-X ^? = Result X
-
-
-diag : (Res Run : Type) -> State X -> Typeâ‚€
-diag Res Run (done x) = Res
-diag Res Run (running m) = Run
-
-
-result≠running : {X : Type} -> ∀ {x : X} {m : Delay X} {ℓ} {Whatever : Type ℓ} →
-  done x ≡ running m → Whatever
-result≠running eq = ⊥.rec (transport (cong (diag ⊤ ⊥) eq) tt)
-
-
-
--- used for showing that the result constructor is injective
-pred' : X -> State X → X
-pred' _ (done x) = x
-pred' x (running m) = x
-
--- used for showing that the running constructor is injective
-pred'' : State X -> Delay X
-view (pred'' (done x)) = done x
-pred'' (running m) = m
-
-result-inj : {ℓ : Level} {X : Type ℓ} {x y : X} -> done x ≡ done y -> x ≡ y
-result-inj {x = x} eq = cong′ (pred' x) eq
-
-
-
-
-{-
-module Isomorphism {X : Type} where
-
-  -- to : L℧F X -> Delay (Result (□ X))
-  -- to l = to' (Iso.fun L℧F-iso l)
-
-  to' : (((□ X) ⊎ ⊤) ⊎ (L℧F X)) -> Delay (Result (□ X))
-  view (to' (inl (inl x))) = done (value x)
-  view (to' (inl (inr tt))) = done error
-  view (to' (inr l')) = running (to' (inr l'))
-
-  to : L℧F X -> Delay (Result (□ X))
-  to l = to' (Iso.fun L℧F-iso l)
-
-  fro' : (k : Clock) -> â–¹ k ,
-    (Delay (Result (□ X)) -> L℧ k X) ->
-    (Delay (Result (□ X)) -> L℧ k X)
-  fro' k rec m with (view m)
-  ... | done (value x) = η (x k)
-  ... | done error = ℧
-  ... | running m' = θ (λ t -> rec t m')
-
-  fro : Delay (Result (□ X)) -> L℧F X
-  fro d k = fix (fro' k) d
-
-  unfold-fro : (d : Delay (Result (â–¡ X))) (k : Clock) ->
-    fro d k ≡ fro' k (next (λ d -> fro d k)) d
-  unfold-fro d k = let eq = fix-eq (fro' k) in
-    λ i -> eq i d
-
-
-  sec : section to fro
-  sec d = {!!}
-
-
-  retr' : (k : Clock) -> (l : L℧F X) -> ▹ k ,
-    (fro' k (next (λ d -> fro d k)) (to' (Iso.fun L℧F-iso l)) ≡ l k) ->
-    (fro' k (next (λ d -> fro d k)) (to' (Iso.fun L℧F-iso l)) ≡ l k)
-  retr' k l IH with (Iso.fun L℧F-iso l) in eq
-  ... | inl (inl x) = let eq' = L℧F-iso-η-inv l x {!!} in {!!}
-  ... | inl (inr tt) = let eq' = {!L℧F-iso-inv-℧!} in {!!}
-  ... | inr l' = {!!}
-
-  retr : retract to fro
-  retr l with (Iso.fun L℧F-iso l) in eq
-  ... | inl (inl x) = {!!}
-  ... | inl (inr tt) =
-    {!!} ≡⟨ funExt (λ k -> unfold-fro (to' (inl (inr tt))) k) ⟩
-    {!!} ≡⟨ {!!} ⟩ {!!}
-    l ∎ 
-  ... | inr l' = {!!} 
-
-
-
-module Isomorphism2 {X : Type} where
-
-  to' : (k : Clock) -> L℧ k X -> Delay (Result (□ X))
-  view (to' k (η x)) = done (value (λ k -> x))
-  view (to' k ℧) = done error
-  view (to' k (θ x)) = running (to' k (x ◇))
-
-  to : L℧F X -> Delay (Result (□ X))
-  to l = to' k0 (l k0)
-
-  
-
--- TODO should X have type Clock -> Type?
--- Then the correct iso would be
--- L℧F X ≅ Delay (∀ k -> X k)
-module Isom {X : Type} (H-irrel : clock-irrel X) where
-
-   X? = Result X
-
-   ∀-to-delay : (L℧F X) -> Delay (Result X)
-   view (∀-to-delay l) with (Iso.fun (L℧F-iso-irrel H-irrel) l)
-   ... | inl (inl x) = done (value x)
-   ... | inl (inr tt) = done error
-   ... | inr l' = running (∀-to-delay l')
-
-
-   delay-to-∀'' : (k : Clock) -> ▹ k , (Delay X? -> L℧ k X) -> (Delay X? -> L℧ k X)
-   delay-to-∀'' k rec m with (view m)
-   ... | done (value x) = η x
-   ... | done error = ℧
-   ... | running m' = θ (λ t → rec t m')
-
-   delay-to-∀' : (k : Clock) -> (Delay X?) -> L℧ k X
-   delay-to-∀' k = fix (delay-to-∀'' k)
-
-   unfold-d2∀ : (k : Clock) -> delay-to-∀' k ≡ delay-to-∀'' k (next (delay-to-∀' k))
-   unfold-d2∀ k = fix-eq (delay-to-∀'' k)
-
-   delay-to-∀ : Delay X? -> L℧F X
-   delay-to-∀ m k = fix (delay-to-∀'' k) m
-
-   sec : section ∀-to-delay delay-to-∀
-   sec b = {!!}
-
-   retr : retract ∀-to-delay delay-to-∀
-   retr l with (Iso.fun (L℧F-iso-irrel H-irrel) l)
-   ... | inl (inl x) = clock-ext (λ k → {!!})
-   ... | inl (inr _) = {!!}
-   ... | inr x = {!!}
-
-
-  -- Showing these are inverses requires a notion of equality for Delays,
-  -- which is the bisimilarity relation defined below.
-
--}
-
-
-
-
-
-
-module IsSet (X : Type) (isSetX : isSet X)  where
-
-  X? : Type
-  X? = Result X
-
-  ≡-stable  : {m m' : Delay X?} → Stable (m ≡ m')
-  ≡'-stable : {s s' : State X?} → Stable (s ≡ s')
-
-  view (≡-stable ¬¬p i) = ≡'-stable (λ ¬p → ¬¬p (λ p → ¬p (cong view p))) i
-  
-  ≡'-stable {done x}  {done y}  ¬¬p' =
-    cong′ done {!!}
-  ≡'-stable {running m} {running m'}  ¬¬p' =
-    cong′ running (≡-stable (λ ¬p -> ¬¬p' (λ p -> ¬p (cong pred'' p))))
-  ≡'-stable {done x}  {running m} ¬¬p' = ⊥.rec (¬¬p' (result≠running {X?}))
-  ≡'-stable {running m} {done x}  ¬¬p' = ⊥.rec (¬¬p' (λ p → result≠running {X?} (sym p)))
-
-  retrState : State X? -> X? ⊎ Delay X?
-  retrState (done x) = inl x
-  retrState (running d) = inr d
-
-  secState : X? ⊎ Delay X? -> State X?
-  secState (inl x) = done x
-  secState (inr d) = running d
-  
-
-
-
---  isSetState = isSetRetract retrState secState {!!} (isSet⊎ (isSetResult isSetX) isSetDelay)
-
-
--- Lock-step bisimilarity relation on Delays, but with no error ordering.
-module StrongBisim (X : Type) where -- (H-irrel : clock-irrel ⟨ X ⟩) where
-
-
-  -- Mutually define coinductive bisimilarity of delays
-  -- along with the relation on states of a delay.
- 
-
-  -- Coinductive lock-step bisimilarity on delays
-  record _≈_ (m m' : Delay X) : Type
-
-  -- Bisimilarity on states
-  _≈'_ : State X -> State X -> Type
-  done x ≈' done x' = x ≡ x' -- rel X x x' × rel X x' x
-  running m ≈' running m' = m ≈ m' -- using the coinductive bisimilarity on delays
-  _ ≈' _ = ⊥
-
-  data _≈''_ : State X -> State X -> Type where
-    con : {s s' : State X} -> (s ≈' s') -> (s ≈'' s')
-
-
-  record _≈_ m m' where
-    coinductive
-    field prove : view m ≈'' view m'
-
-
-  open _≈_ public
-
-  enc : {d d' : Delay X} -> d ≡ d' -> d ≈ d'
-  enc' : {s s' : State X} -> s ≡ s' -> s ≈'' s'
-
-  enc {d} {d'} eq .prove = enc' (cong view eq)
-  enc' {done x} {done y} eq = con (result-inj eq)
-  enc' {done x} {running d'} eq = result≠running eq
-  enc' {running d} {done y} eq = result≠running (sym eq)
-  enc' {running d} {running d'} eq = con (enc (cong pred'' eq))
-
-  dec : {d d' : Delay X} -> d ≈ d' -> d ≡ d'
-  dec' : {s s' : State X} -> s ≈'' s' -> s ≡ s'
-
-  view (dec {d} {d'} eq i) = dec' (eq .prove) i
-  dec' {done x} {done x₁} (con p) = cong done p
-  dec' {done x} {running x₁} (con ())
-  dec' {running x} {done x₁} (con ())
-  dec' {running x} {running x₁} (con x₂) = cong running (dec x₂)
-
-
-  {-
-  iso1 : ∀ {m m'} -> (p : m ≈ m') -> enc (dec p) ≡ p
-  iso1' : ∀ {s s'} -> (p : s ≈'' s') -> enc' (dec' p) ≡ p
-  -}
-
-  {-
-  iso2 : ∀ {m m'} -> (p : m ≡ m') -> dec (enc p) ≡ p
-  iso2' : ∀ {s s'} -> (p : s ≡ s') -> dec' (enc' p) ≡ p
-
-  view (iso2 p i j) = iso2' (cong view p) i j
-  
-  iso2' {done x} {done y} p = λ i j → {!!}
-  iso2' {done x} {running d'} p = {!!}
-  iso2' {running d} {done y} p = {!!}
-  iso2' {running m} {running m'} p i j = {!!}
-  -}
-
-{-
-
-  bisim : ∀ {m m'} -> m ≈ m' -> m ≡ m'
-  bisim' : ∀ {m m'} -> m ≈' m' -> m ≡ m'
-
-  -- bisim' {result x} {result y} (con (xRy , yRx)) = cong result (antisym X x y xRy yRx)
-  bisim' {done x} {done y} (con p) = cong done p
-  bisim' {running m} {running m'} (con m≈m') = cong running (bisim m≈m')
-
-  view (bisim m≈m' i) = bisim' (prove m≈m') i
-
-  misib : ∀ {m m'} → m ≡ m' → m ≈ m'
-  misib' : ∀ {m m'} → m ≡ m' → m ≈' m'
-
-  misib' {done x} {done y} eq = con (result-inj eq)
-  misib' {running m} {running m'} p = con (misib (cong pred'' p))
-  misib' {done x} {running m} = result≠running {X}
-  misib' {running m} {done x} eq = result≠running {X} (sym eq)
-
-  prove (misib m≡m') = misib' (cong view m≡m')
-
-  iso1 : ∀ {m m'} -> (p : m ≈ m') -> misib (bisim p) ≡ p
-  iso1' : ∀ {s s'} -> (p : s ≈' s') -> misib' (bisim' p) ≡ p
-
-  iso1' {done x} {done y} (con p) = refl
-  iso1' {running m} {running m'} (con p) = cong con (iso1 p)
-
-  prove (iso1 p i) = iso1' (prove p) i
-
-
-  iso2 : ∀ {m m'} -> (p : m ≡ m') -> bisim (misib p) ≡ p
-  iso2' : ∀ {s s'} -> (p : s ≡ s') -> bisim' (misib' p) ≡ p
-
-  iso2' {running m} {running m'} p = {!!}
-  iso2' _ = {!!}
-
-  iso2 = {!!}
-
-
-module Evaluate {â„“ : Level} (X : Type â„“) where
-
-  _↓_ : Delay X -> X -> Type ℓ
-  d ↓ x = X
-
-
-module WeakBisim {â„“ â„“' : Level}
-  (X : Type â„“) (Y : Type â„“') (R : X -> Y -> Type (â„“-max â„“ â„“')) where
-  module EvX = Evaluate X
-  module EvY = Evaluate Y
-  _↓X_ = EvX._↓_
-  _↓Y_ = EvY._↓_
-
-   -- Coinductive lock-step bisimilarity on delays
-  record _≈_ (d : Delay X) (d' : Delay Y) : Type (ℓ-suc (ℓ-max ℓ ℓ'))
-
-  -- Bisimilarity on states
-  {- _≈''_ : State X -> State Y -> Type -}
-
-  -- Inductive type of proofs of bisimilarity
-  data _≈'_ : (s : State X) (s' : State Y) -> Type (ℓ-suc (ℓ-max ℓ ℓ'))
-   where
-    -- con : s ≈'' s' -> s ≈' s'
-    done-done : ∀ x y -> R x y -> done x ≈' done y
-    done-run : ∀ x y d' -> d' ↓Y y -> R x y -> done x ≈' running d'
-    run-done : ∀ x y d -> d ↓X x -> R x y -> running d ≈' done y
-    run-run : ∀ d d' -> d ≈ d' -> running d ≈' running d'
-
-  record _≈_ m m' where
-    coinductive
-    field prove : view m ≈' view m'
-
-
--- Ret and Ext for Delays
-ret-delay : {X : Type} -> X -> Delay X
-ret-delay = doneD
-
-ext-delay : {X Y : Type} -> (X -> Delay Y) -> Delay X -> Delay Y
-ext-state : {X Y : Type} -> (X -> State Y) -> State X -> State Y
-
-view (ext-delay f mx) = ext-state (view ∘ f) (view mx)
-
-ext-state f (done x) = f x
-ext-state f (running m) = running (ext-delay (delay ∘ f) m)
-
--}
-
-
-{-
-∀-to-delay : (L℧F X) -> (Delay (X ⊎ ⊤))
-view (∀-to-delay l) with (l k0)
-... | η x   = inl (inl x)  -- done (inl x) }
-... | ℧     = inl (inr tt) -- done (inr tt) }
-... | θ lx~ = inr (tt , (∀-to-delay l)) -- running }
-
-{-# TERMINATING #-}
-delay-to-∀ : Delay (X ⊎ ⊤) -> L℧F X
-delay-to-∀ m with (view m)
-... | inl (inl x) = λ k -> η x
-... | inl (inr tt) = λ k -> ℧
-... | inr (tt , m') = λ k -> θ λ t → delay-to-∀ m' k
-
-isom : {X : Type} -> Iso (L℧F X) (Delay (X ⊎ ⊤))
-isom {X} = iso ∀-to-delay delay-to-∀ sec retr
-  where
-    sec : section ∀-to-delay delay-to-∀
-    sec m with (view m)
-    ... | inl (inl x) = {!!}
-    ... | inl (inr tt) = {!!}
-    ... | inr (_ , m') = {!!}
-
-    retr : retract ∀-to-delay delay-to-∀
-    retr l with (l k0) in eq
-    ... | η x = clock-ext {!!}
-    ... | ℧ = clock-ext {!!}
-    ... | θ l~ = {!!}
-   
--}
diff --git a/formalizations/guarded-cubical/Semantics/Delay.agda b/formalizations/guarded-cubical/Semantics/Delay.agda
new file mode 100644
index 0000000000000000000000000000000000000000..d6c855d9bbcaacaf31f7070f045b34d1f4128222
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Delay.agda
@@ -0,0 +1,291 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+{-# OPTIONS --guardedness #-}
+{-# OPTIONS -W noUnsupportedIndexedMatch #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+
+open import Common.Later
+open import Common.Common
+
+module Semantics.Delay where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Data.Sum
+open import Cubical.Data.Unit renaming (Unit to ⊤)
+open import Cubical.Data.Sigma
+open import Cubical.Data.Nat -- renaming (ℕ to Nat) hiding (_·_ ; _^_)
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Structure
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Relation.Nullary
+open import Cubical.Foundations.Path
+open import Cubical.Relation.Binary.Poset
+
+import Cubical.Data.Equality as Eq
+
+open import Semantics.Predomains hiding (â„•)
+open import Semantics.StrongBisimulation
+open import Semantics.Lift
+
+open import Results.IntensionalAdequacy
+
+open import Cubical.Foundations.HLevels
+
+
+private
+  variable
+    â„“ : Level
+    X : Type â„“
+
+
+record Delay (Res : Type â„“) : Type â„“
+
+data State (Res : Type â„“) : Type â„“ where
+  done : Res -> State Res
+  running : Delay Res -> State Res
+
+record Delay Res where
+  coinductive
+  field view : State Res
+
+open Delay public
+
+
+fromState : State X → Delay X
+view (fromState s) = s
+
+-- The delay that returns the given value of type X in one step.
+doneD : X -> Delay X
+doneD x = fromState (done x)
+
+
+-- Given a delay d, returns the delay d' that takes runs for one step
+-- and then behaves as d.
+stepD : Delay X -> Delay X
+stepD d = fromState (running d)
+
+
+-- An alternative definition of the Delay type using functions from natural numbers
+-- to X ⊎ Unit
+module Alternative (X : Type â„“) where
+
+  -- Given a delay d, return a function on nats that, when d ≡ running ^ n (done x),
+  -- maps n to x and every other number to undefined.
+  fromDelay : Delay X → (ℕ → X ⊎ Unit)
+  fromDelay d n with d .view
+--      f d n       | done x  = inl x
+  fromDelay d zero    | done x = inl x
+  fromDelay d (suc n) | done x = inr tt
+  fromDelay d zero    | running _ = inr tt
+  fromDelay d (suc n) | running d' = fromDelay d' n
+
+  -- Given a function f on nats, return a delay that runs for n0 steps and returns x,
+  -- where n0 is the smallest nat such that f n0 = inl x.
+  toDelay : (ℕ → X ⊎ Unit) → Delay X
+  toDelay f .view with f zero
+  ... | inl x  = done x
+  ... | inr tt = running (toDelay λ n → f (suc n))
+
+  retr : (d : Delay X) → toDelay (fromDelay d) ≡ d
+  retr d i .view with d .view
+  ... | done x  = done x
+  ... | running d' = running (retr d' i)
+
+
+  PreDelay' : Type â„“
+  PreDelay' = ℕ -> (X ⊎ Unit)
+
+  Delay' : Type â„“
+  Delay' = Σ[ f ∈ PreDelay' ] fromDelay (toDelay f) ≡ f
+
+  terminatesWith : PreDelay' -> X -> Type â„“
+  terminatesWith d x = Σ[ n ∈ ℕ ] d n ≡ inl x
+
+  terminates : PreDelay' -> Type â„“
+  terminates d = Σ[ n ∈ ℕ ] Σ[ x ∈ X ] d n ≡ inl x
+
+  -- We can characterize the functions f for which fromDelay (toDelay f) ≡ f
+  -- These are the functions that are defined at most once, i.e.,
+  -- if f n ≡ inl x and f m ≡ inl x', then n ≡ m
+
+
+  -- Iso with global lift
+
+  f' : (∀ k -> L k X) -> PreDelay'
+  f' y n with y k0
+  f' y zero    | η x = inl x
+  f' y (suc n) | η x = inr tt
+  f' y zero    | θ l~ = inr tt
+  f' y (suc n) | θ l~ = f' y n
+
+  f : (∀ k -> L k X) -> Delay'
+  f y = (f' y) , {!!}
+
+  g'' : (k : Clock) -> (â–¹ k , (Delay' -> L k X)) -> Delay' -> L k X
+  g'' k rec h with fst h zero
+  ... | inl x = η x
+  ... | inr tt = θ (λ t → rec t ((λ n -> fst h (suc n)) , {!!}))
+
+  g' : ∀ k -> Delay' -> L k X
+  g' k = fix (g'' k)
+
+  g : Delay' -> (∀ k -> L k X)
+  g h k = g' k h
+
+  sec' : (h : Delay') -> (k : Clock) ->
+    (▹ k , (f (λ k' -> g'' k' (next (g' k')) h) ≡ h)) ->
+           (f (λ k' -> g'' k' (next (g' k')) h) ≡ h)
+  sec' h k IH with fst h zero in eq
+  ... | inl x = Σ≡Prop {!!} aux
+    where
+      aux : f' (λ k' -> η x) ≡ h .fst
+      aux = funExt λ { zero → sym (Eq.eqToPath eq) ; (suc n) → {!!}}
+  ... | inr x = Σ≡Prop {!!} {!!}
+  
+
+  unfold-g' : {k : Clock} -> g' k ≡ g'' k (next (g' k))
+  unfold-g' {k} = fix-eq (g'' k)
+
+  sec : section f g
+  sec = {!!}
+
+
+isSetDelay : ∀ {ℓ : Level} -> {X : Type ℓ} → isSet X → isSet (Delay X)
+isSetDelay {X = X} p = isSetRetract fromDelay toDelay retr (isSetΠ λ n → isSet⊎ p isSetUnit)
+  where open Alternative X
+
+
+
+
+
+
+data Result (X : Type) : Type where
+  value : X -> Result X
+  error : Result X
+
+ResToSum : Result X -> X ⊎ Unit
+ResToSum (value x) = inl x
+ResToSum error = inr tt
+
+SumToRes : X ⊎ Unit -> Result X
+SumToRes (inl x) = value x
+SumToRes (inr tt) = error
+
+result-retr : (x : Result X) → SumToRes (ResToSum x) ≡ x
+result-retr (value x) = refl
+result-retr error = refl
+
+isSetResult : isSet X -> isSet (Result X)
+isSetResult H = isSetRetract ResToSum SumToRes result-retr (isSet⊎ H isSetUnit)
+
+_^? : Type -> Type
+X ^? = Result X
+
+
+diag : (Res Run : Type) -> State X -> Typeâ‚€
+diag Res Run (done x) = Res
+diag Res Run (running m) = Run
+
+
+result≠running : {X : Type} -> ∀ {x : X} {m : Delay X} {ℓ} {Whatever : Type ℓ} →
+  done x ≡ running m → Whatever
+result≠running eq = ⊥.rec (transport (cong (diag ⊤ ⊥) eq) tt)
+
+
+
+-- used for showing that the result constructor is injective
+pred' : X -> State X → X
+pred' _ (done x) = x
+pred' x (running m) = x
+
+-- used for showing that the running constructor is injective
+pred'' : State X -> Delay X
+view (pred'' (done x)) = done x
+pred'' (running m) = m
+
+result-inj : {ℓ : Level} {X : Type ℓ} {x y : X} -> done x ≡ done y -> x ≡ y
+result-inj {x = x} eq = cong′ (pred' x) eq
+
+
+
+
+module IsSet (X : Type) (isSetX : isSet X)  where
+
+  X? : Type
+  X? = Result X
+
+  ≡-stable  : {m m' : Delay X?} → Stable (m ≡ m')
+  ≡'-stable : {s s' : State X?} → Stable (s ≡ s')
+
+  view (≡-stable ¬¬p i) = ≡'-stable (λ ¬p → ¬¬p (λ p → ¬p (cong view p))) i
+  
+  ≡'-stable {done x}  {done y}  ¬¬p' =
+    cong′ done {!!}
+  ≡'-stable {running m} {running m'}  ¬¬p' =
+    cong′ running (≡-stable (λ ¬p -> ¬¬p' (λ p -> ¬p (cong pred'' p))))
+  ≡'-stable {done x}  {running m} ¬¬p' = ⊥.rec (¬¬p' (result≠running {X?}))
+  ≡'-stable {running m} {done x}  ¬¬p' = ⊥.rec (¬¬p' (λ p → result≠running {X?} (sym p)))
+
+  retrState : State X? -> X? ⊎ Delay X?
+  retrState (done x) = inl x
+  retrState (running d) = inr d
+
+  secState : X? ⊎ Delay X? -> State X?
+  secState (inl x) = done x
+  secState (inr d) = running d
+  
+
+
+
+--  isSetState = isSetRetract retrState secState {!!} (isSet⊎ (isSetResult isSetX) isSetDelay)
+
+
+-- Lock-step bisimilarity relation on Delays, but with no error ordering.
+module StrongBisim (X : Type) where -- (H-irrel : clock-irrel ⟨ X ⟩) where
+
+
+  -- Mutually define coinductive bisimilarity of delays
+  -- along with the relation on states of a delay.
+ 
+
+  -- Coinductive lock-step bisimilarity on delays
+  record _≈_ (m m' : Delay X) : Type
+
+  -- Bisimilarity on states
+  _≈'_ : State X -> State X -> Type
+  done x ≈' done x' = x ≡ x' -- rel X x x' × rel X x' x
+  running m ≈' running m' = m ≈ m' -- using the coinductive bisimilarity on delays
+  _ ≈' _ = ⊥
+
+  data _≈''_ : State X -> State X -> Type where
+    con : {s s' : State X} -> (s ≈' s') -> (s ≈'' s')
+
+
+  record _≈_ m m' where
+    coinductive
+    field prove : view m ≈'' view m'
+
+
+  open _≈_ public
+
+  enc : {d d' : Delay X} -> d ≡ d' -> d ≈ d'
+  enc' : {s s' : State X} -> s ≡ s' -> s ≈'' s'
+
+  enc {d} {d'} eq .prove = enc' (cong view eq)
+  enc' {done x} {done y} eq = con (result-inj eq)
+  enc' {done x} {running d'} eq = result≠running eq
+  enc' {running d} {done y} eq = result≠running (sym eq)
+  enc' {running d} {running d'} eq = con (enc (cong pred'' eq))
+
+  dec : {d d' : Delay X} -> d ≈ d' -> d ≡ d'
+  dec' : {s s' : State X} -> s ≈'' s' -> s ≡ s'
+
+  view (dec {d} {d'} eq i) = dec' (eq .prove) i
+  dec' {done x} {done x₁} (con p) = cong done p
+  dec' {done x} {running x₁} (con ())
+  dec' {running x} {done x₁} (con ())
+  dec' {running x} {running x₁} (con x₂) = cong running (dec x₂)
+
diff --git a/formalizations/guarded-cubical/Results/DelayCoalgebra.agda b/formalizations/guarded-cubical/Semantics/DelayCoalgebra.agda
similarity index 77%
rename from formalizations/guarded-cubical/Results/DelayCoalgebra.agda
rename to formalizations/guarded-cubical/Semantics/DelayCoalgebra.agda
index 54cf881195b2730d6e094d20aa84f45fa1504f05..77e7f04cca6b967ff6b2911f1357b102d2dc6aed 100644
--- a/formalizations/guarded-cubical/Results/DelayCoalgebra.agda
+++ b/formalizations/guarded-cubical/Semantics/DelayCoalgebra.agda
@@ -2,7 +2,10 @@
 {-# OPTIONS --guardedness #-}
 {-# OPTIONS -W noUnsupportedIndexedMatch #-}
 
-module Results.DelayCoalgebra where
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module Semantics.DelayCoalgebra where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
@@ -16,7 +19,7 @@ open import Cubical.Foundations.Isomorphism
 
 import Cubical.Data.Equality as Eq
 
-open import Results.Delay
+open import Semantics.Delay
 
 private
   variable
@@ -114,7 +117,7 @@ module _ (X : Type â„“) (isSetX : isSet X)  where
   DelayCoalgFinal : {â„“c : Level} -> (c : Coalg â„“) ->
     isContr (Σ[ h ∈ (c .V -> Delay X) ] unfold-delay ∘ h ≡ liftSum h ∘ c. un) -- isContr (CoalgMorphism c DelayCoalg)
   DelayCoalgFinal c =
-    (fun , (funExt commute)) , {!!}
+    (fun , (funExt commute)) , unique' (fun , (funExt commute))
     where
       
       fun : c .V -> Delay X
@@ -131,8 +134,8 @@ module _ (X : Type â„“) (isSetX : isSet X)  where
       unique' : (s s' : Σ[ h ∈ (c .V → Delay X) ]
                     (unfold-delay ∘ (h) ≡ liftSum h ∘ (c .un))) ->
         s ≡ s'
-      unique' (h , com) (h' , com') = {!!}
-        -- Σ≡Prop (λ g -> isPropΠ (λ v -> {!!})) (funExt eq-fun)
+      unique' (h , com) (h' , com') =
+        Σ≡Prop (λ g -> isSetΠ (λ v -> isSet⊎ isSetX (isSetDelay isSetX)) _ _) (funExt eq-fun)
         where
           eq-fun : (v : c .V) -> h v ≡ h' v
           view (eq-fun v i) with c .un v in eq
@@ -168,47 +171,3 @@ module _ (X : Type â„“) (isSetX : isSet X)  where
                 s1 ≡ s2
               goal .(running (h v')) .(running (h' v')) Eq.refl Eq.refl =
                 cong running (eq-fun v')
-
-             
-
-              
-
-
-{-
-      unique : (s : Σ[ h' ∈ (c .V → Delay X) ] (unfold-delay ∘ h' ≡ liftSum h' ∘ c .un)) →
-        (fun , funExt commute) ≡ s
-      unique (h' , com') = Σ≡Prop (λ g -> isSetΠ (λ v -> isSet⊎ isSetX (isSetDelay isSetX)) _ _) (funExt aux)
-        where
-          -- aux : (v : c .V) → fun v ≡ h' v
-          -- aux v with c .un v
-          -- ... | inl x = λ i -> {!!}
-          -- ... | inr x = {!!}
-
-          aux : (v : c .V) → fun v ≡ h' v
-          view (aux v i) with c. un v in eq
-          ... | inl x =
-            let com-v = funExtS⁻ com' v in
-            let eq' = lem1 (view (h' v)) x
-                        (com-v ∙ λ j -> liftSum h' (Eq.eqToPath eq j)) in
-            sym eq' i
-          ... | inr v' =
-            let com-v = funExtS⁻ com' v in
-            {-let eq' = lem2 (view (h' v)) (fun v')
-                        (com-v ∙ (λ j -> liftSum h' (Eq.eqToPath eq j)) ∙ cong inr (sym (aux v'))) in
-            sym eq' i -}
-            view (goal _ eq {!!})
-              where
-                goal : ∀ w -> w Eq.≡ inr v' -> (fun v') ≡ (h' v')
-                goal w Eq.refl = λ j -> (aux v' j) -- view (aux v')
--}
-
-  --  NTS: liftSum h' (c .un v) ≡ inr (fun v')
-  --  Have : c .un v Eq.≡ inr v'
-  --
-  --  Substituting, NTS:
-  --    liftSum h' (inr v') ≡ inr (fun v')
-  --  i.e.
-  --    inr (h' v') ≡ inr (fun v')
-  --  i.e.
-  --    h' v' ≡ fun v'
-