diff --git a/formalizations/guarded-cubical/GradualSTLC.agda b/formalizations/guarded-cubical/GradualSTLC.agda
index 2afe1cd95ffceda995dbe9bbf513a9b4ab941be2..1c83416b29c765bf916392438729d7ac889ac1ff 100644
--- a/formalizations/guarded-cubical/GradualSTLC.agda
+++ b/formalizations/guarded-cubical/GradualSTLC.agda
@@ -36,6 +36,33 @@ data _⊑_ : Ty -> Ty -> Set where
 ⊑ref dyn = dyn
 ⊑ref (A1 => A2) = (⊑ref A1) => (⊑ref A2)
 
+⊑comp : {A B C : Ty} ->
+  A ⊑ B -> B ⊑ C -> A ⊑ C
+⊑comp dyn dyn = dyn
+⊑comp {Ai => Ao} {Bi => Bo} {Ci => Co} (cin => cout) (din => dout) =
+  (⊑comp cin din) => (⊑comp cout dout)
+⊑comp {Ai => Ao} {Bi => Bo} (cin => cout) (inj-arrow (cin' => cout')) =
+  inj-arrow ((⊑comp cin cin') => (⊑comp cout cout'))
+⊑comp nat nat = nat
+⊑comp nat inj-nat = inj-nat
+⊑comp inj-nat dyn = inj-nat
+⊑comp (inj-arrow c) dyn = inj-arrow c
+
+{-
+ltdyn-transitive {A => B} {A' => B'} {A'' => B''} {n} {m} {p}
+  eq (_=>_ {eq = eq1} dAA' dBB') (_=>_ {eq = eq2} dA'A'' dB'B'') =
+  _=>_ {n = {!?!}} {m = {!!}} {p = {!!}} {eq = {!!}}
+    (ltdyn-transitive {!!} dAA' dA'A'')
+    (ltdyn-transitive {!!} dBB' dB'B'')
+ltdyn-transitive eq (dAA' => dBB') (inj-arrow dBC) = {!!}
+ltdyn-transitive _ nat nat = nat
+ltdyn-transitive _ nat inj-nat = inj-nat
+ltdyn-transitive _ inj-nat dyn = inj-nat
+ltdyn-transitive eq (inj-arrow dA-dyn-dyn) dyn =
+  inj-arrow (ltdyn-transitive _ dA-dyn-dyn (dyn => dyn))
+
+-}
+
 {-
 data ltdyn : â„• -> Ty -> Ty -> Set where
   dyn : {n : â„•} -> ltdyn n dyn dyn
@@ -258,3 +285,14 @@ data Value : ∀ {Γ} {A} -> Tm Γ A -> Set where
     {V : Tm Γ (Bin => Bout)} ->
     Value V ->
     Value (dn (cin => cout) V)
+
+-- Upcasts are values, downcasts are evaluation contexts
+
+{-
+data Value : Type where
+  Zero : {Γ} -> Value
+  Suc : Value -> Value
+-}
+
+
+
diff --git a/formalizations/guarded-cubical/Later.agda b/formalizations/guarded-cubical/Later.agda
index 9e2368c0d82897741283add29566d98c46663037..a074436b709c870621e8b2c24172cdcd9fbae3fe 100644
--- a/formalizations/guarded-cubical/Later.agda
+++ b/formalizations/guarded-cubical/Later.agda
@@ -79,3 +79,70 @@ postulate
 postulate
   force-beta : ∀ {A : Set l} (x : A) → force (λ k _ → x) ≣ λ k → x
 
+
+
+
+
+-- ########################################################## --
+--
+-- Added by Eric (not part of original file from Niccolò Veltri
+-- and Andrea Vezzosi)
+
+
+-- Tick irrelevance axiom. This is needed in the development.
+-- There is likely a better way to do this, see
+-- https://arxiv.org/pdf/2102.01969.pdf (in particular Section 3.2).
+postulate
+  tick-irrelevance : {A : Type} -> (M : â–¹ k , A) (t t' : Tick k) ->
+    M t ≡ M t'
+
+  tr' : {A : Type} -> (M : â–¹ k , A) ->
+    ▸ λ t -> ▸ λ t' -> M t ≡ M t'
+
+{-
+tr→tr' : {M : ▹ k , A} -> tick-irrelevance M -> tr' M
+-}
+
+-- The tick constant.
+postulate
+  _â—‡ : (k : Clock) -> Tick k
+
+-- From Section V.C of Bahr et. al
+-- (See https://bahr.io/pubs/files/bahr17lics-paper.pdf).
+postulate
+  tick-irrelevance-â—‡-refl : {A : Type} -> (M : â–¹ k , A) ->
+    (tick-irrelevance M (k ◇) (k ◇)) ≡ Cubical.Foundations.Everything.refl
+      -- Should this use _≣_.refl instead?
+
+
+-- This relies on tick irrelevance.
+next-Mt≡M : {A : Type} -> (M : ▹ k , A) ->
+  ▸ λ t -> (next (M t) ≡ M)
+next-Mt≡M M t = later-ext (λ t' → tick-irrelevance M t t')
+
+
+next-Mt≡M' : {A : Type} -> (M : ▹ k , A) -> (t : Tick k) ->
+  next (M t) ≡ M
+next-Mt≡M' M t = next-Mt≡M M t
+
+
+
+
+
+-- Clock-related postulates.
+postulate
+  clock-iso : {A : Type} -> (∀ (k : Clock) -> A) ≡ A
+
+postulate
+  k0 : Clock
+
+postulate
+  clock-irrel : {â„“ : Level} -> {A : Type â„“} ->
+    (M : ∀ (k : Clock) -> A) ->
+    (k k' : Clock) ->
+    M k ≡ M k'
+
+
+
+
+
diff --git a/formalizations/guarded-cubical/MonFuns.agda b/formalizations/guarded-cubical/MonFuns.agda
index 93b76822f98f71942f04f4523b3d0c77cb135363..ff86d56ea24886841140e8ccf58155de74aba206 100644
--- a/formalizations/guarded-cubical/MonFuns.agda
+++ b/formalizations/guarded-cubical/MonFuns.agda
@@ -39,16 +39,22 @@ private
 
 open 𝕃
 
-abstract
+-- abstract
 
-  -- Composing monotone functions
-  mComp : {A B C : Predomain} ->
+-- Composing monotone functions
+mCompU : {A B C : Predomain} -> MonFun B C -> MonFun A B -> MonFun A C
+mCompU f1 f2 = record {
+    f = λ a -> f1 .f (f2 .f a) ;
+    isMon = λ x≤y -> f1 .isMon (f2 .isMon x≤y) }
+  where open MonFun
+
+mComp : {A B C : Predomain} ->
     -- MonFun (arr' B C) (arr' (arr' A B) (arr' A C))
     ⟨ (B ==> C) ==> (A ==> B) ==> (A ==> C) ⟩
-  mComp = record {
+mComp = record {
     f = λ fBC →
       record {
-        f = λ fAB → mComp' fBC fAB ;
+        f = λ fAB → mCompU fBC fAB ;
         isMon = λ {f1} {f2} f1≤f2 ->
           λ a1 a2 a1≤a2 → MonFun.isMon fBC (f1≤f2 a1 a2 a1≤a2) } ;
     isMon = λ {f1} {f2} f1≤f2 →
@@ -56,73 +62,105 @@ abstract
         λ a1 a2 a1≤a2 ->
           f1≤f2 (MonFun.f fAB1 a1) (MonFun.f fAB2 a2)
             (fAB1≤fAB2 a1 a2 a1≤a2) }
-    where
-      mComp' : {A B C : Predomain} -> MonFun B C -> MonFun A B -> MonFun A C
-      mComp' f1 f2 = record {
-        f = λ a -> f1 .f (f2 .f a) ;
-        isMon = λ x≤y -> f1 .isMon (f2 .isMon x≤y) }
-        where open MonFun
+     
 
 
   -- 𝕃's return as a monotone function
-  mRet : {A : Predomain} -> ⟨ A ==> 𝕃 A ⟩
-  mRet {A} = record { f = ret ; isMon = ord-η-monotone A }
+mRet : {A : Predomain} -> ⟨ A ==> 𝕃 A ⟩
+mRet {A} = record { f = ret ; isMon = ord-η-monotone A }
 
 
-  -- Extending a monotone function to 𝕃
-  mExt : {A B : Predomain} -> ⟨ (A ==> 𝕃 B) ==> (𝕃 A ==> 𝕃 B) ⟩
-  mExt = record {
-    f = mExt' ;
-    isMon = λ {f1} {f2} f1≤f2  -> ext-monotone (MonFun.f f1) (MonFun.f f2) f1≤f2 }
-    where
-      mExt' : {A B : Predomain} -> MonFun A (𝕃 B) -> MonFun (𝕃 A) (𝕃 B)
-      mExt' f = record {
-        f = λ la -> bind la (MonFun.f f) ;
-        isMon = monotone-bind-mon f }
+  -- Delay as a monotone function
+Δ : {A : Predomain} -> ⟨ 𝕃 A ==> 𝕃 A ⟩
+Δ {A} = record { f = δ ; isMon = λ x≤y → ord-δ-monotone A x≤y }
+
+  -- Lifting a monotone function functorially
+_~->_ : {A B C D : Predomain} ->
+    ⟨ A ==> B ⟩ -> ⟨ C ==> D ⟩ -> ⟨ (B ==> C) ==> (A ==> D) ⟩
+pre ~-> post = {!!}
+  -- λ f -> mCompU post (mCompU f pre)
 
 
+  -- Extending a monotone function to 𝕃
+mExtU : {A B : Predomain} -> MonFun A (𝕃 B) -> MonFun (𝕃 A) (𝕃 B)
+mExtU f = record {
+    f = λ la -> bind la (MonFun.f f) ;
+    isMon = monotone-bind-mon f }
+
+mExt : {A B : Predomain} -> ⟨ (A ==> 𝕃 B) ==> (𝕃 A ==> 𝕃 B) ⟩
+mExt = record {
+    f = mExtU ;
+    isMon = λ {f1} {f2} f1≤f2 -> ext-monotone (MonFun.f f1) (MonFun.f f2) f1≤f2 }
+     
+  -- mBind : ⟨ 𝕃 A ==> (A ==> 𝕃 B) ==> 𝕃 B ⟩
+
   -- Monotone successor function
-  mSuc : ⟨ ℕ ==> ℕ ⟩
-  mSuc = record {
+mSuc : ⟨ ℕ ==> ℕ ⟩
+mSuc = record {
     f = suc ;
     isMon = λ {n1} {n2} n1≤n2 -> λ i -> suc (n1≤n2 i) }
 
 
   -- Combinators
 
-  S : {Γ A B : Predomain} ->
-    ⟨ Γ ==> A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
-  S f g =
+U : {A B : Predomain} -> ⟨ A ==> B ⟩ -> ⟨ A ⟩ -> ⟨ B ⟩
+U f = MonFun.f f
+
+_<$$>_ : {A B : Predomain} -> ⟨ A ==> B ⟩ -> ⟨ A ⟩ -> ⟨ B ⟩
+_<$$>_ = U
+
+S : (Γ : Predomain) -> {A B : Predomain} ->
+    ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+S Γ f g =
     record {
-      f = λ γ -> MonFun.f (MonFun.f f γ) (MonFun.f g γ) ;
-      isMon = λ {γ1} {γ2} γ1≤γ2 →
+      f = λ γ -> MonFun.f f (γ , (U g γ)) ;
+      isMon = λ {γ1} {γ2} γ1≤γ2 ->
+        MonFun.isMon f (γ1≤γ2 , (MonFun.isMon g γ1≤γ2)) }
+
+  {- λ {γ1} {γ2} γ1≤γ2 →
         let fγ1≤fγ2 = MonFun.isMon f γ1≤γ2 in
-          fγ1≤fγ2 (MonFun.f g γ1) (MonFun.f g γ2) (MonFun.isMon g γ1≤γ2) }
+          fγ1≤fγ2 (MonFun.f g γ1) (MonFun.f g γ2) (MonFun.isMon g γ1≤γ2) } -}
 
 
-  _<*>_ : {Γ A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
-  f <*> g = S f g
+_!_<*>_ : {A B : Predomain} ->
+    (Γ : Predomain) -> ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+Γ ! f <*> g = S Γ f g
 
-  infixl 20 _<*>_
+infixl 20 _<*>_
 
 
-  K : {Γ : Predomain} -> {A : Predomain} -> ⟨ A ⟩ -> ⟨ Γ ==> A ⟩
-  K {_} {A} = λ a → record {
+K : (Γ : Predomain) -> {A : Predomain} -> ⟨ A ⟩ -> ⟨ Γ ==> A ⟩
+K _ {A} = λ a → record {
     f = λ γ → a ;
     isMon = λ {a1} {a2} a1≤a2 → reflexive A a }
 
-  Id : {A : Predomain} -> ⟨ A ==> A ⟩
-  Id = record { f = id ; isMon = λ x≤y → x≤y }
 
-  Curry : {Γ A B : Predomain} -> ⟨ (Γ ×d A) ==> B ⟩ -> ⟨ Γ ==> A ==> B ⟩
-  Curry f = record { f = λ γ →
-    record { f = λ a → MonFun.f f (γ , a) ; isMon = {!!} } ; isMon = {!!} }
+Id : {A : Predomain} -> ⟨ A ==> A ⟩
+Id = record { f = id ; isMon = λ x≤y → x≤y }
+
+
+Curry : {Γ A B : Predomain} -> ⟨ (Γ ×d A) ==> B ⟩ -> ⟨ Γ ==> A ==> B ⟩
+Curry f = record {
+    f = λ γ →
+      record {
+        f = λ a → MonFun.f f (γ , a) ;
+        isMon = {!!} } ;
+    isMon = {!!} }
+
+Uncurry : {Γ A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ (Γ ×d A) ==> B ⟩
+Uncurry f = record {
+    f = λ (γ , a) → MonFun.f (MonFun.f f γ) a ;
+    isMon = λ {(γ1 , a1)} {(γ2 , a2)} (γ1≤γ2 , a1≤a2) ->
+      let fγ1≤fγ2 = MonFun.isMon f γ1≤γ2 in
+        fγ1≤fγ2 a1 a2 a1≤a2 }
+
+
+App : {A B : Predomain} -> ⟨ ((A ==> B) ×d A) ==> B ⟩
+App = Uncurry Id
 
-  Uncrry : {Γ A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ (Γ ×d A) ==> B ⟩
-  Uncrry = {!!}
 
-  swap : {Γ A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ A ==> Γ ==> B ⟩
-  swap f = record {
+Swap : (Γ : Predomain) -> {A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ A ==> Γ ==> B ⟩
+Swap Γ f = record {
     f = λ a →
       record {
         f = λ γ → MonFun.f (MonFun.f f γ) a ;
@@ -135,31 +173,88 @@ abstract
 
   -- Convenience versions of comp, ext, and ret using combinators
 
-  mComp' : {Γ A B C : Predomain} ->
-    ⟨ (Γ ==> B ==> C) ⟩ -> ⟨ (Γ ==> A ==> B) ⟩ -> ⟨ (Γ ==> A ==> C) ⟩
-  mComp' f g = (K mComp) <*> f <*> g
+mComp' : (Γ : Predomain) -> {A B C : Predomain} ->
+    ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+mComp' Γ f g = {!!}
+    --_ ! _ ! K Γ mComp <*> f <*> g
+    -- (K Γ mComp) <*> f <*> g
+
+
+_∘m_ : {Γ A B C : Predomain} ->
+   ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+_∘m_ {Γ} = mComp' Γ
+
+_$_∘m_ :  (Γ : Predomain) -> {A B C : Predomain} ->
+    ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+Γ $ f ∘m g = mComp' Γ f g
+infixl 20 _∘m_
+
 
-  _∘m_ :  {Γ A B C : Predomain} ->
-    ⟨ (Γ ==> B ==> C) ⟩ -> ⟨ (Γ ==> A ==> B) ⟩ -> ⟨ (Γ ==> A ==> C) ⟩
-  f ∘m g = mComp' f g
-  infixl 20 _∘m_
+-- Apply a monotone function to the first or second argument of a pair
 
-  mExt' : {Γ A B : Predomain} ->
-    ⟨ (Γ ==> A ==> 𝕃 B) ⟩ -> ⟨ (Γ ==> 𝕃 A ==> 𝕃 B) ⟩
-  mExt' f = K mExt <*> f
+With1st : {Γ A B : Predomain} ->
+    ⟨ Γ ==> B ⟩ -> ⟨ Γ ×d A ==> B ⟩
+-- ArgIntro1 {_} {A} f = Uncurry (Swap A (K A f))
+With1st {_} {A} f = mCompU f π1
 
-  mRet' : {Γ A : Predomain} -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> 𝕃 A ⟩
-  mRet' a = K mRet <*> a
+With2nd : {Γ A B : Predomain} ->
+    ⟨ A ==> B ⟩ -> ⟨ Γ ×d A ==> B ⟩
+With2nd f = mCompU f π2
+-- ArgIntro2 {Γ} f = Uncurry (K Γ f)
 
+{-
+Cong2nd : {Γ A A' B : Predomain} ->
+    ⟨ Γ ×d A ==> B ⟩ -> ⟨ A' ==> A ⟩ -> ⟨ Γ ×d A' ==> B ⟩
+Cong2nd = {!!}
+-}
 
-  -- Mapping a monotone function
-  mMap : {A B : Predomain} -> ⟨ (A ==> B) ==> (𝕃 A ==> 𝕃 B) ⟩
-  mMap = {!!} -- mExt' (mComp' (Curry {!!}) {!!}) -- mExt (mComp mRet f)
 
 
-  mMap' : {Γ A B : Predomain} ->
-    ⟨ (Γ ==> A ==> B) ⟩ -> ⟨ (Γ ==> 𝕃 A ==> 𝕃 B) ⟩
-  mMap' = {!!}
+IntroArg : {Γ B B' : Predomain} ->
+    ⟨ Γ ==> B ⟩ -> ⟨ B ==> B' ⟩ -> ⟨ Γ ==> B' ⟩
+IntroArg {Γ} {B} {B'} fΓB fBB' = S Γ (With2nd fBB') fΓB
+-- S : ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+
+
+TransformDomain : {Γ A A' B : Predomain} ->
+    ⟨ Γ ×d A ==> B ⟩ ->
+    ⟨ ( A ==> B ) ==> ( A' ==> B ) ⟩ ->
+    ⟨ Γ ×d A' ==> B ⟩
+TransformDomain f1 f2 = Uncurry (IntroArg (Curry f1) f2)
+
+
+mExt' : (Γ : Predomain) -> {A B : Predomain} ->
+    ⟨ (Γ ×d A ==> 𝕃 B) ⟩ -> ⟨ (Γ ×d 𝕃 A ==> 𝕃 B) ⟩
+mExt' Γ f = TransformDomain f mExt
+
+mRet' : (Γ : Predomain) -> { A : Predomain} -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> 𝕃 A ⟩
+mRet' Γ a = {!!} -- _ ! K _ mRet <*> a
+
+Bind : (Γ : Predomain) -> {A B : Predomain} ->
+    ⟨ Γ ==> 𝕃 A ⟩ -> ⟨ Γ ×d A ==> 𝕃 B ⟩ -> ⟨ Γ ==> 𝕃 B ⟩
+Bind Γ la f = S Γ (mExt' Γ f) la
+
+Comp : (Γ : Predomain) -> {A B C : Predomain} ->
+    ⟨ Γ ×d B ==> C ⟩ -> ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ×d A ==> C ⟩
+Comp Γ f g = {!!}
+
+
+
+
+
+-- Mapping a monotone function
+mMap : {A B : Predomain} -> ⟨ (A ==> B) ==> (𝕃 A ==> 𝕃 B) ⟩
+mMap {A} {B} = Curry (mExt' (A ==> B) ((With2nd mRet) ∘m App))
+-- Curry (mExt' {!!} {!!}) -- mExt' (mComp' (Curry {!!}) {!!}) -- mExt (mComp mRet f)
+
+
+mMap' : {Γ A B : Predomain} ->
+    ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d 𝕃 A ==> 𝕃 B) ⟩
+mMap' f = Uncurry {!!}
+
+Map : {Γ A B : Predomain} ->
+    ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ==> 𝕃 A) ⟩ -> ⟨ (Γ ==> 𝕃 B) ⟩
+Map {Γ} f la = S Γ (mMap' f) la -- Γ ! mMap' f <*> la
 
 
   {-
@@ -190,18 +285,23 @@ abstract
   -}
 
   -- Embedding of function spaces is monotone
-  mFunEmb : {A A' B B' : Predomain} ->
+mFunEmb : (A A' B B' : Predomain) ->
     ⟨ A' ==> 𝕃 A ⟩ ->
     ⟨ B ==> B' ⟩ ->
     ⟨ (A ==> 𝕃 B) ==> (A' ==> 𝕃 B') ⟩
-  mFunEmb fA'LA fBB' = (mExt' (mMap' (K fBB') ∘m Id)) ∘m (K fA'LA)
+mFunEmb A A' B B' fA'LA fBB' =
+    Curry (Bind ((A ==> 𝕃 B) ×d A')
+      (mCompU fA'LA π2)
+      (Map (mCompU fBB' π2) ({!!})))
+  --  _ $ (mExt' _ (_ $ (mMap' (K _ fBB')) ∘m Id)) ∘m (K _ fA'LA)
   -- mComp' (mExt' (mComp' (mMap' (K fBB')) Id)) (K fA'LA)
 
-  mFunProj : {A A' B B' : Predomain} ->
+mFunProj : (A A' B B' : Predomain) ->
    ⟨ A ==> A' ⟩ ->
    ⟨ B' ==> 𝕃 B ⟩ ->
    ⟨ (A' ==> 𝕃 B') ==> 𝕃 (A ==> 𝕃 B) ⟩
-  mFunProj fAA' fB'LB = mRet' (mExt' (K fB'LB) ∘m Id ∘m (K fAA'))
+mFunProj A A' B B' fAA' fB'LB = {!!}
+  -- mRet' (mExt' (K fB'LB) ∘m Id ∘m (K fAA'))
 
   -- 
 
@@ -219,3 +319,42 @@ abstract
 
   -- mComp (mExt (mComp (mMap fBB') f1)) fA'LA ≤ mComp (mExt (mComp (mMap fBB') f2)) fA'LA
   -- ((ext ((mapL fBB') ∘ f1)) ∘ fA'LA) (a'1) ≤ ((ext ((mapL fBB') ∘ f2)) ∘ fA'LA) (a'2)
+
+
+ -- Properties
+bind-unit-l : {Γ A B : Predomain} ->
+    (f : ⟨ Γ ×d A ==> 𝕃 B ⟩) ->
+    (a : ⟨ Γ ==> A ⟩) ->
+    rel (Γ ==> 𝕃 B)
+      (Bind Γ (mRet' Γ a) f)
+      (Γ ! f <*> a)
+bind-unit-l = {!!}
+
+bind-unit-r : {Γ A B : Predomain} ->
+    (la : ⟨ Γ ==> 𝕃 A ⟩) ->
+    rel (Γ ==> 𝕃 A)
+     la
+     (Bind Γ la (mRet' _ π2))
+bind-unit-r la = {!!}
+
+
+bind-Ret' : {Γ A : Predomain} ->
+    (la : ⟨ Γ ==> 𝕃 A ⟩) ->
+    (a : ⟨ Γ ×d A ==> A ⟩) ->
+    rel (Γ ==> 𝕃 A)
+      la
+      (Bind Γ la ((mRet' _ a)))
+bind-Ret' = {!!}
+      
+
+bind-K : {Γ A B : Predomain} ->
+    (la : ⟨ Γ ==> 𝕃 A ⟩) ->
+    (lb : ⟨ 𝕃 B ⟩) ->
+     rel (Γ ==> 𝕃 B)
+       (K Γ lb)
+       (Bind Γ la ((K (Γ ×d A) lb)))
+bind-K = {!!}
+
+ {- Goal: rel (⟦ Γ ⟧ctx ==> 𝕃 ⟦ B ⟧ty) ⟦ err [ N ] ⟧tm
+      (Bind ⟦ Γ ⟧ctx ⟦ N ⟧tm (Curry ⟦ err ⟧tm))
+ -}
diff --git a/formalizations/guarded-cubical/Results.agda b/formalizations/guarded-cubical/Results.agda
index 52ed6959c91850b35af2bff32153c7c97deaafec..9e1a62e5f7f6cda9017c13057216e724d8b1a639 100644
--- a/formalizations/guarded-cubical/Results.agda
+++ b/formalizations/guarded-cubical/Results.agda
@@ -5,13 +5,20 @@ open import Later
 module Results (k : Clock) where
 
 open import Cubical.Foundations.Prelude
-open import Cubical.Data.Nat renaming (ℕ to Nat) hiding (_·_)
+open import Cubical.Data.Nat renaming (ℕ to Nat) hiding (_·_ ; _^_)
+open import Cubical.Data.Nat.Order
 open import Cubical.Foundations.Structure
+open import Cubical.Data.Empty.Base renaming (rec to exFalso)
+open import Cubical.Data.Sum
+open import Cubical.Data.Sigma
+open import Cubical.Relation.Nullary
+
 
 open import StrongBisimulation k
 open import Semantics k
 open import SyntacticTermPrecision k
 open import GradualSTLC
+open import MonFuns k
 
 private
   variable
@@ -22,6 +29,223 @@ private
   â–¹_ A = â–¹_,_ k A
 
 
+
+
+-- Results about the intensional theory
+
+
+module 2Cell
+  (A A' B B' : Predomain)
+  (Aâ–¹A' : EP A A')
+  (Bâ–¹B' : EP B B')
+ where
+
+  open 𝕃
+  open EP
+
+  _⊑A'_ : ⟨ A' ⟩ -> ⟨ A' ⟩ -> Type
+  _⊑A'_ = rel A'
+
+  _⊑B'_ : ⟨ 𝕃 B' ⟩ -> ⟨ 𝕃 B' ⟩ -> Type
+  _⊑B'_ = rel (𝕃 B')
+
+  _⊑c_ : ⟨ A ⟩ -> ⟨ A' ⟩ -> Type
+  a ⊑c a' = (U (emb A▹A') a) ⊑A' a'
+
+  _⊑d_ : ⟨ 𝕃 B ⟩ -> ⟨ 𝕃 B' ⟩ -> Type
+  lb ⊑d lb' = (mapL (U (emb B▹B')) lb) ⊑B' lb'
+
+  _⊑f_ : ⟨ A ==> 𝕃 B ⟩ -> ⟨ A' ==> 𝕃 B' ⟩ -> Type
+  f ⊑f f' = fun-order-het A A' (𝕃 B) (𝕃 B') _⊑c_ _⊑d_ (MonFun.f f) (MonFun.f f')
+  
+
+module 2CellVertical
+  (A A' A'' B B' B'' : Predomain)
+  (Aâ–¹A' : EP A A')
+  (A'â–¹A'' : EP A' A'')
+  (Bâ–¹B' : EP B B')
+  (B'â–¹B'' : EP B' B'')
+  where
+
+
+
+
+-- Results about the extensional theory
+
+tick-extensionality : (X : Set) -> (lx~ : ▹ (L℧ X)) -> (ly : L℧ X) ->
+  ▸ (λ t -> lx~ t ≡ ly) ->
+  lx~ ≡ next ly
+tick-extensionality X lx~ ly H = λ i t → H t i
+
+
+tick-extensionality' : (X : Set) -> (lx~ : ▹ (L℧ X)) -> (ly : L℧ X) ->
+  ((t : Tick k) -> lx~ t ≡ ly) -> -- is there an implicit ▸ here?
+  lx~ ≡ next ly
+tick-extensionality' X lx~ ly H = λ i t₁ → H t₁ i
+
+
+
+
+
+
+η≢δ : (d : Predomain) -> (x : ⟨ d ⟩) -> (n : Nat) ->
+  ¬ ((η x) ≡ (δ ^ n) ℧)
+η≢δ d x zero contra = {!!}
+η≢δ d x (suc n) = {!!}
+
+
+open 𝕃 ℕ -- defines the lock-step relation
+
+
+-- Bisimilarity is non-trivial at Nat type
+≈-non-trivial : {!!}
+≈-non-trivial = {!!}
+
+-- Bisimilarity is not transitive at Nat type
+
+
+
+-- Adequacy of lock-step relation
+module AdequacyLockstep
+  -- (lx ly : L℧ Nat)
+  -- (lx≾ly : lx ≾ ly)
+  where
+
+  _≾'_ : L℧ Nat → L℧ Nat → Type
+  _≾'_ = ord' (next _≾_)
+
+  {-
+  lx≾'ly : lx ≾' ly
+  lx≾'ly = transport (λ i → unfold-ord i lx ly) lx≾ly
+  -}
+
+  eq-later-eq-now : (X : Set) -> (lx~ : ▹ (L℧ X)) -> (ly : L℧ X) ->
+    ▸ (λ t -> lx~ t ≡ ly) ->
+    θ lx~ ≡ θ (next ly)
+  eq-later-eq-now = {!!}
+
+
+  sigma-later : (X : Set) (A : X -> Tick k -> Type) ->
+    ▸ (λ t -> Σ X λ x -> A x t) ->
+    Σ (▹ X) λ x~ -> ▸ (λ t -> A (x~ t) t)
+  sigma-later X A H = (λ t → fst (H t)) , (λ t → snd (H t))
+
+  ≾->≾' : (lx ly : L℧ Nat) ->
+    lx ≾ ly -> lx ≾' ly
+  ≾->≾' lx ly lx≾ly = transport (λ i → unfold-ord i lx ly) lx≾ly
+
+  adequate-err-baby :
+    ▹ ((lx : L℧ Nat) ->
+      (H-lx : lx ≾' δ ℧) ->
+      (lx ≡ ℧) ⊎ (lx ≡ δ ℧)) ->
+    (lx : L℧ Nat) ->
+    (H-lx : lx ≾' δ ℧) ->
+    (lx ≡ ℧) ⊎ (lx ≡ δ ℧)
+  adequate-err-baby _ (η x) ()
+  adequate-err-baby _ ℧ _ = inl refl
+  adequate-err-baby IH (θ lx~) H-lx =
+    inr (cong θ (tick-extensionality Nat lx~ ℧
+      λ t → {!!}))
+
+
+  data GuardedNat : Type where
+    zro : GuardedNat
+    suc : â–¹ Nat -> GuardedNat
+
+  _≤GN_ : GuardedNat -> Nat -> Type
+  n~ ≤GN m = {!!}
+
+{-
+  adequate-err :
+    â–¹ ((m : Nat) ->
+    (lx : L℧ Nat) ->
+    (H-lx : lx ≾' (δ ^ m) ℧) ->
+    (Σ (▹ Nat) λ n -> (n ≤GN m) × (lx ≡ (δ ^ n) ℧))) ->
+    (m : Nat) ->
+    (lx : L℧ Nat) ->
+    (H-lx : lx ≾' (δ ^ m) ℧) ->
+    (Σ (▹ Nat) λ n -> (n ≤ m) × ((lx ≡ (δ ^ n) ℧)))
+  adequate-err _ zero (η x) ()
+  adequate-err _ (suc m') (η x) ()
+  adequate-err _ m ℧ H-lx = next (0 , {!!})
+  adequate-err _ zero (θ lx~) ()
+  adequate-err IH (suc m') (θ lx~) H-lx = {!!}
+-}
+
+  ≾'-δ : (lx ly : L℧ Nat) -> (lx ≾' ly) -> (lx ≾' (δ ly))
+  ≾'-δ = {!!}
+
+
+  adequate-err-2 : (m : Nat) -> Σ Nat λ n -> (n ≤ m) ×
+    (▹ ((lx : L℧ Nat) ->
+        (H-lx : lx ≾' (δ ^ m) ℧) ->
+        (lx ≡ (δ ^ n) ℧)) ->
+      (lx : L℧ Nat) ->
+      (H-lx : lx ≾' (δ ^ m) ℧) ->
+      ((lx ≡ (δ ^ n) ℧)))
+  adequate-err-2 zero = zero , ≤-refl , thm-zero
+    where
+      thm-zero : ▹ ((lx : L℧ Nat) → lx ≾' (δ ^ zero) ℧ → lx ≡ (δ ^ zero) ℧) →
+                    (lx : L℧ Nat) → lx ≾' (δ ^ zero) ℧ → lx ≡ (δ ^ zero) ℧
+      thm-zero IH ℧ H-lx = refl
+  adequate-err-2 (suc m') =
+    (suc (fst (adequate-err-2 m'))) , ({!!} , {!!})
+      where
+        thm-suc-m' : {!!}
+        thm-suc-m' IH ℧ H-lx = {!!}
+        thm-suc-m' IH (θ lx~) H-lx =
+          cong θ (tick-irrelevance Nat lx~ ((δ ^ fst (adequate-err-2 m')) ℧)
+          λ t → {!!})
+
+
+-- Given:  θ lx~ ≾' (δ ^ suc m') ℧
+-- i.e.    θ lx~ ≾' θ (next (δ ^ m') ℧)
+-- i.e.    ▸ (λ t -> (lx~ t) ≾ (δ ^ m') ℧)
+
+-- By IH, we have
+-- ▸ (λ t -> lx~ t ≡ (δ ^ n') ℧ for some n')
+
+-- By tick extensionality, we have
+-- lx~ ≡ next (δ ^ n') ℧, so
+-- θ lx~ ≡ θ (next (δ ^ n') ℧) ≡ (δ ^ (suc n')) ℧
+
+
+-- Adequacy of weak bisimilarity relation
+
+open Bisimilarity â„•
+
+module AdequacyBisimilarity
+  (lx ly : L℧ Nat)
+  (lx≈ly : lx ≈ ly) where
+
+
+-- Combined result: Adequacy of extensional ordering
+
+open ExtRel â„•
+
+module AdequacyExt
+  (lx ly : L℧ Nat)
+  (lx⊴ly : lx ⊴ ly) where
+
+  adequate-1 : (n : Nat) (x : Nat) ->
+    (lx ≡ (δ ^ n) (η x)) ->
+    Σ Nat λ m -> ly ≡ (δ ^ m) (η x)
+  adequate-1 n x H-lx = {!!}
+
+  adequate-2 : (m : Nat) ->
+    (ly ≡ (δ ^ m) ℧) ->
+    Σ Nat λ n -> lx ≡ (δ ^ n) ℧
+  adequate-2 m H-ly = {!!}
+
+
+
+  
+
+
+
+
+{-
 gradual_guarantee : (M : Tm · nat) (N : Tm · nat) ->
                     · |- M ⊑tm N # nat ->
                     ⟦ M ⟧ ≲ ⟦ N ⟧
+-}
diff --git a/formalizations/guarded-cubical/Semantics.agda b/formalizations/guarded-cubical/Semantics.agda
index ad95c95198e02249234007092dba5a6de2072fc2..02ba34f87b462a90fb6daad3aad50cc1a88f202a 100644
--- a/formalizations/guarded-cubical/Semantics.agda
+++ b/formalizations/guarded-cubical/Semantics.agda
@@ -37,71 +37,10 @@ private
   â–¹_ A = â–¹_,_ k A
 
 
-
 open 𝕃
 
 -- Denotations of Types
 
-{-
-
--- First definition of Dyn'
-
-data Dyn' (D : â–¹ Type) : Type where
-  nat : Nat -> Dyn' D
-  fun : (▸ D -> L℧ (Dyn' D)) -> Dyn' D
-
--- Dyn' is a recursive sum type, so we can
--- define the ordering inductively
--- (same way as you'd define an ordering on lists)
-
-DynP' : (D : â–¹ Predomain) -> Predomain
-DynP' D = Dyn' (λ t -> ⟨ D t ⟩) ,
-          posetstr order {!!}
-
-      where
-
-      order : Dyn' (λ t → ⟨ D t ⟩) → Dyn' (λ t → ⟨ D t ⟩) → Type ℓ-zero
-      order (nat n1) (nat n2) = n1 ≡ n2
-      order (fun f) (fun g) = ∀ x y ->
-        rel (â–¸' D) x y ->
-        cust-order (f x) (g y)
-          where
-            cust-order' :
-             ▹ (L℧ (Dyn' (λ t → ⟨ D t ⟩)) -> L℧ (Dyn' (λ t → ⟨ D t ⟩)) -> Type) ->
-                L℧ (Dyn' (λ t → ⟨ D t ⟩)) -> L℧ (Dyn' (λ t → ⟨ D t ⟩)) -> Type
-            cust-order' _ ℧ _ = Unit
-            cust-order' rec (η x) (η y) = order x y
-            cust-order' _ (η _) _ = ⊥
-            cust-order' rec (θ lx~) (θ ly~) = {!!}
-            cust-order' _ (θ _) _ = ⊥
-
-            cust-order :  L℧ (Dyn' (λ t → ⟨ D t ⟩)) -> L℧ (Dyn' (λ t → ⟨ D t ⟩)) -> Type
-            cust-order = fix cust-order'
-         
-      order _ _ = ⊥
--}
-
--- Alternate definition of Dyn' (different encoding of function case)
-
-{-
-data Dyn' (T : â–¹ Type) : Type where
-  nat : Nat -> Dyn' T
-  fun  : ▸ (λ t → T t -> L℧ (T t)) -> Dyn' T
-
-DynP' : (D : â–¹ Predomain) -> Predomain
-DynP' D = Dyn' (λ t -> ⟨ D t ⟩) , posetstr order {!!}
-  where
-    order : Dyn' (λ t → ⟨ D t ⟩) → Dyn' (λ t → ⟨ D t ⟩) → Type ℓ-zero
-    order (nat n1) (nat n2) = n1 ≡ n2
-    order (fun f) (fun g) = ∀ x y ->
-      rel (â–¸' D) x y ->
-      ▸ λ t -> rel (𝕃 (D t)) (f t (x t)) (g t (y t))
-    order _ _ = ⊥
--}
-
-----------------------------------------------------------
--- Third definition of DynP, where we build in the requirement that
--- the functions must be monotone
 
 data Dyn' (D : â–¹ Predomain) : Type where
   nat : Nat -> Dyn' D
@@ -139,7 +78,6 @@ DynP' D = (Dyn' D) ,
 
 ----------------------------------------------------------
 
---DynP P = (▸ (λ t -> Dyn' (next ⟨ P t ⟩))) , posetstr {!!} {!!}
 
 DynP : Predomain
 DynP = fix DynP'
@@ -149,17 +87,6 @@ unfold-DynP = fix-eq DynP'
 
 
 
--- Equation for the underlying set of DynP
-{-
-unfold-⟨DynP⟩ : ⟨ DynP ⟩ ≡ Dyn' (next ⟨ DynP ⟩)
-unfold-⟨DynP⟩ =
-  ⟨ fix DynP' ⟩                    ≡⟨ (λ i → ⟨ unfold-DynP i ⟩ ) ⟩
-  ⟨ DynP' (next DynP) ⟩            ≡⟨ refl ⟩
-  Dyn' (λ t -> ⟨ (next DynP) t ⟩)  ≡⟨ refl ⟩
-  Dyn' (next ⟨ DynP ⟩) ∎
--}
-
-
 unfold-⟨DynP⟩ : ⟨ DynP ⟩ ≡ ⟨ DynP' (next DynP) ⟩
 unfold-⟨DynP⟩ = λ i → ⟨ unfold-DynP i ⟩
 
@@ -171,6 +98,14 @@ DynP'-to-DynP d = transport (sym (λ i -> ⟨ unfold-DynP i ⟩)) d
 DynP-to-DynP' : ⟨ DynP ⟩ -> ⟨ DynP' (next DynP) ⟩
 DynP-to-DynP' d = transport (λ i → ⟨ unfold-DynP i ⟩) d
 
+DynP-DynP'-iso : (d : ⟨ DynP' (next DynP) ⟩) ->
+  DynP-to-DynP' (DynP'-to-DynP d) ≡ d
+DynP-DynP'-iso d = {!!}
+
+DynP-DynP'-iso-inv : (d : ⟨ DynP ⟩) ->
+  DynP'-to-DynP (DynP-to-DynP' d) ≡ d
+DynP-DynP'-iso-inv d = {!!}
+
 
 -- This basically is a monotonicity result, and could be
 -- incorporated as a constant into the combinator language.
@@ -209,6 +144,10 @@ record EP (A B : Predomain) : Set where
   field
     emb : MonFun A B
     proj : MonFun B (𝕃 A)
+    wait-l-e : ⟨ A ==> A ⟩
+    wait-l-p : ⟨ 𝕃 A ==> 𝕃 A ⟩
+    wait-r-e : ⟨ B ==> B ⟩
+    wait-r-p : ⟨ 𝕃 B ==> 𝕃 B ⟩
 
 
 -- Identity E-P pair
@@ -216,7 +155,11 @@ record EP (A B : Predomain) : Set where
 EP-id : (A : Predomain) -> EP A A
 EP-id A = record {
   emb = record { f = id ; isMon = λ x≤y → x≤y };
-  proj = record { f = ret ; isMon = ord-η-monotone A }}
+  proj = record { f = ret ; isMon = ord-η-monotone A };
+  wait-l-e = Id;
+  wait-l-p = Id;
+  wait-r-e = Id;
+  wait-r-p = Id}
 
 
 
@@ -244,7 +187,7 @@ p-nat' = record { f = g ; isMon = g-mon }
     g-mon {fun f} {fun g} x≤y = ord-bot ℕ ℧
 
 p-nat : MonFun DynP (𝕃 ℕ)
-p-nat = S (K p-nat') (mTransport unfold-DynP)
+p-nat = {!!} -- S DynP (K DynP p-nat') (mTransport unfold-DynP)
   -- or:
   -- mTransportDomain (sym unfold-DynP) p-nat'
 
@@ -252,34 +195,39 @@ p-nat = S (K p-nat') (mTransport unfold-DynP)
 EP-nat : EP â„• DynP
 EP-nat = record {
   emb = e-nat;
-  proj = p-nat }
+  proj = p-nat;
+  wait-l-e = Id;
+  wait-l-p = Id;
+  wait-r-e = Id;
+  wait-r-p = Id}
 
 
 -- E-P Pair for monotone functions Dyn to L℧ Dyn
 
-e-fun : MonFun (arr' DynP (𝕃 DynP)) DynP
+e-fun : MonFun (DynP ==> (𝕃 DynP)) DynP
 e-fun = record { f = e-fun-f ; isMon = e-fun-mon }
   where
-    e-fun-f : ⟨ arr' DynP (𝕃 DynP) ⟩ -> ⟨ DynP ⟩
+    e-fun-f : ⟨ DynP ==> (𝕃 DynP) ⟩ -> ⟨ DynP ⟩
     e-fun-f f = DynP'-to-DynP (fun (next f))
 
     e-fun-mon :
-      {f1 f2 : ⟨ arr' DynP (𝕃 DynP) ⟩} ->
-      rel (arr' DynP (𝕃 DynP)) f1 f2 ->
+      {f1 f2 : ⟨ DynP ==> (𝕃 DynP) ⟩} ->
+      rel (DynP ==> (𝕃 DynP)) f1 f2 ->
       rel DynP (e-fun-f f1) (e-fun-f f2)
     e-fun-mon {f1} {f2} f1≤f2 =
       DynP-rel (fun (next f1)) (fun (next f2)) (λ t d1 d2 d1≤d2 → {!!})
 
 
-p-fun : MonFun DynP (𝕃 (arr' DynP (𝕃 DynP)))
+p-fun : MonFun DynP (𝕃 (DynP ==> (𝕃 DynP)))
 p-fun = record { f = p-fun-f ; isMon = {!!} }
   where
 
-    p-fun-f' : ⟨ DynP' (next DynP) ⟩ -> ⟨ 𝕃 (arr' DynP (𝕃 DynP)) ⟩
+    p-fun-f' : ⟨ DynP' (next DynP) ⟩ -> ⟨ 𝕃 (DynP ==> (𝕃 DynP)) ⟩
     p-fun-f' (nat n) = ℧
-    p-fun-f' (fun f) = η {!!}
+    p-fun-f' (fun f) = θ (λ t → η (f t))
+    -- f : ▸ (λ t → MonFun (next DynP t) (𝕃 (next DynP t)))
 
-    p-fun-f : ⟨ DynP ⟩ -> ⟨ 𝕃 (arr' DynP (𝕃 DynP)) ⟩
+    p-fun-f : ⟨ DynP ⟩ -> ⟨ 𝕃 (DynP ==> (𝕃 DynP)) ⟩
     -- p-fun-f d = p-fun-f' (transport unfold-⟨DynP⟩ d)
     p-fun-f d = p-fun-f' (transport (λ i -> ⟨ unfold-DynP i ⟩) d)
 
@@ -287,7 +235,11 @@ p-fun = record { f = p-fun-f ; isMon = {!!} }
 EP-fun : EP (arr' DynP (𝕃 DynP)) DynP
 EP-fun = record {
   emb = e-fun;
-  proj = p-fun }
+  proj = p-fun;
+  wait-l-e = Id;
+  wait-l-p = Δ;
+  wait-r-e = Id;
+  wait-r-p = Δ}
 
 
 
@@ -303,10 +255,13 @@ module EPComp
   open MonFun
 
   comp-emb : ⟨ A ==> C ⟩
-  comp-emb = K (emb epBC) <*> (emb epAB) -- mComp (emb epBC) (emb epAB)
+  comp-emb = mCompU (emb epBC) (emb epAB)
+  -- A ! K A (emb epBC) <*> (emb epAB) -- mComp (emb epBC) (emb epAB)
 
   comp-proj : ⟨ C ==> 𝕃 A ⟩
-  comp-proj = (mExt' (K (proj epAB))) <*> (proj epBC) -- mComp (mExt (proj epAB)) (proj epBC)
+  comp-proj = Bind C (proj epBC) (mCompU (proj epAB) π2)
+  --C ! (mExt' C (K C (proj epAB))) <*> (proj epBC)
+  -- mComp (mExt (proj epAB)) (proj epBC)
   --  comp-proj-f =
   --    λ c -> bind (f (proj epBC) c) (f (proj epAB)) ==
   --    λ c -> ext  (f (proj epAB)) (f (proj epBC) c) ==
@@ -315,7 +270,23 @@ module EPComp
   EP-comp : EP A C
   EP-comp = record {
     emb = comp-emb;
-    proj = comp-proj }
+    proj = comp-proj;
+    wait-l-e = wait-l-e epAB;
+    wait-l-p = wait-l-p epAB;
+    wait-r-e = wait-r-e epBC;
+    wait-r-p = wait-r-p epBC}
+
+
+-- Lifting EP pairs to 𝕃
+EP-lift : {A B : Predomain} -> EP A B -> EP (𝕃 A) (𝕃 B)
+EP-lift epAB =
+  record {
+    emb = U mMap (EP.emb epAB);
+    proj = U mMap (EP.proj epAB);
+    wait-l-e = U mMap (EP.wait-l-e epAB);
+    wait-l-p = U mMap (EP.wait-l-p epAB);
+    wait-r-e = U mMap (EP.wait-r-e epAB);
+    wait-r-p = U mMap (EP.wait-r-p epAB) }
 
 
 -- Lifting EP pairs to functions
@@ -326,10 +297,10 @@ module EPArrow
   (epBB' : EP B B') where
 
     e-arrow : ⟨ (A ==> 𝕃 B) ==> (A' ==> 𝕃 B') ⟩
-    e-arrow = mFunEmb (EP.proj epAA') (EP.emb epBB')
+    e-arrow = mFunEmb A A' B B' (EP.proj epAA') (EP.emb epBB')
 
     p-arrow : ⟨ (A' ==> (𝕃 B')) ==> (𝕃 (A ==> (𝕃 B))) ⟩
-    p-arrow = mFunProj (EP.emb epAA') (EP.proj epBB')
+    p-arrow = mFunProj A A' B B' (EP.emb epAA') (EP.proj epBB')
 
 {-
     p-lift :
@@ -342,10 +313,40 @@ module EPArrow
 EP-arrow : {A A' B B' : Predomain} ->
   EP A A' ->
   EP B B' ->
-  EP (arr' A (𝕃 B)) (arr' A' (𝕃 B'))
+  EP (A ==> (𝕃 B)) (A' ==> (𝕃 B'))
 EP-arrow epAA' epBB' = record {
   emb = e-arrow;
-  proj = p-arrow  }
+  proj = p-arrow;
+  
+  wait-l-e = Curry (
+    (mMap' (With2nd (EP.wait-l-e epBB'))) ∘m
+    (Uncurry mExt) ∘m
+    (With2nd (EP.wait-l-p epAA')) ∘m
+    (mRet' _ π2)
+  ) ;
+  
+  wait-l-p = U mMap (Curry (
+    With2nd (EP.wait-l-p epBB') ∘m
+    App ∘m
+    With2nd (EP.wait-l-e epAA')
+  )) ;
+  
+  wait-r-e = Curry (
+    mMap' (With2nd (EP.wait-r-e epBB')) ∘m
+    ((Uncurry mExt) ∘m
+    (With2nd (EP.wait-r-p epAA') ∘m
+    (mRet' _ π2)))) ;
+  -- or : wait-r-e = Curry (mMap' (With2nd (EP.wait-r-e epBB')) ∘m ((Uncurry mExt) ∘m (With2nd (EP.wait-r-p epAA') ∘m (With2nd mRet)))) ;
+
+  
+  wait-r-p = U mMap (Curry (
+    With2nd (EP.wait-r-p epBB') ∘m
+    App ∘m
+    With2nd (EP.wait-r-e epAA')
+  ))
+
+  }
+  
   where open EPArrow epAA' epBB'
 
 
@@ -355,13 +356,14 @@ EP-arrow epAA' epBB' = record {
 
 open EPComp
 
-
+-- Types are predomains
 ⟦_⟧ty : Ty -> Predomain
 ⟦ nat ⟧ty = ℕ
 ⟦ dyn ⟧ty = DynP
-⟦ A => B ⟧ty = arr' ⟦ A ⟧ty (𝕃 ⟦ B ⟧ty)
+⟦ A => B ⟧ty =  ⟦ A ⟧ty ==> (𝕃 ⟦ B ⟧ty)
 -- ⟦ A ⟧ty -> L℧ ⟦ B ⟧ty
 
+-- Contexts are predomains
 ⟦_⟧ctx : Ctx -> Predomain
 ⟦ · ⟧ctx = UnitP
 ⟦ Γ :: A ⟧ctx = ⟦ Γ ⟧ctx ×d ⟦ A ⟧ty -- ⟦ Γ ⟧ctx × ⟦ A ⟧ty
@@ -389,10 +391,12 @@ mLook : {Γ : Ctx} ->
   (A : Ty) ->
   (x : Γ ∋ A) ->
   ⟨ ⟦ Γ ⟧ctx ==> ⟦ A ⟧ty ⟩
-mLook A x = record {
-  f = λ env -> look env A x ;
-  isMon = λ {env1} {env2} env1≤env2 → look-mon env1 env2 A x env1≤env2 }
+mLook A vz = π2
+mLook A (vs z) = mCompU (mLook A z) π1
 
+mLook-vz : {Γ : Ctx} -> (A : Ty) -> (env : ⟨ ⟦ Γ :: A ⟧ctx ⟩) ->
+  MonFun.f (mLook A (vz {Γ})) env ≡ proj₂ env
+mLook-vz = {!!}
 
 
 ---------------------------------------
@@ -413,8 +417,11 @@ mLook A x = record {
 -- *** Denotation of terms ***
 
 tm-sem : {A : Ty} {Γ : Ctx} -> Tm Γ A -> ⟨ ⟦ Γ ⟧ctx ==> (𝕃 ⟦ A ⟧ty) ⟩
-tm-sem (var z) = mRet' (mLook _ z)
-tm-sem (lda M) = mRet' (K (tm-sem M) ∘m Pair)
+tm-sem {_} {Γ} (var z) = mRet' ⟦ Γ ⟧ctx (mLook _ z)
+tm-sem {_} {Γ} (lda M) = mRet' ⟦ Γ ⟧ctx (Curry (tm-sem M))
+--(_ $ K ⟦ Γ ⟧ctx (tm-sem M) ∘m Pair)
+
+-- mRet' ? (K (tm-sem M) ∘m Pair))
 
 {-
 record {
@@ -425,10 +432,11 @@ record {
   isMon = {!!} }
 -}
   
-tm-sem {A} {Γ} (app {S = B} M1 M2) =
-    let kont = (K (swap mExt) <*> tm-sem M2) in
-    (mExt' kont <*> tm-sem M1)
-
+tm-sem {A} {Γ} (app {S = B} M1 M2) = {!!}
+{-
+    let kont = (⟦ Γ ⟧ctx ! K ⟦ Γ ⟧ctx (swap _ {- (⟦ B ⟧ty ==> 𝕃 ⟦ A ⟧ty) -} mExt) <*> tm-sem M2) in
+    (⟦ Γ ⟧ctx ! mExt' ⟦ Γ ⟧ctx kont <*> tm-sem M1)
+-}
 
 -- mExt :      ⟨ (⟦ B ⟧ty ==> 𝕃 ⟦ A ⟧ty) ==> 𝕃 ⟦ B ⟧ty ==> 𝕃 ⟦ A ⟧ty ⟩
 -- swap mExt : ⟨ 𝕃 ⟦ B ⟧ty ==> ( ⟦ B ⟧ty ==> 𝕃 ⟦ A ⟧ty ) ==> 𝕃 ⟦ A ⟧ty ⟩
@@ -458,10 +466,12 @@ record {
     isMon = {!!} }
 -}
     
-tm-sem {A} err = K ℧
+tm-sem {A} {Γ} err = K ⟦ Γ ⟧ctx ℧
 -- record { f = λ _ -> ℧ ; isMon = λ _ -> ord-bot ⟦ A ⟧ty ℧ }
 
-tm-sem (up A⊑B M) = (mMap' (K (EP.emb ⟦ A⊑B ⟧lt))) <*> (tm-sem M)
+tm-sem {_} {Γ} (up A⊑B M) = Map (mCompU (EP.emb ⟦ A⊑B ⟧lt) π2) (tm-sem M)
+  -- ⟦ Γ ⟧ctx ! (mMap' (K ⟦ Γ ⟧ctx (EP.emb ⟦ A⊑B ⟧lt))) <*> (tm-sem M)
+  -- Map (K ⟦ Γ ⟧ctx (EP.emb ⟦ A⊑B ⟧lt)) (tm-sem M)
 
 {-
 record {
@@ -469,7 +479,9 @@ record {
   isMon = {!!} }
 -}
   
-tm-sem (dn A⊑B M) = (mExt' (K (EP.proj ⟦ A⊑B ⟧lt))) <*> (tm-sem M)
+tm-sem {_} {Γ} (dn A⊑B M) =
+  -- ⟦ Γ ⟧ctx ! (mExt' ⟦ Γ ⟧ctx (K ⟦ Γ ⟧ctx (EP.proj ⟦ A⊑B ⟧lt))) <*> (tm-sem M)
+  Bind ⟦ Γ ⟧ctx (tm-sem M) (mCompU (EP.proj ⟦ A⊑B ⟧lt) π2)
 
 {-
 record { f =
@@ -477,10 +489,11 @@ record { f =
   isMon = {!!} }
 -}
   
-tm-sem zro = K (η zero)
+tm-sem {_} {Γ} zro = K ⟦ Γ ⟧ctx (η zero)
 -- record { f = λ _ -> η zero ; isMon = λ _ → ord-refl ℕ (η zero) }
 
-tm-sem (suc M) = (mExt' (K (mRet' mSuc))) <*> (tm-sem M)
+tm-sem {_} {Γ} (suc M) = {!!}
+-- ⟦ Γ ⟧ctx ! (mExt' ⟦ Γ ⟧ctx (K ⟦ Γ ⟧ctx (mRet' ℕ mSuc))) <*> (tm-sem M)
 {-
 record {
   f =  λ ⟦Γ⟧ -> bind (MonFun.f (tm-sem M) ⟦Γ⟧) (λ n -> η (suc n)) ;
@@ -499,17 +512,18 @@ record {
 -- *** Denotation of term precision ***
 --  ⟦ M ⟧ ≲ ⟦ N ⟧
 
-open WeakRel
+open Bisimilarity
 
+{-
 -- Homogeneous term precision relation
 lttm-hom : {A : Ty} ->
   (Γ : Ctx) ->
   (M : Tm (lhs (Ctx-ref Γ)) A) ->
   (N : Tm (rhs (Ctx-ref Γ)) A) ->
   (Ctx-ref Γ) |- M ⊑tm N # (⊑ref A) ->
-  (⟦ A ⟧ty ≾ ((MonFun.f ⟦ M ⟧tm) {!!})) ((MonFun.f ⟦ N ⟧tm) {!!})
+  (⟦ A ⟧ty ≾ ((MonFun.f ⟦ M ⟧tm) {!!} )) ((MonFun.f ⟦ N ⟧tm) {!!})
 lttm-hom Γ M N M⊑N = {!!}
-
+-}
 
 {-
 mapL-emb : {A A' : Type} -> (epAA' : EP A A') (a : L℧ A) ->
@@ -527,18 +541,224 @@ typrecd-sem : {A B : Ty} ->
   (c : A ⊑ B) -> (⟨ ⟦ A ⟧ty ⟩ -> ⟨ ⟦ B ⟧ty ⟩ -> Type)
 typrecd-sem dyn = rel DynP
 typrecd-sem {Ain => Aout} {Bin => Bout} (cin => cout) =
-  λ f1 f2 -> fun-order-het
-    ⟦ Ain ⟧ty ⟦ Bin ⟧ty (𝕃 ⟦ Aout ⟧ty) (𝕃 ⟦ Bout ⟧ty)
+  λ f1 f2 -> fun-order-het  ⟦ Ain ⟧ty ⟦ Bin ⟧ty (𝕃 ⟦ Aout ⟧ty) (𝕃 ⟦ Bout ⟧ty)
     (typrecd-sem cin)
     (LiftRelation.ord ⟦ Aout ⟧ty ⟦ Bout ⟧ty (typrecd-sem cout))
     (MonFun.f f1) (MonFun.f f2)
+    -- (MonFun.f (MonFun.f (EP.wait-l-e ⟦ cin => cout ⟧lt) f1))
+    -- (MonFun.f (MonFun.f (EP.wait-r-e ⟦ cin => cout ⟧lt) f2))
 typrecd-sem nat = rel â„•
 typrecd-sem inj-nat = λ n d -> rel' n (DynP-to-DynP' d)
   where
     rel' : ⟨ ℕ ⟩ -> ⟨ DynP' (next DynP) ⟩ -> Type
     rel' n (nat n') = n ≡ n'
     rel' n (fun _) = ⊥
-typrecd-sem (inj-arrow c) = {!!}
+typrecd-sem {Ain => Aout} (inj-arrow (cin => cout)) =
+  λ f d -> rel' f (DynP-to-DynP' d)
+  where
+    rel' : ⟨ ⟦ Ain ⟧ty ==> 𝕃 ⟦ Aout ⟧ty ⟩ -> ⟨ DynP' (next DynP) ⟩ -> Type
+    rel' f (nat n) = ⊥
+    rel' f (fun f') = ▸ λ t ->
+      fun-order-het ⟦ Ain ⟧ty DynP (𝕃 ⟦ Aout ⟧ty) (𝕃 DynP)
+      (typrecd-sem cin)
+      (LiftRelation.ord ⟦ Aout ⟧ty DynP (typrecd-sem cout))
+      (MonFun.f f) (MonFun.f (f' t))
+
+------------------------------------------
+-- *** Heterogeneous term precision *** --
+
+tmprec : {Γ : Ctx} -> {A B : Ty} ->
+  (c : A ⊑ B) -> Tm Γ A -> Tm Γ B -> Type
+tmprec {Γ} {A} {B} c M N =
+  fun-order-het ⟦ Γ ⟧ctx ⟦ Γ ⟧ctx (𝕃 ⟦ A ⟧ty) (𝕃 ⟦ B ⟧ty)
+  (rel ⟦ Γ ⟧ctx)
+    (LiftRelation.ord ⟦ A ⟧ty ⟦ B ⟧ty (typrecd-sem c))
+    (MonFun.f ⟦ M ⟧tm) (MonFun.f ⟦ N ⟧tm)
+
+
+
+-----------------------------------------
+
+
+x≤emb : {Γ : Ctx} -> (A B : Ty) -> (x : (· :: A) ∋ A) -> (c : A ⊑ B) ->
+  tmprec c (var x) (up c (var x))
+x≤emb .dyn .dyn x dyn (_ , d1) (_ , d2) (_ , d1≤d2) =
+           transport
+             (sym (λ i → LiftRelation.unfold-ord DynP DynP (rel DynP) i
+                           (MonFun.f ⟦ var x ⟧tm (tt , d1))
+                           (MonFun.f ⟦ up dyn (var x) ⟧tm (tt , d2))))
+             {!!}
+x≤emb .(_ => _) .(_ => _) x (c => c₁) = {!!}
+x≤emb .nat .nat x nat (_ , n1) (_ , n2) (_ , n1≡n2) =
+           transport
+             (sym (λ i → LiftRelation.unfold-ord ℕ ℕ (rel ℕ) i
+                           (MonFun.f ⟦ var x ⟧tm (tt , n1))
+                           (MonFun.f ⟦ up nat (var x) ⟧tm (tt , n2))))
+             {!!}
+x≤emb .nat .dyn x inj-nat = {!!}
+x≤emb A .dyn x (inj-arrow c) = {!!}
+
+
+
+
+
+open EPComp
+
+
+-- Properties of the wait functions
+module WaitProp
+  where
+
+  open EP
+
+  wait-l-θ : {A B : Ty} -> (c : A ⊑ B) -> (la~ : ▹ L℧ ⟨ ⟦ A ⟧ty ⟩) ->
+    Σ (▹ L℧ ⟨ ⟦ A ⟧ty ⟩) λ la'~ ->
+      MonFun.f (wait-l-p ⟦ c ⟧lt) (θ la~) ≡
+      θ (λ t -> MonFun.f (wait-l-p ⟦ c ⟧lt) (la'~ t))
+  wait-l-θ dyn la~ = la~ , refl
+  wait-l-θ {Ai => Ao} {Bi => Bo} (cin => cout) la~ = {!!}
+  wait-l-θ nat la~ = la~ , refl
+  wait-l-θ inj-nat la~ = la~ , refl
+  wait-l-θ {Ai => Ao} (inj-arrow (cin => cout)) la~ = {!!} , {!!}
+
+
+  wait-r-θ : {A B : Ty} -> (c : A ⊑ B) -> (lb~ : ▹ L℧ ⟨ ⟦ B ⟧ty ⟩) ->
+    Σ (▹ L℧ ⟨ ⟦ B ⟧ty ⟩) λ lb'~ ->
+      MonFun.f (wait-r-p ⟦ c ⟧lt) (θ lb~) ≡
+      θ (λ t -> MonFun.f (wait-r-p ⟦ c ⟧lt) (lb'~ t))
+  wait-r-θ dyn la~ = la~ , refl
+  wait-r-θ {Ai => Ao} {Bi => Bo} (cin => cout) la~ = {!!}
+  wait-r-θ nat la~ = la~ , refl
+  wait-r-θ inj-nat la~ = la~ , refl
+  wait-r-θ {Ai => Ao} (inj-arrow (cin => cout)) la~ = la~ ,
+    transport (λ i -> δ (θ la~) ≡ θ (λ t -> θ (next-Mt≡M la~ t (~ i)))) refl
+
+  -- Goal :  δ (θ la~)        ≡ θ (λ t → δ (la~ t))
+  -- i.e.    θ (next (θ la~)) ≡ θ (λ t → θ (next (la~ t)))
+  
+  -- By tick irr + later extensionality, we have that
+  -- ▸ λ t -> (next (la~ t) == la~)
+
+  -- So the goal becomes
+  -- θ (next (θ la~)) ≡ θ (λ t → θ (la~))
+  -- θ (next (θ la~)) ≡ θ (next (θ la~))
+  
+
+
+-- Universal properties of casts
+module UniversalProps where
+{-
+UpR : {A B C : Ty} ->
+  (M1 : ⟨ ⟦ A ⟧ty ⟩) ->
+  (M2 : ⟨ ⟦ B ⟧ty ⟩) ->
+  (c : A ⊑ B) ->
+  (d : B ⊑ C) ->
+  typrecd-sem c M1 M2 ->
+  typrecd-sem (⊑comp c d)
+    (MonFun.f (EP.wait-l-e ⟦ c ⟧lt) M1)
+    (MonFun.f (EP.emb ⟦ d ⟧lt) M2)
+UpR M1 M2 dyn dyn M1⊑M2 = M1⊑M2
+
+UpR {Ai => Ao} {Bi => Bo} {Ci => Co}
+  M1 M2 (cin => cout) (din => dout) M1⊑M2 =
+  λ ai ci ai⊑ci → {!!}
+
+UpR {Ai => Ao} {Bi => Bo}
+  M1 M2 (cin => cout) (inj-arrow (cin' => cout')) M1⊑M2 =
+  {!!}
+
+UpR M1 M2 nat nat M1⊑M2 = M1⊑M2
+
+UpR M1 M2 nat inj-nat M1⊑M2 = {!!}
+
+UpR M1 M2 inj-nat dyn M1⊑M2 = M1⊑M2
+
+UpR {Ai => Ao} M1 M2 (inj-arrow (cin' => cout')) dyn M1⊑M2 = {!!}
+-}
+
+
+  UpR : {A B C : Ty} ->
+    (M1 M2 : ⟨ ⟦ A ⟧ty ⟩) ->
+    (c : A ⊑ B) ->
+    rel ⟦ A ⟧ty M1 M2 ->
+    typrecd-sem c
+      (MonFun.f (EP.wait-l-e ⟦ c ⟧lt) M1)
+      (MonFun.f (EP.emb ⟦ c ⟧lt) M2)
+  UpR M1 M2 dyn M1⊑M2 = M1⊑M2
+  UpR M1 M2 (cin => cout) M1⊑M2 = {!!}
+  UpR M1 M2 nat M1⊑M2 = M1⊑M2
+  UpR M1 M2 inj-nat M1⊑M2 = {!!} -- transport stuff
+  UpR {Ai => Ao} M1 M2 (inj-arrow (cin' => cout')) M1⊑M2 = {!!}
+
+
+
+  UpL : {A B C : Ty} ->
+    (M1 : ⟨ ⟦ A ⟧ty ⟩) ->
+    (M2 : ⟨ ⟦ B ⟧ty ⟩) ->
+    (c : A ⊑ B) ->
+    typrecd-sem c M1 M2 ->
+    rel ⟦ B ⟧ty
+      (MonFun.f (EP.emb ⟦ c ⟧lt) M1)
+      (MonFun.f (EP.wait-r-e ⟦ c ⟧lt) M2)
+  UpL M1 M2 dyn M1⊑M2 = M1⊑M2
+  UpL M1 M2 (cin => cout) M1⊑M2 = {!!}
+  UpL M1 M2 nat M1⊑M2 = M1⊑M2
+  UpL M1 M2 inj-nat M1⊑M2 = {!!} -- transport stuff
+  UpL {Ai => Ao} M1 M2 (inj-arrow (cin' => cout')) M1⊑M2 = {!!}
+
+-- By our assumption that M1 is related to M2,
+-- (DynP-to-DynP' M2) must be of the form (fun f') where
+-- ▸ (λ t -> M1 ⊑ (f' t)).
+-- Thus, we have that emb M1 is related to M2 in the DynP relation
+-- which is what we needed to show (since here wait-r-e is the identity)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+id≤map : {A B : Predomain} ->
+  (la la' : L℧ ⟨ A ⟩) ->
+  (f : ⟨ A ⟩ -> ⟨ B ⟩) ->
+  (R : ⟨ A ⟩ -> ⟨ B ⟩ -> Type) ->
+  ((a a' : ⟨ A ⟩) -> rel A a a' -> R a (f a')) ->
+  ord' A (next (ord A)) la la' ->
+  LiftRelation.ord' A B R (next (LiftRelation.ord A B R)) la (mapL f la')
+id≤map {A} {B} (η x) (η x') f R H la≤la' =
+  -- subst {!!} {!!} (H x x' la≤la')  -- (H x x' la≤la')
+  transport
+    (sym (λ i → LiftRelation.ord' A B R _ (η x) (mapL-eta f x' i)))
+    (H x x' la≤la')
+id≤map ℧ la' f R H la≤la' = tt
+id≤map {A} {B} (θ lx~) (θ ly~) f R H la≤la' =
+  transport
+    (sym (λ i → LiftRelation.ord' A B R (next (LiftRelation.ord A B R)) (θ lx~) (mapL-theta f ly~ i)))
+    λ t → {!!}
+
+-- LiftRelation.ord' A B R (next (LiftRelation.ord A B R)) (η x)
+--      (mapL f (η x'))
+
+
+
+
+
 
 
 
@@ -547,15 +767,30 @@ typrecd-sem (inj-arrow c) = {!!}
 -- *** Beta/eta properties ***
 
 
+-- Semantic interpretation of substitution
+
+-- Correct subtitution lemma for values
+
 
--- Semantic meaning of substitution
 
+
+-- This is incorrect. Counterexample is if N is err and M is a term that
+-- doesn't refer to its free variable
 sub-lemma : (Γ : Ctx) (A B : Ty) -> (M : Tm (Γ :: A) B) -> (N : Tm Γ A) ->
-  ⟦ M [ N ] ⟧tm ≡ {!!}
-sub-lemma = {!!}
+  rel (⟦ Γ ⟧ctx ==> 𝕃 ⟦ B ⟧ty)
+      (⟦ M [ N ] ⟧tm)
+      (Bind ⟦ Γ ⟧ctx ⟦ N ⟧tm (⟦ M ⟧tm))
+sub-lemma Γ A .A (var vz) N = bind-Ret' (⟦ N ⟧tm) (mLook A vz)
+sub-lemma Γ A B (var (vs x)) N = {!!}
+sub-lemma Γ A .(_ => _) (lda M) N = {!!}
+sub-lemma Γ A B (app M1 M2) N = {!!}
+sub-lemma Γ A B err N = bind-K (⟦ N ⟧tm) ℧
+sub-lemma Γ A B (up x M) N = {!!}
+sub-lemma Γ A B (dn x M) N = {!!}
+sub-lemma Γ A .nat zro N = bind-K (⟦ N ⟧tm) (η zero)
+sub-lemma Γ A .nat (suc M) N = {!!}
 
 {-
-
 lem1 : ∀ (Γ : Ctx) (A B : Ty) -> (M : Tm (Γ :: A) B) (N : Tm Γ A) ->
    ⟦ app (lda M) N ⟧tm ≡ {!!}
 lem1 Γ A B M N =
@@ -573,21 +808,18 @@ lem1 Γ A B M N =
 
 -}
 
--- TODO need to stipulate that N is a value?
-beta-lt : (Γ : Ctx) (A B : Ty) -> (M : Tm (Γ :: A) B) -> (N : Tm Γ A) ->
-  rel (⟦ Γ ⟧ctx ==> 𝕃 ⟦ B ⟧ty)   ⟦ app (lda M) N ⟧tm   ⟦ M [ N ] ⟧tm
-beta-lt Γ A B (var x) N = {!!}
-beta-lt Γ A .(_ => _) (lda M) N = {!!}
-beta-lt Γ A B (app M M₁) N = {!!}
-beta-lt Γ A B err N = {!!}
-beta-lt Γ A B (up x M) N = {!!}
-beta-lt Γ A B (dn x M) N = {!!}
-beta-lt Γ A .nat zro N = {!!}
-beta-lt Γ A .nat (suc M) N = {!!}
 
+beta-lt : (Γ : Ctx) (A B : Ty) -> (M : Tm (Γ :: A) B) -> {!!}
+  -- rel {!!} ⟦ app (lda {!!}) (var vz) ⟧tm ⟦ M ⟧tm
+beta-lt = {!!}
+
+
+
+{-
 eta : (Γ : Ctx) (A B : Ty) -> (M : Tm Γ (A => B)) ->
   rel {!!}  ⟦ M ⟧tm ⟦ {!lda!} ⟧tm
 eta = {!!}
+-}
 
 
 {-
diff --git a/formalizations/guarded-cubical/StrongBisimulation.agda b/formalizations/guarded-cubical/StrongBisimulation.agda
index 8fd40b292c5a00052a63efa4bea05ff6f0a78699..895c8cbe81358e7de26aa75b8b17a7fc640749f1 100644
--- a/formalizations/guarded-cubical/StrongBisimulation.agda
+++ b/formalizations/guarded-cubical/StrongBisimulation.agda
@@ -24,6 +24,8 @@ open import Cubical.Data.Sum hiding (rec)
 open import Cubical.Foundations.Structure
 open import Cubical.Foundations.HLevels
 
+open import Cubical.Relation.Nullary
+
 open import Cubical.Data.Unit.Properties
 
 open import Agda.Primitive
@@ -58,6 +60,10 @@ rel d = PosetStr._≤_ (d .snd)
 reflexive : (d : Predomain) -> (x : ⟨ d ⟩) -> (rel d x x)
 reflexive d x = IsPoset.is-refl (PosetStr.isPoset (str d)) x
 
+transitive : (d : Predomain) -> (x y z : ⟨ d ⟩) ->
+  rel d x y -> rel d y z -> rel d x z
+transitive d x y z x≤y y≤z =
+  IsPoset.is-trans (PosetStr.isPoset (str d)) x y z x≤y y≤z 
 
 -- Monotone functions from X to Y
 
@@ -70,6 +76,33 @@ record MonFun (X Y : Predomain) : Set where
     f : (X .fst) → (Y .fst)
     isMon : ∀ {x y} → x ≤X y → f x ≤Y f y
 
+-- Use reflection to show that this is a sigma type
+-- Look for proof in standard library to show that
+-- Sigma type with a proof that RHS is a prop, then equality of a pair
+-- follows from equality of the LHS's
+-- Specialize to the case of monotone functions and fill in the proof
+-- later
+
+-- Monotone relations between predomains X and Y
+-- (antitone in X, monotone in Y).
+record MonRel {â„“' : Level} (X Y : Predomain) : Type (â„“-suc â„“') where
+  module X = PosetStr (X .snd)
+  module Y = PosetStr (Y .snd)
+  _≤X_ = X._≤_
+  _≤Y_ = Y._≤_
+  field
+    R : ⟨ X ⟩ -> ⟨ Y ⟩ -> Type ℓ'
+    isAntitone : ∀ {x x' y} -> R x y -> x' ≤X x -> R x' y
+    isMonotone : ∀ {x y y'} -> R x y -> y ≤Y y' -> R x y'
+
+predomain-monrel : (X : Predomain) -> MonRel X X
+predomain-monrel X = record {
+  R = rel X ;
+  isAntitone = λ {x} {x'} {y} x≤y x'≤x → transitive X x' x y x'≤x x≤y ;
+  isMonotone = λ {x} {y} {y'} x≤y y≤y' -> transitive X x y y' x≤y y≤y' }
+
+
+{-
 record IsMonFun {X Y : Predomain} (f : ⟨ X ⟩ → ⟨ Y ⟩) : Type (ℓ-max ℓ ℓ') where
   no-eta-equality
   constructor ismonfun
@@ -94,6 +127,7 @@ record MonFunStr (â„“' : Level) (X Y : Predomain) : Type (â„“-max â„“ (â„“-suc 
 
 MonF : ∀ ℓ ℓ' -> Predomain -> Predomain -> Type (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ'))
 MonF â„“ â„“' X Y = TypeWithStr â„“ {!!}
+-}
 
 {-
 lem-later : {X~ : â–¹ Type} ->
@@ -101,9 +135,13 @@ lem-later : {X~ : â–¹ Type} ->
 lem-later = ?
 -}
 
+
 isSet-poset : {ℓ ℓ' : Level} -> (P : Poset ℓ ℓ') -> isSet ⟨ P ⟩
 isSet-poset P = IsPoset.is-set (PosetStr.isPoset (str P))
 
+
+-- Theta for predomains
+
 ▸' : ▹ Predomain → Predomain
 ▸' X = (▸ (λ t → ⟨ X t ⟩)) ,
        posetstr ord
@@ -134,9 +172,13 @@ isSet-poset P = IsPoset.is-set (PosetStr.isPoset (str P))
          (PosetStr.isPoset (str (X t))) (a t) (b t) (ord-ab t) (ord-ba t) i
 
 
+-- Delay for predomains
 ▸''_ : Predomain → Predomain
 â–¸'' X = â–¸' (next X)
 
+
+-- Error domains
+
 record ErrorDomain : Set₁ where
   field
     X : Predomain
@@ -155,6 +197,44 @@ data L℧ (X : Set) : Set where
   ℧ : L℧ X
   θ : ▹ (L℧ X) → L℧ X
 
+-- Similar to caseNat,
+-- defined at https://agda.github.io/cubical/Cubical.Data.Nat.Base.html#487
+caseL℧ : {X : Set} -> {ℓ : Level} -> {A : Type ℓ} ->
+  (aη a℧ aθ : A) → (L℧ X) → A
+caseL℧ aη a℧ aθ (η x) = aη
+caseL℧ aη a℧ aθ ℧ = a℧
+caseL℧ a0 a℧ aθ (θ lx~) = aθ
+
+-- Similar to znots and snotz, defined at
+-- https://agda.github.io/cubical/Cubical.Data.Nat.Properties.html
+℧≠θ : {X : Set} -> {lx~ : ▹ (L℧ X)} -> ¬ (℧ ≡ θ lx~)
+℧≠θ {X} {lx~} eq = subst (caseL℧ X (L℧ X) ⊥) eq ℧
+
+θ≠℧ : {X : Set} -> {lx~ : ▹ (L℧ X)} -> ¬ (θ lx~ ≡ ℧)
+θ≠℧ {X} {lx~} eq = subst (caseL℧ X ⊥ (L℧ X)) eq (θ lx~)
+
+
+-- Does this make sense?
+pred : {X : Set} -> (lx : L℧ X) -> ▹ (L℧ X)
+pred (η x) = next ℧
+pred ℧ = next ℧
+pred (θ lx~) = lx~
+
+pred-def : {X : Set} -> (def : ▹ (L℧ X)) -> (lx : L℧ X) -> ▹ (L℧ X)
+pred-def def (η x) = def
+pred-def def ℧ = def
+pred-def def (θ lx~) = lx~
+
+
+-- Uses the pred function above, and I'm not sure whether that
+-- function makes sense.
+inj-θ : {X : Set} -> (lx~ ly~ : ▹ (L℧ X)) ->
+  θ lx~ ≡ θ ly~ ->
+  ▸ (λ t -> lx~ t ≡ ly~ t)
+inj-θ lx~ ly~ H = let lx~≡ly~ = cong pred H in
+  λ t i → lx~≡ly~ i t
+
+
 
 ret : {X : Set} -> X -> L℧ X
 ret = η
@@ -185,17 +265,53 @@ ext f = fix (ext' f)
 bind : L℧ A -> (A -> L℧ B) -> L℧ B
 bind {A} {B} la f = ext f la
 
+mapL : (A -> B) -> L℧ A -> L℧ B
+mapL f la = bind la (λ a -> ret (f a))
+
 unfold-ext : (f : A -> L℧ B) -> ext f ≡ ext' f (next (ext f))
 unfold-ext f = fix-eq (ext' f)
 
-mapL : (A -> B) -> L℧ A -> L℧ B
-mapL f la = bind la (λ a -> ret (f a))
+
+ext-eta : ∀ (a : A) (f : A -> L℧ B) ->
+  ext f (η a) ≡ f a
+ext-eta a f =
+  fix (ext' f) (ret a)            ≡⟨ (λ i → unfold-ext f i (ret a)) ⟩
+  (ext' f) (next (ext f)) (ret a) ≡⟨ refl ⟩
+  f a ∎
+
+ext-err : (f : A -> L℧ B) ->
+  bind ℧ f ≡ ℧
+ext-err f =
+  fix (ext' f) ℧            ≡⟨ (λ i → unfold-ext f i ℧) ⟩
+  (ext' f) (next (ext f)) ℧ ≡⟨ refl ⟩
+  ℧ ∎
+
+
+ext-theta : (f : A -> L℧ B)
+            (l : ▹ (L℧ A)) ->
+            bind (θ l) f ≡ θ (ext f <$> l)
+ext-theta f l =
+  (fix (ext' f)) (θ l)            ≡⟨ (λ i → unfold-ext f i (θ l)) ⟩
+  (ext' f) (next (ext f)) (θ l)   ≡⟨ refl ⟩
+  θ (fix (ext' f) <$> l) ∎
+
+
+
+mapL-eta : (f : A -> B) (a : A) ->
+  mapL f (η a) ≡ η (f a)
+mapL-eta f a = ext-eta a λ a → ret (f a)
+
+mapL-theta : (f : A -> B) (la~ : ▹ (L℧ A)) ->
+  mapL f (θ la~) ≡ θ (mapL f <$> la~)
+mapL-theta f la~ = ext-theta (ret ∘ f) la~
 
 
 -- Strong bisimulation relation/ordering for the lift monad
 
+{-
 U : Predomain -> Type
 U p = ⟨ p ⟩
+-}
 
 {-
 module LiftOrder (p : Predomain) where
@@ -304,7 +420,7 @@ fun-order-het P1 P1' P2 P2' rel-P1P1' rel-P2P2' fP1P2 fP1'P2' =
   rel-P2P2' (fP1P2 p) (fP1'P2' p')
 
 
--- TODO can define this in terms of fun-order-general
+-- TODO can define this in terms of fun-order-het
 fun-order : (P1 P2 : Predomain) -> (⟨ P1 ⟩ -> ⟨ P2 ⟩) -> (⟨ P1 ⟩ -> ⟨ P2 ⟩) -> Type ℓ-zero
 fun-order P1 P2 f1 f2 =
   (x y : ⟨ P1 ⟩) -> x ≤P1 y -> (f1 x) ≤P2 (f2 y)
@@ -416,7 +532,9 @@ arr dom cod =
     where
        -- open LiftOrder
        const-err : ⟨ arr' dom (𝕌 cod) ⟩
-       const-err = record { f = λ _ -> ErrorDomain.℧ cod ; isMon = λ _ -> reflexive (𝕌 cod) (ErrorDomain.℧ cod) }
+       const-err = record {
+         f = λ _ -> ErrorDomain.℧ cod ;
+         isMon = λ _ -> reflexive (𝕌 cod) (ErrorDomain.℧ cod) }
 
        const-err-bot : (f : ⟨ arr' dom (𝕌 cod) ⟩) -> rel (arr' dom (𝕌 cod)) const-err f
        const-err-bot f = λ x y x≤y → ErrorDomain.℧⊥ cod (MonFun.f f y)
@@ -460,10 +578,7 @@ module LiftRelation
   ord-bot lb = transport (sym (λ i → unfold-ord i ℧ lb)) tt
 
 
-  -- ord-trans-IH
-
-
-module LiftRelTransitive
+module LiftRelMonotone
   (A B C : Predomain)
   (ordAB : ⟨ A ⟩ -> ⟨ B ⟩ -> Type)
   (ordBC : ⟨ B ⟩ -> ⟨ C ⟩ -> Type)
@@ -513,6 +628,11 @@ module LiftRelTransitive
   -}
   
 
+-- Delay function
+δ : {X : Type} -> L℧ X -> L℧ X
+δ = θ ∘ next
+  where open L℧
+
 
 -- Predomain to lift predomain
 module 𝕃 (p : Predomain) where
@@ -534,12 +654,18 @@ module 𝕃 (p : Predomain) where
   ord :  L℧ ⟨ p ⟩ → L℧ ⟨ p ⟩ → Type
   ord = fix ord'
 
+  _≾_ : L℧ ⟨ p ⟩ -> L℧ ⟨ p ⟩ -> Type
+  _≾_ = ord
+
   unfold-ord : ord ≡ ord' (next ord)
   unfold-ord = fix-eq ord'
 
   ord-η-monotone : {x y : ⟨ p ⟩} -> x ≤ y -> ord (η x) (η y)
   ord-η-monotone {x} {y} x≤y = transport (sym λ i → unfold-ord i (η x) (η y)) x≤y
 
+  ord-δ-monotone : {lx ly : L℧ ⟨ p ⟩} -> ord lx ly -> ord (δ lx) (δ ly)
+  ord-δ-monotone = {!!}
+
   ord-bot : (lx : L℧ ⟨ p ⟩) -> ord ℧ lx
   ord-bot lx = transport (sym λ i → unfold-ord i ℧ lx) tt
 
@@ -721,44 +847,307 @@ Pair {A} = record {
   isMon = λ {a1} {a2} a1≤a2 b1 b2 b1≤b2 → a1≤a2 , b1≤b2 }
 
 
--- Weak bisimulation relaion
--- Define compositionally
 
-δ : {X : Type} -> L℧ X -> L℧ X
-δ = θ ∘ next
-  where open L℧
 
-module WeakRel (d : Predomain) where
+
+-- Induced equivalence relation on a Predomain
+equivRel : (d : Predomain) -> EquivRel ⟨ d ⟩ ℓ-zero
+equivRel d =
+  (λ x y → (x ≤ y) × (y ≤ x)) ,
+  BinaryRelation.equivRel
+    (λ x → (reflexive d x) , (reflexive d x))
+    (λ x y (x≤y , y≤x) → y≤x , x≤y)
+    λ x y z (x≤y , y≤x) (y≤z , z≤y) →
+      (transitive d x y z x≤y y≤z) , (transitive d z y x z≤y y≤x)
+  where
+    module D = PosetStr (d .snd)
+    _≤_ = D._≤_
+
+
+congruence : {X : Type} -> (_R_ : L℧ X -> L℧ X -> Type) -> Type
+congruence {X} _R_ = {lx ly : ▹ (L℧ X)} -> ▸ (λ t → (lx t) R (ly t)) -> (θ lx) R (θ ly)
+
+congruence' : {X : Type} -> (_R_ : L℧ X -> L℧ X -> Type) -> Type
+congruence' {X} _R_ = {lx ly : L℧ X} -> ▹ (lx R ly) -> (θ (next lx)) R (θ (next ly))
+
+cong→cong' : ∀ {X}{_R_ : L℧ X -> L℧ X -> Type} → congruence _R_ → congruence' _R_
+cong→cong' cong ▹R = cong ▹R
+
+trivialize : {X : Type} (_R_ : L℧ X -> L℧ X -> Type) ->
+  BinaryRelation.isTrans _R_ ->
+  congruence _R_ ->
+  ((x : L℧ X) -> x R (θ (next x))) ->
+  ((x : L℧ X) -> x R (fix θ))
+trivialize {X} _R_ hTrans hCong hθR = fix trivialize'
+  where
+   trivialize' :
+    ▹ ((x : L℧ X) -> x R (fix θ)) → (x : L℧ X) -> x R (fix θ)
+   trivialize' IH lx =
+     subst (λ y → lx R y) (sym (fix-eq θ))
+       (hTrans _ _ _
+         (hθR lx)
+         (hCong (λ t → IH t lx)))
+
+
+
+-- Weak bisimulation relaion
+
+module Bisimilarity (d : Predomain) where
 
   module D = PosetStr (d .snd)
-  _≤_ = D._≤_
+  private
+    _==_ = fst (equivRel d) -- the equivalence relation induced by d
+    isEqRel = snd (equivRel d)
 
   -- make this a module so we can avoid having to make the IH
   -- a parameter of the comparison function
   module Inductive (IH : ▹ (L℧ ⟨ d ⟩ -> L℧ ⟨ d ⟩ -> Type)) where
 
-
-    _≾'_ : L℧ (U d) -> L℧ (U d) -> Type
-    ℧ ≾' _ = Unit
+    _≈'_ : L℧ (⟨ d ⟩) -> L℧ (⟨ d ⟩) -> Type
+    ℧ ≈' ℧ = Unit
       
-    η x ≾' η y = x ≤ y
+    η x ≈' η y = x == y
     
-    θ lx ≾' θ ly = ▸ (λ t -> IH t (lx t) (ly t))
+    θ lx ≈' θ ly = ▸ (λ t -> IH t (lx t) (ly t))
     -- or equivalently: θ lx ≾' θ ly = ▸ ((IH ⊛ lx) ⊛ ly)
-      
-    η x ≾' θ t = Σ Nat λ n -> Σ (U d) (λ y -> (θ t ≡ (δ ^ n) (η y)) × (x ≤ y))
 
-    -- need to account for error (θ s ≡ delay of η x or delay of ℧, in which case we're done)
-    θ s ≾' η y = Σ Nat λ n ->
-       (θ s ≡ (δ ^ n) L℧.℧) ⊎
-       (Σ (U d) (λ x -> (θ s ≡ (δ ^ n) (η x)) × (x ≤ y)))
-      
-    _ ≾' ℧ = ⊥
-   
-  _≾_ : L℧ (U d) -> L℧ (U d) -> Type
-  _≾_ = fix _≾'_
+    θ x~ ≈' ℧ = Σ Nat λ n -> θ x~ ≡ (δ ^ n) ℧
+
+    θ x~ ≈' η y = Σ Nat λ n -> Σ ⟨ d ⟩ λ x -> (θ x~ ≡ (δ ^ n) (η x)) × (x == y)
+
+    ℧ ≈' θ y~ = Σ Nat λ n -> θ y~ ≡ (δ ^ n) ℧
+
+    η x ≈' θ y~ = Σ Nat λ n -> Σ ⟨ d ⟩ λ y -> (θ y~ ≡ (δ ^ n) (η y)) × (x == y)
+
+    _ ≈' _ = ⊥
+
+
+  _≈_ : L℧ (⟨ d ⟩) -> L℧ (⟨ d ⟩) -> Type
+  _≈_ = fix _≈'_
     where open Inductive
 
+  unfold-≈ : _≈_ ≡ Inductive._≈'_ (next _≈_)
+  unfold-≈ = fix-eq Inductive._≈'_
+
+  
+  
+
+  module Properties where
+    open Inductive (next _≈_)
+    open BinaryRelation (_==_)
+
+    ≈->≈' : {lx ly : L℧ ⟨ d ⟩} ->
+     lx ≈ ly -> lx ≈' ly
+    ≈->≈' {lx} {ly} lx≈ly = transport (λ i → unfold-≈ i lx ly) lx≈ly
+
+    ≈'->≈ : {lx ly : L℧ ⟨ d ⟩} ->
+     lx ≈' ly -> lx ≈ ly
+    ≈'->≈ {lx} {ly} lx≈'ly = transport (sym (λ i → unfold-≈ i lx ly)) lx≈'ly
+
+
+
+{-
+    bisim-θ : (lx~ ly~ : L℧ ⟨ d ⟩) ->
+       ▸ (λ t → lx~ t ≈ ly~ t) ->
+       θ lx~ ≈ θ ly~
+-} 
+
+    symmetric' :
+      ▹ ((lx ly : L℧ ⟨ d ⟩) -> lx ≈' ly -> ly ≈' lx) ->
+         (lx ly : L℧ ⟨ d ⟩) -> lx ≈' ly -> ly ≈' lx
+    symmetric' _ ℧ ℧ _ = tt
+    symmetric' _ (η x) (η y) (x≤y , y≤x) = y≤x , x≤y -- symmetry of the underlying relation
+    symmetric' IH (θ lx~) (θ ly~) lx≈'ly =
+      λ t → ≈'->≈  (IH t (lx~ t) (ly~ t) (≈->≈' (lx≈'ly t)))
+    symmetric' _ (θ lx~) ℧ (n , H-eq) = n , H-eq
+    symmetric' _ (θ lx~) (η y) (n , x , H-eq , H-rel) =
+      n , x , H-eq , (isEquivRel.symmetric isEqRel x y H-rel)
+    symmetric' _ ℧ (θ ly~) (n , H-eq) = n , H-eq
+    symmetric' _ (η x) (θ ly~) (n , y , H-eq , H-rel) =
+      n , y , H-eq , (isEquivRel.symmetric isEqRel x y H-rel)
+
+    symmetric : (lx ly : L℧ ⟨ d ⟩) -> lx ≈ ly -> ly ≈ lx
+    symmetric = fix (subst {!!} {!!}) 
+
+     -- fix (transport {!!} symmetric')
+
+   {-
+
+        ord-trans = fix (transport (sym (λ i ->
+         (▹ ((a b c : L℧ ⟨ p ⟩) →
+            unfold-ord i a b → unfold-ord i b c → unfold-ord i a c) →
+             (a b c : L℧ ⟨ p ⟩) →
+            unfold-ord i a b → unfold-ord i b c → unfold-ord i a c))) ord-trans-ind)
+  -}
+
+    θ-cong : congruence _≈_
+    θ-cong {lx~} {ly~} H-later = ≈'->≈ H-later
+    -- Goal: θ lx ≈ θ ly
+    -- i.e. (θ lx) (≈' (next ≈)) (θ ly)
+    -- i.e. ▸ (λ t → (lx t) ((next ≈) t) (ly t))
+    -- i.e. ▸ (λ t → (lx t) ≈ (ly t))
+
+    x≈'δx : ▹ ((lx : L℧ ⟨ d ⟩) -> lx ≈' (δ lx)) ->
+               (lx : L℧ ⟨ d ⟩) -> lx ≈' (δ lx)
+    x≈'δx _ (η x) = 1 , x , refl , (isEquivRel.reflexive isEqRel x)
+    x≈'δx _ ℧ = 1 , refl
+    x≈'δx IH (θ lx~) =
+
+      -- Alternate solution:
+      -- λ t → ≈'->≈
+      --  (transport (λ i → (lx~ t) ≈' θ (next-Mt≡M lx~ t i)) (IH t (lx~ t)))
+
+       transport
+         (λ i -> ▸ (λ t -> unfold-≈ (~ i) (lx~ t) (θ (next-Mt≡M lx~ t i))))
+         λ t → IH t (lx~ t)
+
+    -- Goal: θ lx~ ≈' δ (θ lx~)
+    -- i.e.  θ lx~ ≈' θ (next (θ lx~))
+    -- i.e. ▸ λ t -> (lx~ t) ((next ≈) t) ((next (θ lx~)) t)
+    -- i.e. ▸ λ t -> (lx~ t) ≈ (θ lx~)
+    -- The IH says: ▸ λ t -> (lx~ t) ≈' (θ (next (lx~ t)))
+    -- So we just need to change ≈' to ≈ and change
+    -- (θ (next (lx~ t))) to (θ lx~). The below term does this.
+   
+    -- (λ i -> ▸ (λ t -> unfold-≈ (~ i) (lx~ t) (θ (next-Mt≡M lx~ t i)))) :
+    --
+    --   ▸ λ t -> (lx~ t) ≈' (θ (next (lx~ t))) ≡
+    --   ▸ λ t -> (lx~ t) ≈  (θ lx~)
+
+    -- Informally:
+  
+    -- By IH, we know:
+    --   (lx~ t) ≈' (δ (lx~ t))
+
+    -- Also Know:
+    --   lx~ ≡ next (lx~ t) (using later-extensionality + tick irrelevance)
+
+    -- So STS:
+    --         (lx~ t) ≈ θ (next (lx~ t))
+    -- which holds by IH.
+
+    x≈δx : (lx : L℧ ⟨ d ⟩) -> lx ≈ (δ lx)
+    x≈δx = {!!}
+
+
+    -- ¬_ : Set → Set
+    -- ¬ A = A → ⊥
+
+    contradiction : {A : Type} -> A -> ¬ A -> ⊥
+    contradiction HA ¬A = ¬A HA
+
+    contrapositive : {A : Type} -> (A -> B) -> (¬ B -> ¬ A)
+    contrapositive A→B ¬B HA = ¬B (A→B HA)
+
+    non-trivial→not-transitive :
+      (Σ ⟨ d ⟩ λ x -> Σ ⟨ d ⟩ λ y -> (¬ (x == y))) ->
+      ¬ (BinaryRelation.isTrans _≈_)
+    non-trivial→not-transitive (x , y , x≠y) H-trans =
+      let fixθ-top = trivialize _≈_ H-trans θ-cong x≈δx in
+      let ηx≈ηy = H-trans (η x) (fix θ) (η y)
+                        (fixθ-top (η x))
+                        (symmetric _ _ (fixθ-top (η y))) in
+      let not-ηx≈ηy = contrapositive (λ H -> ≈->≈' H) x≠y in
+      contradiction ηx≈ηy not-ηx≈ηy
+
+
+    inj-δ : {X : Set} -> (lx ly : L℧ X) -> δ lx ≡ δ ly -> lx ≡ ly
+    inj-δ lx ly δlx≡δly = let tmp = inj-θ (next lx) (next ly) δlx≡δly in
+      {!!}
+
+
+    fixθ-lem1 : (n : Nat) ->
+      (▹ (¬ (θ (next (fix θ)) ≡ (δ ^ n) ℧))) ->
+          ¬ (θ (next (fix θ)) ≡ (δ ^ n) ℧)
+    fixθ-lem1 zero    _  H-eq =  θ≠℧ H-eq
+    fixθ-lem1 (suc n) IH H-eq =
+       let tmp = inj-θ (next (fix θ)) (next ((δ ^ n) ℧)) H-eq in {!!}
+     
+
+    ℧-fixθ : ¬ (℧ ≈' θ (next (fix θ)))
+    ℧-fixθ (n , H-eq) = {!!}
+
+
+
+
+
+
+{-
+    lem1 :
+      ▹ ((lx : L℧ ⟨ d ⟩) -> lx ≾' θ (next lx)) ->
+        (lx : L℧ ⟨ d ⟩) -> lx ≾' θ (next lx)
+    lem1 _ (η x) = 1 , (x , (refl , (reflexive d x)))
+    lem1 _ ℧ = tt
+    lem1 IH (θ lx~) = {!!}
+
+
+    lem2 :
+      (lx~ ly~ : ▹ L℧ ⟨ d ⟩) ->
+      (n : Nat) ->
+      θ lx~ ≾' θ ly~ ->
+      θ ly~ ≡ (δ ^ n)  ℧ ->
+      Σ Nat λ m -> θ lx~ ≡ (δ ^ m) ℧
+    lem2 lx ly n lx≤ly H-eq-δ = {!!}
+
+    lem3 :
+      (lx~ ly~ : ▹ L℧ ⟨ d ⟩) ->
+      (n : Nat) ->
+      (x' : ⟨ d ⟩) ->
+      θ lx~ ≾' θ ly~ ->
+      θ lx~ ≡ (δ ^ n) (η x') ->
+      Σ Nat λ m -> Σ ⟨ d ⟩ λ y' -> θ ly~ ≡ (δ ^ m) (η y')
+    lem3 = {!!}
+
+
+    trans-ind :
+        ▹ ((lx ly lz : L℧ ⟨ d ⟩) ->
+           lx ≾' ly -> ly ≾' lz -> lx ≾' lz) ->
+        (lx ly lz : L℧ ⟨ d ⟩) ->
+          lx ≾' ly -> ly ≾' lz -> lx ≾' lz
+    trans-ind IH ℧ ly lz lx≤ly ly≤lz = tt
+    trans-ind IH (η x) (η y) (η z) lx≤ly ly≤lz =
+      IsPoset.is-trans D.isPoset x y z lx≤ly ly≤lz
+
+    trans-ind IH lx ℧ lz = {!!} -- not possible unless x is ℧
+    trans-ind IH lx ly ℧ = {!!} -- not possible unless lx and ly are ℧
+
+    trans-ind IH (θ lx~) (θ ly~) (θ lz~) = {!!} -- follows by induction
+    {-
+      λ t -> transport (sym λ i → unfold-ord i (lx~ t) (lz~ t))
+          (IH t (lx~ t) (ly~ t) (lz~ t)
+          (transport (λ i -> unfold-ord i (lx~ t) (ly~ t)) (ord-ab t))
+          (transport (λ i -> unfold-ord i (ly~ t) (lz~ t)) (ord-bc t)))
+
+    -}
+
+    
+    trans-ind IH (η x) (θ ly~) (η z) (n , y' , H-eq-δ , H-y'≤z) (m , inl H-℧) =
+      {!-- contradiction: θ ly~ ≡ δ^m ℧ and also ≡ δ^n (η y')!}
+    trans-ind IH (η x) (θ ly~) (η z)
+      (n , y' , H-eq-δ1 , H-y'≤z)
+      (m , inr (y'' , H-eq-δ2 , H-y''≤z)) =
+      {! -- we have m ≡ n and y'== y'', so x ≤ z by transitivity!}
+
+    trans-ind IH (η x) (θ ly~) (θ lz~) (n , y' , H-eq-δ , H-x≤y') ly≤lz =
+      let (m , y'' , eq) = lem3 ly~ lz~ n y' ly≤lz H-eq-δ in {!!}
+
+    trans-ind IH (θ lx~) (θ ly~) (η z) lx≤ly ly≤lz = {!!}
+
+    trans-ind IH (θ lx~) (η y) (θ lz~) lx≤ly ly≤lz = {!!}
+-}
+
+
+
+-- Extensional relation (two terms are error-related "up to thetas")
+module ExtRel (d : Predomain) where
+
+  open Bisimilarity d
+  open 𝕃 d
+
+  _⊴_ : L℧ ⟨ d ⟩ -> L℧ ⟨ d ⟩ -> Type
+  x ⊴ y = Σ (L℧ ⟨ d ⟩) λ p -> Σ (L℧ ⟨ d ⟩) λ q ->
+    (x ≈ p) × (p ≾ q) × (q ≈ y)
+
 
 
 
@@ -797,4 +1186,129 @@ module WeakRel (d : ErrorDomain) where
   _≾_ = fix _≾'_
     where open Inductive
 
+-}
+
+{-
+
+
+Lemma A:
+
+If lx ≈ ly and ly ≡ δ^n (℧), then
+lx = δ^m (℧) for some m ≥ 0.
+
+Proof. By induction on n.
+
+  First note that if lx ≡ ℧, then we are finished (taking m = 0).
+  If lx ≡ η x', this contradicts the assumption that lx ≈ δ^n (℧).
+
+  Hence, we may assume lx = (θ lx~). By definition of the relation, we have
+
+    ▸t [lx~ t ≈ δ^(n-1) (℧)],
+
+  so by induction, we have lx~ t ≡ δ^m (℧) for some m,
+  and thus lx~ ≡ δ^(m+1) (℧)
+
+
+
+Lemma B:
+
+If lx ≈ ly and 
+
+
+
+Claim: The weak bisimulation relation is transitive,
+
+i.e. if lx ≈ ly ≈ lz, then lx ≈ lz.
+
+Proof.
+
+By Lob induction.
+Consider cases on lx, ly, and lz.
+
+
+Case η x ≈ η y ≈ η z:
+  We have x ≤ y ≤ z, so by transitivity of the underlying relation we
+  have x ≤ z, so η x ≈ η z
+
+Case ℧ ≈ ly ≈ lz:
+  Trivial by definition of the relation.
+
+Case ly = ℧ or lz = ℧:
+  Impossible by definition of the relation.
+
+Case (θ lx~) ≈ (θ ly~) ≈ (θ lz~):
+  By definition of the relation, STS that
+  ▸t [(lx~ t) ≈ (lz~ t)]
+
+  We know
+  ▸t [(lx~ t) ≈ (ly~ t)] and
+  ▸t [(ly~ t) ≈ (lz~ t)],
+
+  so the conclusion follows by the IH.
+
+
+          (1)       (2)
+Case (η x) ≈ (θ ly~) ≈ (η z):
+
+  By (2), we have that either
+  (θ ly~) ≡ δ^n ℧ or (θ ly~) ≡ δ^n (η y') where y' ≤ z.
+
+  But by (1), we have (θ ly~) ≡ δ^n (η y') where x ≤ y'.
+  Thus the second case above must hold, and we have by
+  transitivity of the underlying relation that x ≤ z,
+  so (η x) ≈ (η z).
+
+
+          (1)       (2)
+Case (η x) ≈ (θ ly~) ≈ (θ lz~):
+
+  
+
+
+            (1)     (2)
+Case (θ lx~) ≈ (η y) ≈ (θ lz~):
+
+  We need to show that
+
+    ▸t [(lx~ t) ≈ (lz~ t)].
+
+  By (1), either (θ lx~) ≡ δ^n (℧) for some n ≥ 1, or
+  (θ lx~) ≡ δ^n (η x') where x' ≤ y.
+
+  By (2), (θ lz~) ≡ δ^m (η z') for some m ≥ 1 and y ≤ z'.
+
+  Suppose n ≤ m. Then after n "steps" of unfolding thetas
+  on both sides, we will be left with either ℧ or η x' on the left,
+  and δ^(m-n)(η z') on the right.
+  In the former case we are finished since ℧ is the bottom element,
+  and in the latter case we can use transitivity of the underlying
+  relation to conclude x' ≤ z' and hence η x' ≈ δ^(m-n)(η z').
+
+  Now suppose n > m. Then after m steps of unfolding,
+  we will be left with either δ^(n-m)(℧) or δ(n-m)(η x') on the left,
+  and η z' on the right.
+  In the former case we are finished by definition of the relation.
+  In the latter case we again use transitivity of the underlying relation.
+  
+
+
+            (1)       (2)
+Case (θ lx~) ≈ (θ ly~) ≈ (η z):
+
+  By (2), either (θ ly~) ≡ δ^n (℧), or
+  (θ ly~) ≡ δ^n (η y') where y' ≤ z.
+
+  In the former case, (1) and Lemma A imply that
+  (θ lx~) ≡ δ^m (℧) for some m, and we are finished
+  by definiton of the relation.
+
+  In the latter case, (1) and Lemma B imply that
+  (θ lx~) ≡ δ^m (η x') for some m and some x'
+  with x' ≤ y'.
+  Then by transitivity of the underlying relation
+  we have x' ≤ z, so we are finished.
+
+
+
+
 -}
diff --git a/formalizations/guarded-cubical/SyntacticTermPrecision.agda b/formalizations/guarded-cubical/SyntacticTermPrecision.agda
new file mode 100644
index 0000000000000000000000000000000000000000..ee17a0c1e55226cffb8fcdfbeea4ae08709556ff
--- /dev/null
+++ b/formalizations/guarded-cubical/SyntacticTermPrecision.agda
@@ -0,0 +1,170 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Later
+
+module SyntacticTermPrecision (k : Clock) where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat
+open import Cubical.Relation.Nullary
+
+open import ErrorDomains k
+open import GradualSTLC
+
+---- Syntactic term precision relation ----
+
+-- Make this a sigma type
+data CtxTyPrec : Set where
+  · : CtxTyPrec
+  _::_ : {A B : Ty} -> CtxTyPrec -> A ⊑ B -> CtxTyPrec
+
+
+infixr 5 _::_
+
+Ctx-ref : Ctx -> CtxTyPrec
+Ctx-ref · = ·
+Ctx-ref (Γ :: x) = Ctx-ref Γ :: ⊑ref x
+
+
+lhs-ty : {A B : Ty} -> A ⊑ B -> Ty
+lhs-ty {A} d = A
+
+rhs-ty : {A B : Ty} -> A ⊑ B -> Ty
+rhs-ty {_} {B} d = B
+
+lhs : CtxTyPrec -> Ctx
+lhs · = ·
+lhs (ctx :: d) = (lhs ctx) :: lhs-ty d
+
+rhs : CtxTyPrec -> Ctx
+rhs · = ·
+rhs (ctx :: d) = (rhs ctx) :: rhs-ty d
+
+
+lem-lhs : (A : Ty) -> A ≡ lhs-ty (⊑ref A)
+lem-lhs A = refl
+
+lem-rhs : (A : Ty) -> A ≡ rhs-ty (⊑ref A)
+lem-rhs A = refl
+
+
+ctx-refl-lhs : (Γ : Ctx) -> Γ ≡ lhs (Ctx-ref Γ)
+ctx-refl-lhs · = refl
+ctx-refl-lhs (Γ :: x) = λ i -> ctx-refl-lhs Γ i :: lem-lhs x i
+
+ctx-refl-rhs : (Γ : Ctx) -> Γ ≡ rhs (Ctx-ref Γ)
+ctx-refl-rhs · = refl
+ctx-refl-rhs (Γ :: x) = λ i -> ctx-refl-rhs Γ i :: lem-rhs x i
+
+iso-L : {Γ : Ctx} {A : Ty} -> Tm Γ A -> Tm (lhs (Ctx-ref Γ)) A
+iso-L {Γ} {A} M = transport (λ i → Tm (ctx-refl-lhs Γ i) A) M
+
+iso-R : {Γ : Ctx} {A : Ty} -> Tm Γ A -> Tm (rhs (Ctx-ref Γ)) A
+iso-R {Γ} {A} M = transport (λ i -> Tm (ctx-refl-rhs Γ i) A) M
+
+
+TmL : {A B : Ty} -> CtxTyPrec -> A ⊑ B -> Set
+TmL ctx d = {!!}
+
+
+-- "Contains" relation stating that a context Γ contains a type T
+
+data _∋'_ : {A B : Ty} -> CtxTyPrec -> A ⊑ B -> Set where
+
+infix 4 _∋'_
+
+contains-lhs : {A B : Ty} ->
+  (Γ : CtxTyPrec) (d : A ⊑ B) -> (Γ ∋' d) -> (lhs Γ ∋ A)
+contains-lhs = {!!}
+
+contains-rhs : {A B : Ty} ->
+  (Γ : CtxTyPrec) (d : A ⊑ B) -> (Γ ∋' d) -> (rhs Γ ∋ B)
+contains-rhs = {!!}
+
+
+
+
+-- d is fixed here so it should be a parameter, not an index
+-- (hence why it doesn't appear after M and N)
+data ltdyn-tm :
+  {A B : Ty} ->
+  (Γ : CtxTyPrec) ->
+  (d : A ⊑ B) ->
+  (M : Tm (lhs Γ) A) ->
+  (N : Tm (rhs Γ) B) -> Set where
+
+  -- err
+  err : {A B : Ty} -> (Γ : CtxTyPrec) -> (d : A ⊑ B) -> (N : Tm (rhs Γ) B) -> ltdyn-tm Γ d err N
+
+  ---- *Congruence rules* ----
+
+  -- variables
+  -- var : {!{A B : Ty} -> (Γ : CtxTyPrec) -> (d : A ⊑ B) -> (Γ ∋' d) -> ?!}
+  var : (A B : Ty) ->
+        (Γ : CtxTyPrec) ->
+        (d : A ⊑ B) ->
+        (x : Γ ∋' d) ->
+        ltdyn-tm Γ d (var (contains-lhs Γ d x)) (var (contains-rhs Γ d x))
+
+  -- natural numbers
+  zro : (Γ : CtxTyPrec) -> ltdyn-tm Γ nat zro zro
+  suc : (Γ : CtxTyPrec) (M : Tm (lhs Γ) nat) (M' : Tm (rhs Γ) nat) ->
+        ltdyn-tm Γ nat M M' ->
+        ltdyn-tm Γ nat (suc M) (suc M')
+
+  -- lambdas
+  lda : (Γ : CtxTyPrec) (A A' B B' : Ty)
+        (c : A ⊑ A') (d : B ⊑ B')
+        (M1 : Tm ((lhs Γ) :: A) B) (M2 : Tm ((rhs Γ) :: A') B') ->
+        ltdyn-tm (Γ :: c) d M1 M2 ->
+        ltdyn-tm Γ (c => d) (lda M1) (lda M2)
+
+  -- application
+  app : (Γ : CtxTyPrec) (Ain Bin Aout Bout : Ty)
+        (din : Ain ⊑ Bin) (dout : Aout ⊑ Bout)
+        (M1 : Tm (lhs Γ) (Ain => Aout)) (N1 : Tm (lhs Γ) Ain)
+        (M2 : Tm (rhs Γ) (Bin => Bout)) (N2 : Tm (rhs Γ) Bin) ->
+        ltdyn-tm Γ (din => dout) M1 M2 ->
+        ltdyn-tm Γ din N1 N2 ->
+        ltdyn-tm Γ dout (app M1 N1) (app M2 N2)
+    
+
+  ---- *Cast rules* ----
+  
+  upR : (Γ : Ctx) (A B : Ty)
+        (c : A ⊑ B)
+        --(M : Tm (lhs Γ) A)
+        (N : Tm Γ A) ->
+     --   ltdyn-tm Γ (⊑ref A) N N ->
+     ltdyn-tm (Ctx-ref Γ) c (iso-L N) (up c (iso-R N))
+     --   ltdyn-tm (Ctx-ref Γ) c N (up c N)
+
+  upL : (Γ : CtxTyPrec) (A B : Ty)
+        (c : A ⊑ B)
+        (M : Tm (lhs Γ) A)
+        (N : Tm (rhs Γ) B) ->
+        ltdyn-tm Γ c M N ->
+        ltdyn-tm Γ (⊑ref B) (up c M) N
+  
+  dnL : (Γ : Ctx) (A B : Ty)
+        (c : A ⊑ B)
+        (M : Tm Γ B) ->
+       --  (N : Tm (rhs Γ) B) ->
+       --  ltdyn-tm Γ (⊑ref B) M N ->
+       ltdyn-tm (Ctx-ref Γ) c (dn c (iso-L M)) (iso-R M)
+        -- ltdyn-tm Γ c (dn c M) M
+
+  dnR : (Γ : CtxTyPrec) (A B : Ty)
+        (c : A ⊑ B)
+        (M : Tm (lhs Γ) A)
+        (N : Tm (rhs Γ) B) ->
+        ltdyn-tm Γ c M N ->
+        ltdyn-tm Γ (⊑ref A) M (dn c N)
+
+
+-- Notation that matches the written syntax, with d appearing at the end
+_|-_⊑tm_#_ : {A B : Ty} -> (Γ : CtxTyPrec) -> (Tm (lhs Γ) A) -> (Tm (rhs Γ) B) -> A ⊑ B -> Set
+Γ |- M ⊑tm N # d = ltdyn-tm Γ d M N