diff --git a/formalizations/guarded-cubical/Results/Coinductive.agda b/formalizations/guarded-cubical/Results/Coinductive.agda
index d5e19891ce52f8d7dd15891d337d462acd8988bc..ae807c3f624b9d7650c4949573d3de16bbe5589f 100644
--- a/formalizations/guarded-cubical/Results/Coinductive.agda
+++ b/formalizations/guarded-cubical/Results/Coinductive.agda
@@ -15,8 +15,12 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Structure
 open import Cubical.Data.Empty
 
-open import Results.IntensionalAdequacy
+open import Semantics.Predomains
 open import Semantics.StrongBisimulation
+open import Semantics.Lift
+
+open import Results.IntensionalAdequacy
+
 
 private
   variable
@@ -178,7 +182,7 @@ module _ {X : Type} (H-irrel : clock-irrel X) where
 
 
 -- Bisimilarity relation on Machines.
-module Bisim (X : Predomain k0) (H-irrel : clock-irrel ⟨ X ⟩) where
+module Bisim (X : Predomain) (H-irrel : clock-irrel ⟨ X ⟩) where
 
 
   -- Mutually define coinductive bisimilarity of machines
@@ -188,7 +192,7 @@ module Bisim (X : Predomain k0) (H-irrel : clock-irrel ⟨ X ⟩) where
   record _≋_ (m m' : Machine ⟨ X ⟩) : Type
 
   _≋''_ : State ⟨ X ⟩ -> State ⟨ X ⟩ -> Type
-  result x ≋'' result x' = rel k0 X x x'
+  result x ≋'' result x' = rel X x x'
   error ≋'' error = ⊤
   running m ≋'' running m' = m ≋ m' -- using the coinductive bisimilarity on machines
   _ ≋'' _ = ⊥
diff --git a/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda b/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda
index 7b4a0d6e408b40fb91ba78926347827a316ea1d3..dcb58df3e78a1075b4085cf5b3287d5403ecd388 100644
--- a/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda
+++ b/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda
@@ -26,10 +26,12 @@ open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Function
 
 import Semantics.StrongBisimulation
-import Common.MonFuns
+import Semantics.Monotone.Base
 import Syntax.GradualSTLC
 
 open import Common.Common
+open import Semantics.Predomains
+open import Semantics.Lift
 
 -- TODO move definition of Predomain to a module that
 -- isn't parameterized by a clock!
@@ -199,7 +201,7 @@ module AdequacyLockstep
   open Semantics.StrongBisimulation
   open Semantics.StrongBisimulation.LiftPredomain
 
-  _≾-gl_ : {p : Predomain k0} -> (L℧F ⟨ p ⟩) -> (L℧F ⟨ p ⟩) -> Type
+  _≾-gl_ : {p : Predomain} -> (L℧F ⟨ p ⟩) -> (L℧F ⟨ p ⟩) -> Type
   _≾-gl_ {p} lx ly = ∀ (k : Clock) -> _≾_ k p (lx k) (ly k)
 
   -- _≾'_ : {k : Clock} -> L℧ k Nat → L℧ k Nat → Type
@@ -299,7 +301,7 @@ module AdequacyBisim where
 
 
   -- Some properties of the global bisimilarity relation
-  module GlobalBisim (p : Predomain k0) where
+  module GlobalBisim (p : Predomain) where
 
     _≈-gl_ : (L℧F ⟨ p ⟩) -> (L℧F ⟨ p ⟩) -> Type
     _≈-gl_ lx ly = ∀ (k : Clock) -> _≈_ k p (lx k) (ly k)
diff --git a/formalizations/guarded-cubical/Semantics/ErrorDomains.agda b/formalizations/guarded-cubical/Semantics/ErrorDomains.agda
new file mode 100644
index 0000000000000000000000000000000000000000..89c6f66f7e1ba4f24ee44b0c8c1a18f2ca271626
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/ErrorDomains.agda
@@ -0,0 +1,69 @@
+
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Common.Later
+
+module Semantics.ErrorDomains (k : Clock) where
+
+open import Cubical.Relation.Binary.Poset
+open import Cubical.Foundations.Structure
+
+open import Semantics.Predomains
+open import Cubical.Data.Sigma
+
+
+open import Semantics.Monotone.Base
+
+-- Error domains
+
+record ErrorDomain : Set₁ where
+  field
+    X : Predomain
+  module X = PosetStr (X .snd)
+  _≤_ = X._≤_
+  field
+    ℧ : X .fst
+    ℧⊥ : ∀ x → ℧ ≤ x
+    θ : MonFun (▸''_ k X) X
+
+
+-- Underlying predomain of an error domain
+
+𝕌 : ErrorDomain -> Predomain
+𝕌 d = ErrorDomain.X d
+
+{-
+arr : Predomain -> ErrorDomain -> ErrorDomain
+arr dom cod =
+  record {
+    X = arr' dom (𝕌 cod) ;
+    ℧ = const-err ;
+    ℧⊥ = const-err-bot ;
+    θ = {!!} }
+    where
+       -- open LiftOrder
+       const-err : ⟨ arr' dom (𝕌 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)
+-}
+
+
+{-
+-- Predomain to lift Error Domain
+
+𝕃℧ : Predomain → ErrorDomain
+𝕃℧ X = record {
+  X = 𝕃 X ; ℧ = ℧ ; ℧⊥ = ord-bot X ;
+  θ = record { f = θ ; isMon = λ t -> {!!} } }
+  where
+    -- module X = PosetStr (X .snd)
+    -- open Relation X
+    open LiftPredomain
+-}
diff --git a/formalizations/guarded-cubical/Semantics/Lift.agda b/formalizations/guarded-cubical/Semantics/Lift.agda
new file mode 100644
index 0000000000000000000000000000000000000000..9b45cc8f0ea4c65382426676e1be43b878644e52
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Lift.agda
@@ -0,0 +1,127 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Common.Later
+
+module Semantics.Lift (k : Clock) where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Empty hiding (rec)
+
+private
+  variable
+    l : Level
+    A B : Set l
+private
+  ▹_ : Set l → Set l
+  â–¹_ A = â–¹_,_ k A
+
+
+  -- Lift monad
+
+data L℧ (X : Set) : Set where
+  η : X → L℧ X
+  ℧ : L℧ X
+  θ : ▹ (L℧ X) → L℧ X
+
+
+-- Delay function
+δ : {X : Type} -> L℧ X -> L℧ X
+δ = θ ∘ next
+
+-- 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~)
+
+
+-- TODO: 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~
+
+
+-- TODO: This 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 = η
+
+
+ext' : (A -> L℧ B) -> ▹ (L℧ A -> L℧ B) -> L℧ A -> L℧ B
+ext' f rec (η x) = f x
+ext' f rec ℧ = ℧
+ext' f rec (θ l-la) = θ (rec ⊛ l-la)
+
+ext : (A -> L℧ B) -> L℧ A -> L℧ B
+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)
+
+
+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~
+
diff --git a/formalizations/guarded-cubical/Semantics/Monotone/Base.agda b/formalizations/guarded-cubical/Semantics/Monotone/Base.agda
new file mode 100644
index 0000000000000000000000000000000000000000..686421606fd2e7a75f374f207e086227ef79273a
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Monotone/Base.agda
@@ -0,0 +1,82 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+
+module Semantics.Monotone.Base where
+
+open import Cubical.Relation.Binary.Poset
+open import Cubical.Data.Sigma
+open import Cubical.Foundations.Structure
+
+open import Semantics.Predomains
+
+private
+  variable
+    â„“ : Level
+
+-- Monotone functions from X to Y
+record MonFun (X Y : Predomain) : Set where
+  module X = PosetStr (X .snd)
+  module Y = PosetStr (Y .snd)
+  _≤X_ = X._≤_
+  _≤Y_ = Y._≤_
+  field
+    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' }
+
+
+compRel : {X Y Z : Type} ->
+  (R1 : Y -> Z -> Type â„“) ->
+  (R2 : X -> Y -> Type â„“) ->
+  (X -> Z -> Type â„“)
+compRel {ℓ} {X} {Y} {Z} R1 R2 x z = Σ[ y ∈ Y ] R2 x y × R1 y z
+
+CompMonRel : {X Y Z : Predomain} ->
+  MonRel {â„“} Y Z ->
+  MonRel {â„“} X Y ->
+  MonRel {â„“} X Z
+CompMonRel {â„“} {X} {Y} {Z} R1 R2 = record {
+  R = compRel (MonRel.R R1) (MonRel.R R2) ;
+  isAntitone = antitone ;
+  isMonotone = {!!} }
+    where
+      antitone : {x x' : ⟨ X ⟩} {z : ⟨ Z ⟩} ->
+        compRel (MonRel.R R1) (MonRel.R R2) x z ->
+        rel X x' x ->
+        compRel (MonRel.R R1) (MonRel.R R2) x' z 
+      antitone (y , xR2y , yR1z) x'≤x = y , (MonRel.isAntitone R2 xR2y x'≤x) , yR1z
+
+      monotone : {x : ⟨ X ⟩} {z z' : ⟨ Z ⟩} ->
+        compRel (MonRel.R R1) (MonRel.R R2) x z ->
+        rel Z z z' ->
+        compRel (MonRel.R R1) (MonRel.R R2) x z'
+      monotone (y , xR2y , yR1z) z≤z' = y , xR2y , (MonRel.isMonotone R1 yR1z z≤z')
diff --git a/formalizations/guarded-cubical/Semantics/Monotone/Lemmas.agda b/formalizations/guarded-cubical/Semantics/Monotone/Lemmas.agda
new file mode 100644
index 0000000000000000000000000000000000000000..15e0791a0b5fafce49ed45b8e94965f9552c9d4a
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Monotone/Lemmas.agda
@@ -0,0 +1,403 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Common.Later
+
+module Semantics.Monotone.Lemmas (k : Clock) where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat renaming (â„• to Nat) hiding (_^_)
+
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Binary.Poset
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Transport
+
+open import Cubical.Data.Unit
+open import Cubical.Data.Sigma
+open import Cubical.Data.Empty
+
+open import Cubical.Foundations.Function
+
+open import Semantics.Predomains
+open import Semantics.Lift k
+open import Semantics.Monotone.Base
+open import Semantics.StrongBisimulation k
+open import Syntax.GradualSTLC
+open import Syntax.SyntacticTermPrecision k
+
+private
+  variable
+    l : Level
+    A B : Set l
+private
+  ▹_ : Set l → Set l
+  â–¹_ A = â–¹_,_ k A
+
+open LiftPredomain
+
+{-
+test : (A B : Type) -> (eq : A ≡ B) -> (x : A) -> (T : (A : Type) -> A -> Type) ->
+ (T A x) -> (T B (transport eq x))
+test A B eq x T Tx = transport (λ i -> T (eq i) (transport-filler eq x i)) Tx
+
+-- transport (λ i -> T (eq i) ?) Tx
+-- Goal : eq i
+-- Constraints:
+-- x = ?8 (i = i0) : A
+-- ?8 (i = i1) = transp (λ i₁ → eq i₁) i0 x : B
+
+
+-- transport-filler : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) (x : A)
+--                   → PathP (λ i → p i) x (transport p x)
+                   
+
+test' : (A B : Predomain) -> (S : Type) ->
+ (eq : A ≡ B)  ->
+ (x : ⟨ A ⟩) ->
+ (T : (A : Predomain) -> ⟨ A ⟩ -> Type) ->
+ (T A x) -> T B (transport (λ i -> ⟨ eq i ⟩) x)
+test' A B S eq x T Tx = transport
+  (λ i -> T (eq i) (transport-filler (λ j → ⟨ eq j ⟩) x i))
+  Tx
+-}
+
+
+-- If A ≡ B, then we can translate knowledge about a relation on A
+-- to its image in B obtained by transporting the related elements of A
+-- along the equality of the underlying sets of A and B
+rel-transport :
+  {A B : Predomain} ->
+  (eq : A ≡ B) ->
+  {a1 a2 : ⟨ A ⟩} ->
+  rel A a1 a2 ->
+  rel B
+    (transport (λ i -> ⟨ eq i ⟩) a1)
+    (transport (λ i -> ⟨ eq i ⟩) a2)
+rel-transport {A} {B} eq {a1} {a2} a1≤a2 =
+  transport (λ i -> rel (eq i)
+    (transport-filler (λ j -> ⟨ eq j ⟩) a1 i)
+    (transport-filler (λ j -> ⟨ eq j ⟩) a2 i))
+  a1≤a2
+
+rel-transport-sym : {A B : Predomain} ->
+  (eq : A ≡ B) ->
+  {b1 b2 : ⟨ B ⟩} ->
+  rel B b1 b2 ->
+  rel A
+    (transport (λ i → ⟨ sym eq i ⟩) b1)
+    (transport (λ i → ⟨ sym eq i ⟩) b2)
+rel-transport-sym eq {b1} {b2} b1≤b2 = rel-transport (sym eq) b1≤b2
+
+
+mTransport : {A B : Predomain} -> (eq : A ≡ B) -> ⟨ A ==> B ⟩
+mTransport {A} {B} eq = record {
+  f = λ b → transport (λ i -> ⟨ eq i ⟩) b ;
+  isMon = λ {b1} {b2} b1≤b2 → rel-transport eq b1≤b2 }
+
+
+mTransportSym : {A B : Predomain} -> (eq : A ≡ B) -> ⟨ B ==> A ⟩
+mTransportSym {A} {B} eq = record {
+  f = λ b → transport (λ i -> ⟨ sym eq i ⟩) b ;
+  isMon = λ {b1} {b2} b1≤b2 → rel-transport (sym eq) b1≤b2 }
+
+
+-- Transporting the domain of a monotone function preserves monotonicity
+mon-transport-domain : {A B C : Predomain} ->
+  (eq : A ≡ B) ->
+  (f : MonFun A C) ->
+  {b1 b2 : ⟨ B ⟩} ->
+  (rel B b1 b2) ->
+  rel C
+    (MonFun.f f (transport (λ i → ⟨ sym eq i ⟩ ) b1))
+    (MonFun.f f (transport (λ i → ⟨ sym eq i ⟩ ) b2))
+mon-transport-domain eq f {b1} {b2} b1≤b2 =
+  MonFun.isMon f (rel-transport (sym eq) b1≤b2)
+
+mTransportDomain : {A B C : Predomain} ->
+  (eq : A ≡ B) ->
+  MonFun A C ->
+  MonFun B C
+mTransportDomain {A} {B} {C} eq f = record {
+  f = g eq f;
+  isMon = mon-transport-domain eq f }
+  where
+    g : {A B C : Predomain} ->
+      (eq : A ≡ B) ->
+      MonFun A C ->
+      ⟨ B ⟩ -> ⟨ C ⟩
+    g eq f b = MonFun.f f (transport (λ i → ⟨ sym eq i ⟩ ) b)
+
+
+
+
+
+
+-- rel (𝕃 B) (ext f la) (ext f' la') ≡ _A_1119
+-- ord (ext f la) (ext f' la') ≡ 
+-- ord' (next ord) (ext' f (next (ext f)) la) (ext' f (next (ext f)) la')
+
+
+-- ext respects monotonicity, in a general, heterogeneous sense
+ext-monotone-het : {A A' B B' : Predomain} ->
+  (rAA' : ⟨ A ⟩ -> ⟨ A' ⟩ -> Type) -> (rBB' : ⟨ B ⟩ -> ⟨ B' ⟩ -> Type) ->
+  (f : ⟨ A ⟩ -> ⟨ (𝕃 B) ⟩) -> (f' : ⟨ A' ⟩ -> ⟨ (𝕃 B') ⟩) ->
+  fun-order-het A A' (𝕃 B) (𝕃 B') rAA' (LiftRelation._≾_ B B' rBB') f f' ->
+  (la : ⟨ 𝕃 A ⟩) -> (la' : ⟨ 𝕃 A' ⟩) ->
+  (LiftRelation._≾_ A A' rAA' la la') ->
+  LiftRelation._≾_ B B' rBB' (ext f la) (ext f' la')
+ext-monotone-het {A} {A'} {B} {B'} rAA' rBB' f f' f≤f' la la' la≤la' =
+  let fixed = fix (monotone-ext') in
+  transport
+    (sym (λ i -> LiftBB'.unfold-≾ i (unfold-ext f i la) (unfold-ext f' i la')))
+    (fixed la la' (transport (λ i → LiftAA'.unfold-≾ i la la') la≤la'))
+  where
+
+
+    -- Note that these four have already been
+    -- passed (next _≾_) as a parameter (this happened in
+    -- the defintion of the module 𝕃, where we said
+    -- open Inductive (next _≾_) public)
+    _≾'LA_  = LiftPredomain._≾'_ A
+    _≾'LA'_ = LiftPredomain._≾'_ A'
+    _≾'LB_  = LiftPredomain._≾'_ B
+    _≾'LB'_ = LiftPredomain._≾'_ B'
+
+    module LiftAA' = LiftRelation A A' rAA'
+    module LiftBB' = LiftRelation B B' rBB'
+
+    -- The heterogeneous lifted relations
+    _≾'LALA'_ = LiftAA'.Inductive._≾'_ (next LiftAA'._≾_)
+    _≾'LBLB'_ = LiftBB'.Inductive._≾'_ (next LiftBB'._≾_)
+    
+
+    monotone-ext' :
+      â–¹ (
+          (la : ⟨ 𝕃 A ⟩) -> (la' : ⟨ 𝕃 A' ⟩)  ->
+          (la ≾'LALA' la') ->
+          (ext' f  (next (ext f))  la) ≾'LBLB'
+          (ext' f' (next (ext f')) la')) ->
+       (la : ⟨ 𝕃 A ⟩) -> (la' : ⟨ 𝕃 A' ⟩)  ->
+          (la ≾'LALA' la') ->
+          (ext' f  (next (ext f))  la) ≾'LBLB'
+          (ext' f' (next (ext f')) la')
+    monotone-ext' IH (η x) (η y) x≤y =
+      transport
+      (λ i → LiftBB'.unfold-≾ i (f x) (f' y))
+      (f≤f' x y x≤y)
+    monotone-ext' IH ℧ la' la≤la' = tt
+    monotone-ext' IH (θ lx~) (θ ly~) la≤la' = λ t ->
+      transport
+        (λ i → (sym (LiftBB'.unfold-≾)) i
+          (sym (unfold-ext f) i (lx~ t))
+          (sym (unfold-ext f') i (ly~ t)))
+        (IH t (lx~ t) (ly~ t)
+          (transport (λ i -> LiftAA'.unfold-≾ i (lx~ t) (ly~ t)) (la≤la' t)))
+
+
+
+-- ext respects monotonicity (in the usual homogeneous sense)
+-- This can be rewritten to reuse the above result!
+ext-monotone : {A B : Predomain} ->
+  (f f' : ⟨ A ⟩ -> ⟨ (𝕃 B) ⟩) ->
+  fun-order A (𝕃 B) f f' ->
+  (la la' : ⟨ 𝕃 A ⟩) ->
+  rel (𝕃 A) la la' ->
+  rel (𝕃 B) (ext f la) (ext f' la')
+ext-monotone {A} {B} f f' f≤f' la la' la≤la' =
+  let fixed = fix (monotone-ext' f f' f≤f') in
+  transport
+    (sym (λ i -> unfold-≾ B i (unfold-ext f i la) (unfold-ext f' i la')))
+    (fixed la la' (transport (λ i → unfold-≾ A i la la') la≤la'))
+  where
+
+    -- bring the homogeneous lifted relations into scope
+    _≾LA_ = LiftPredomain._≾_ A
+    _≾LB_ = LiftPredomain._≾_ B
+
+    -- Note that these next two have already been
+    -- passed (next _≾_) as a parameter (this happened in
+    -- the defintion of the module 𝕃, where we said
+    -- open Inductive (next _≾_) public)
+    _≾'LA_ = LiftPredomain._≾'_ A
+    _≾'LB_ = LiftPredomain._≾'_ B
+
+    monotone-ext' :
+      (f f' : ⟨ A ⟩ -> ⟨ (𝕃 B) ⟩) ->
+      (fun-order A (𝕃 B) f f') ->
+      â–¹ (
+        (la la' : ⟨ 𝕃 A ⟩) ->
+          la ≾'LA la' ->
+          (ext' f  (next (ext f))  la) ≾'LB
+          (ext' f' (next (ext f')) la')) ->
+     (la la' : ⟨ 𝕃 A ⟩) ->
+        la ≾'LA la' ->
+        (ext' f  (next (ext f))  la) ≾'LB
+        (ext' f' (next (ext f')) la')
+    monotone-ext' f f' f≤f' IH (η x) (η y) x≤y =
+      transport
+      (λ i → unfold-≾ B i (f x) (f' y))
+      (f≤f' x y x≤y)
+    monotone-ext' f f' f≤f' IH ℧ la' la≤la' = tt
+    monotone-ext' f f' f≤f' IH (θ lx~) (θ ly~) la≤la' = λ t ->
+      transport
+        (λ i → (sym (unfold-≾ B)) i
+          (sym (unfold-ext f) i (lx~ t))
+          (sym (unfold-ext f') i (ly~ t)))
+        (IH t (lx~ t) (ly~ t)
+          (transport (λ i -> unfold-≾ A i (lx~ t) (ly~ t)) (la≤la' t)))
+
+
+
+{-
+ext-monotone' : {A B : Predomain} ->
+  {la la' : ⟨ 𝕃 A ⟩} ->
+  (f f' : ⟨ A ⟩ -> ⟨ (𝕃 B) ⟩) ->
+  rel (𝕃 A) la la' ->
+  fun-order A (𝕃 B) f f' ->
+  rel (𝕃 B) (ext f la) (ext f' la')
+ext-monotone' {A} {B} {la} {la'} f f' la≤la' f≤f' =
+  let fixed = fix (monotone-ext' f f' f≤f') in
+  --transport
+    --(sym (λ i -> ord B (unfold-ext f i la) (unfold-ext f' i la')))
+    (fixed la la' (transport (λ i → unfold-ord A i la la') la≤la'))
+  where
+    monotone-ext' :
+      (f f' : ⟨ A ⟩ -> ⟨ (𝕃 B) ⟩) ->
+      (fun-order A (𝕃 B) f f') ->
+      â–¹ (
+        (la la' : ⟨ 𝕃 A ⟩) ->
+         ord' A (next (ord A)) la la' ->
+         ord B
+          (ext f  la)
+          (ext f' la')) ->
+     (la la' : ⟨ 𝕃 A ⟩) ->
+       ord' A (next (ord A)) la la' ->
+       ord B
+        (ext f  la)
+        (ext f' la')
+    monotone-ext' f f' f≤f' IH (η x) (η y) x≤y = {!!} -- (f≤f' x y x≤y)
+    monotone-ext' f f' f≤f' IH ℧ la' la≤la' = transport (sym (λ i -> unfold-ord B i (ext f ℧) (ext f' la'))) {!!}
+      -- transport (sym (λ i → unfold-ord B i (ext' f (next (ext f)) ℧) (ext' f' (next (ext f')) la'))) tt
+    monotone-ext' f f' f≤f' IH (θ lx~) (θ ly~) la≤la' = {!!} -- λ t -> ?
+-}
+
+
+bind-monotone : {A B : Predomain} ->
+  {la la' : ⟨ 𝕃 A ⟩} ->
+  (f f' : ⟨ A ⟩ -> ⟨ (𝕃 B) ⟩) ->
+  rel (𝕃 A) la la' ->
+  fun-order A (𝕃 B) f f' ->
+  rel (𝕃 B) (bind la f) (bind la' f')
+bind-monotone {A} {B} {la} {la'} f f' la≤la' f≤f' =
+  ext-monotone f f' f≤f' la la' la≤la'
+   
+
+mapL-monotone-het : {A A' B B' : Predomain} ->
+  (rAA' : ⟨ A ⟩ -> ⟨ A' ⟩ -> Type) -> (rBB' : ⟨ B ⟩ -> ⟨ B' ⟩ -> Type) ->
+  (f : ⟨ A ⟩ -> ⟨ B ⟩) -> (f' : ⟨ A' ⟩ -> ⟨ B' ⟩) ->
+  fun-order-het A A' B B' rAA' rBB' f f' ->
+  (la : ⟨ 𝕃 A ⟩) -> (la' : ⟨ 𝕃 A' ⟩) ->
+  (LiftRelation._≾_ A A' rAA' la la') ->
+   LiftRelation._≾_ B B' rBB' (mapL f la) (mapL f' la')
+mapL-monotone-het {A} {A'} {B} {B'} rAA' rBB' f f' f≤f' la la' la≤la' =
+  ext-monotone-het rAA' rBB' (ret ∘ f) (ret ∘ f')
+    (λ a a' a≤a' → LiftRelation.Properties.ord-η-monotone B B' rBB' (f≤f' a a' a≤a'))
+    la la' la≤la'
+
+
+-- This is a special case of the above
+mapL-monotone : {A B : Predomain} ->
+  {la la' : ⟨ 𝕃 A ⟩} ->
+  (f f' : ⟨ A ⟩ -> ⟨ B ⟩) ->
+  rel (𝕃 A) la la' ->
+  fun-order A B f f' ->
+  rel (𝕃 B) (mapL f la) (mapL f' la')
+mapL-monotone {A} {B} {la} {la'} f f' la≤la' f≤f' =
+  bind-monotone (ret ∘ f) (ret ∘ f') la≤la'
+    (λ a1 a2 a1≤a2 → ord-η-monotone B (f≤f' a1 a2 a1≤a2))
+
+-- As a corollary/special case, we can consider the case of a single
+-- monotone function.
+monotone-bind-mon : {A B : Predomain} ->
+  {la la' : ⟨ 𝕃 A ⟩} ->
+  (f : MonFun A (𝕃 B)) ->
+  (rel (𝕃 A) la la') ->
+  rel (𝕃 B) (bind la (MonFun.f f)) (bind la' (MonFun.f f))
+monotone-bind-mon f la≤la' =
+  bind-monotone (MonFun.f f) (MonFun.f f) la≤la' (mon-fun-order-refl f)
+
+{-
+-- bind respects monotonicity
+
+monotone-bind : {A B : Predomain} ->
+  {la la' : ⟨ 𝕃 A ⟩} ->
+  (f f' : MonFun A (𝕃 B)) ->
+  rel (𝕃 A) la la' ->
+  rel (arr' A (𝕃 B)) f f' ->
+  rel (𝕃 B) (bind la (MonFun.f f)) (bind la' (MonFun.f f'))
+monotone-bind {A} {B} {la} {la'} f f' la≤la' f≤f' =
+  {!!}
+
+  where
+    
+    monotone-ext' :
+     
+      (f f' : MonFun A (𝕃 B)) ->
+      (rel (arr' A (𝕃 B)) f f') ->
+      â–¹ (
+        (la la' : ⟨ 𝕃 A ⟩) ->
+         ord' A (next (ord A)) la la' ->
+         ord' B (next (ord B))
+          (ext' (MonFun.f f)  (next (ext (MonFun.f f)))  la)
+          (ext' (MonFun.f f') (next (ext (MonFun.f f'))) la')) ->
+     (la la' : ⟨ 𝕃 A ⟩) ->
+       ord' A (next (ord A)) la la' ->
+       ord' B (next (ord B))
+        (ext' (MonFun.f f)  (next (ext (MonFun.f f)))  la)
+        (ext' (MonFun.f f') (next (ext (MonFun.f f'))) la')
+    monotone-ext' f f' f≤f' IH (η x) (η y) x≤y =
+      transport
+      (λ i → unfold-ord B i (MonFun.f f x) (MonFun.f f' y))
+      (f≤f' x y x≤y)
+    monotone-ext' f f' f≤f' IH ℧ la' la≤la' = tt
+    monotone-ext' f f' f≤f' IH (θ lx~) (θ ly~) la≤la' = λ t ->
+      transport
+        (λ i → (sym (unfold-ord B)) i
+          (sym (unfold-ext (MonFun.f f)) i (lx~ t))
+          (sym (unfold-ext (MonFun.f f')) i (ly~ t)))
+          --(ext (MonFun.f f) (lx~ t))
+          --(ext (MonFun.f f') (ly~ t)))
+        (IH t (lx~ t) (ly~ t)
+          (transport (λ i -> unfold-ord A i (lx~ t) (ly~ t)) (la≤la' t)))
+       --  (IH t (θ lx~) {!θ ly~!} la≤la')
+-}
+--  unfold-ord : ord ≡ ord' (next ord)
+
+
+
+-- For the η case:
+--  Goal:
+--      ord' B (λ _ → fix (ord' B)) (MonFun.f f x) (MonFun.f f' y)
+
+-- Know: (x₁ y₁ : fst A) →
+--      rel A x₁ y₁ →
+--      fix (ord' B) (MonFun.f f x₁) (MonFun.f f' y₁)
+
+
+-- For the θ case:
+-- Goal:
+--  ord B
+--      ext (MonFun.f f)) (lx~ t)
+--      ext (MonFun.f f')) (ly~ t)
+
+-- Know: IH : ...
+-- la≤la'   : (t₁ : Tick k) → fix (ord' A) (lx~ t₁) (ly~ t₁)
+
+-- The IH is in terms of ord' (i.e., ord' A (next (ord A)) la la')
+-- but the assumption la ≤ la' in the θ case is equivalent to
+-- (t₁ : Tick k) → fix (ord' A) (lx~ t₁) (ly~ t₁)
+
+
diff --git a/formalizations/guarded-cubical/Semantics/Monotone/MonFunCombinators.agda b/formalizations/guarded-cubical/Semantics/Monotone/MonFunCombinators.agda
new file mode 100644
index 0000000000000000000000000000000000000000..c019add022c8b6c0947d41150d0d9af3be53d0cc
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Monotone/MonFunCombinators.agda
@@ -0,0 +1,417 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Common.Later
+
+module Semantics.Monotone.MonFunCombinators (k : Clock) where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat renaming (â„• to Nat)
+
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Binary.Poset
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Transport
+
+open import Cubical.Data.Unit
+-- open import Cubical.Data.Prod
+open import Cubical.Data.Sigma
+open import Cubical.Data.Empty
+
+open import Cubical.Foundations.Function
+
+open import Common.Common
+
+open import Semantics.Lift k
+open import Semantics.Predomains
+open import Semantics.Monotone.Base
+open import Semantics.Monotone.Lemmas k
+
+open import Semantics.StrongBisimulation k
+
+
+private
+  variable
+    l : Level
+    A B : Set l
+private
+  ▹_ : Set l → Set l
+  â–¹_ A = â–¹_,_ k A
+
+open MonFun
+
+open LiftPredomain
+
+-- abstract
+
+-- 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 {
+    f = λ fBC →
+      record {
+        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 →
+      λ fAB1 fAB2 fAB1≤fAB2 →
+        λ a1 a2 a1≤a2 ->
+          f1≤f2 (MonFun.f fAB1 a1) (MonFun.f fAB2 a2)
+            (fAB1≤fAB2 a1 a2 a1≤a2) }
+     
+
+
+  -- 𝕃's return as a monotone function
+mRet : {A : Predomain} -> ⟨ A ==> 𝕃 A ⟩
+mRet {A} = record { f = ret ; isMon = ord-η-monotone A }
+
+
+  -- 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 {
+    f = suc ;
+    isMon = λ {n1} {n2} n1≤n2 -> λ i -> suc (n1≤n2 i) }
+
+
+  -- Combinators
+
+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 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) } -}
+
+
+_!_<*>_ : {A B : Predomain} ->
+    (Γ : Predomain) -> ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+Γ ! f <*> g = S Γ f g
+
+infixl 20 _<*>_
+
+
+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 {Γ} g = record {
+    f = λ γ →
+      record {
+        f = λ a → MonFun.f g (γ , a) ;
+        -- For a fixed γ, f as defined directly above is monotone
+        isMon = λ {a} {a'} a≤a' → MonFun.isMon g (reflexive Γ _ , a≤a') } ;
+
+    -- The outer f is monotone in γ
+    isMon = λ {γ} {γ'} γ≤γ' → λ a a' a≤a' -> MonFun.isMon g (γ≤γ' , a≤a') }
+
+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
+
+
+Swap : (Γ : Predomain) -> {A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ A ==> Γ ==> B ⟩
+Swap Γ f = record {
+    f = λ a →
+      record {
+        f = λ γ → MonFun.f (MonFun.f f γ) a ;
+        isMon = λ {γ1} {γ2} γ1≤γ2 ->
+          let fγ1≤fγ2 = MonFun.isMon f γ1≤γ2 in
+          fγ1≤fγ2 a a (reflexive _ a) } ;
+    isMon = λ {a1} {a2} a1≤a2 ->
+      λ γ1 γ2 γ1≤γ2 -> {!!} } -- γ1 γ2 γ1≤γ2 → {!!} }
+
+
+SwapPair : {A B : Predomain} -> ⟨ (A ×d B) ==> (B ×d A) ⟩
+SwapPair = record {
+  f = λ { (a , b) -> b , a } ;
+  isMon = λ { {a1 , b1} {a2 , b2} (a1≤a2 , b1≤b2) → b1≤b2 , a1≤a2} }
+
+
+-- Apply a monotone function to the first or second argument of a pair
+
+With1st : {Γ A B : Predomain} ->
+    ⟨ Γ ==> B ⟩ -> ⟨ Γ ×d A ==> B ⟩
+-- ArgIntro1 {_} {A} f = Uncurry (Swap A (K A f))
+With1st {_} {A} f = mCompU f π1
+
+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 = {!!}
+-}
+
+
+
+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 ⟩
+
+IntroArg : {Γ B B' : Predomain} ->
+  ⟨ B ==> B' ⟩ -> ⟨ (Γ ==> B) ==> (Γ ==> B') ⟩
+IntroArg f = Curry (mCompU f App)
+
+
+PairAssocLR : {A B C : Predomain} ->
+  ⟨ A ×d B ×d C ==> A ×d (B ×d C) ⟩
+PairAssocLR = record {
+  f = λ { ((a , b) , c) → a , (b , c) } ;
+  isMon = λ { {(a1 , b1) , c1} {(a2 , b2) , c2} ((a1≤a2 , b1≤b2) , c1≤c2) →
+    a1≤a2 , (b1≤b2 , c1≤c2)} }
+
+PairAssocRL : {A B C : Predomain} ->
+ ⟨ A ×d (B ×d C) ==> A ×d B ×d C ⟩
+PairAssocRL = record {
+  f =  λ { (a , (b , c)) -> (a , b) , c } ;
+  isMon = λ { {a1 , (b1 , c1)} {a2 , (b2 , c2)} (a1≤a2 , (b1≤b2 , c1≤c2)) →
+    (a1≤a2 , b1≤b2) , c1≤c2} }
+
+PairCong : {Γ A A' : Predomain} ->
+  ⟨ A ==> A' ⟩ -> ⟨ (Γ ×d A) ==> (Γ ×d A') ⟩
+PairCong f = record {
+  f = λ { (γ , a) → γ , (f $ a)} ;
+  isMon = λ { {γ1 , a1} {γ2 , a2} (γ1≤γ2 , a1≤a2) → γ1≤γ2 , isMon f a1≤a2 }}
+
+{-
+PairCong : {Γ A A' : Predomain} ->
+  ⟨ A ==> A' ⟩ -> ⟨ (Γ ×d A) ==> (Γ ×d A') ⟩
+PairCong f = Uncurry (mCompU {!!} {!!})
+-- Goal: 
+-- Γ ==> (A ==> Γ ×d A')
+-- Write it as : Γ ==> (A ==> (A' ==> Γ ×d A'))
+-- i.e. Γ ==> A' ==> Γ ×d A'
+-- Pair : ⟨ A ==> B ==> A ×d B ⟩
+-}
+
+TransformDomain : {Γ A A' B : Predomain} ->
+    ⟨ Γ ×d A ==> B ⟩ ->
+    ⟨ ( A ==> B ) ==> ( A' ==> B ) ⟩ ->
+    ⟨ Γ ×d A' ==> B ⟩
+TransformDomain fΓ×A->B f = Uncurry (IntroArg' (Curry fΓ×A->B) f)
+
+
+
+  -- Convenience versions of comp, ext, and ret using combinators
+
+mComp' : (Γ : Predomain) -> {A B C : Predomain} ->
+    ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+mComp' Γ {A} {B} {C} f g = S {!!} (mCompU f aux) g
+    where
+      aux : ⟨ Γ ×d A ×d B ==> Γ ×d B ⟩
+      aux = mCompU π1 (mCompU (mCompU PairAssocRL (PairCong SwapPair)) PairAssocLR)
+
+      aux2 : ⟨ Γ ×d B ==> C ⟩ -> ⟨ Γ ×d A ×d B ==> C ⟩
+      aux2 h = mCompU f aux
+
+
+_∘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_
+
+
+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 = {!!}
+
+Map : {Γ A B : Predomain} ->
+    ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ==> 𝕃 A) ⟩ -> ⟨ (Γ ==> 𝕃 B) ⟩
+Map {Γ} f la = S Γ (mMap' f) la -- Γ ! mMap' f <*> la
+
+
+  {-
+  -- Montone function between function spaces
+  mFun : {A A' B B' : Predomain} ->
+    MonFun A' A ->
+    MonFun B B' ->
+    MonFun (arr' A B) (arr' A' B')
+  mFun fA'A fBB' = record {
+    f = λ fAB → {!!} ; --  mComp (mComp fBB' fAB) fA'A ;
+    isMon = λ {fAB-1} {fAB-2} fAB-1≤fAB-2 →
+      λ a'1 a'2 a'1≤a'2 ->
+        MonFun.isMon fBB'
+          (fAB-1≤fAB-2
+            (MonFun.f fA'A a'1)
+            (MonFun.f fA'A a'2)
+            (MonFun.isMon fA'A a'1≤a'2))}
+
+  -- NTS :
+  -- In the space of monotone functions from A' to B', we have
+  -- mComp (mComp fBB' f1) fA'A) ≤ (mComp (mComp fBB' f2) fA'A)
+  -- That is, given a'1 and a'2 of type ⟨ A' ⟩ with a'1 ≤ a'2 we
+  -- need to show that
+  -- (fBB' ∘ fAB-1 ∘ fA'A)(a'1) ≤ (fBB' ∘ fAB-2 ∘ fA'A)(a'2)
+  -- By monotonicity of fBB', STS that
+  -- (fAB-1 ∘ fA'A)(a'1) ≤  (fAB-2 ∘ fA'A)(a'2)
+  -- which follows by assumption that fAB-1 ≤ fAB-2 and monotonicity of fA'A
+  -}
+
+  -- Embedding of function spaces is monotone
+mFunEmb : (A A' B B' : Predomain) ->
+    ⟨ A' ==> 𝕃 A ⟩ ->
+    ⟨ B ==> B' ⟩ ->
+    ⟨ (A ==> 𝕃 B) ==> (A' ==> 𝕃 B') ⟩
+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) ->
+   ⟨ A ==> A' ⟩ ->
+   ⟨ B' ==> 𝕃 B ⟩ ->
+   ⟨ (A' ==> 𝕃 B') ==> 𝕃 (A ==> 𝕃 B) ⟩
+mFunProj A A' B B' fAA' fB'LB = {!!}
+  -- mRet' (mExt' (K fB'LB) ∘m Id ∘m (K fAA'))
+
+  -- 
+
+  {-
+  record {
+    f = λ f -> {!!} ; -- mComp (mExt (mComp (mMap fBB') f)) fA'LA ;
+    isMon = λ {f1} {f2} f1≤f2 ->
+      λ a'1 a'2 a'1≤a'2 ->
+        ext-monotone
+          (mapL (MonFun.f fBB') ∘ MonFun.f f1)
+          (mapL (MonFun.f fBB') ∘ MonFun.f f2)
+          ({!!})
+          (MonFun.isMon fA'LA a'1≤a'2) }
+  -}
+
+  -- 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/Semantics/Predomains.agda b/formalizations/guarded-cubical/Semantics/Predomains.agda
new file mode 100644
index 0000000000000000000000000000000000000000..316544eeb62dd8035d6b5118c82889fd5966f3a1
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Predomains.agda
@@ -0,0 +1,84 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module Semantics.Predomains where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Binary.Poset
+
+open import Common.Later
+
+-- Define predomains as posets
+Predomain : Set₁
+Predomain = Poset â„“-zero â„“-zero
+
+
+-- The relation associated to a predomain d
+rel : (d : Predomain) -> (⟨ d ⟩ -> ⟨ d ⟩ -> Type)
+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
+
+
+
+-- Theta for predomains
+
+module _ (k : Clock) where
+
+  private
+    variable
+      l : Level
+    
+    ▹_ : Set l → Set l
+    â–¹_ A = â–¹_,_ k A
+
+
+  
+  isSet-poset : {ℓ ℓ' : Level} -> (P : Poset ℓ ℓ') -> isSet ⟨ P ⟩
+  isSet-poset P = IsPoset.is-set (PosetStr.isPoset (str P))
+
+
+  ▸' : ▹ Predomain → Predomain
+  ▸' X = (▸ (λ t → ⟨ X t ⟩)) ,
+         posetstr ord
+                  (isposet isset-later {!!} ord-refl ord-trans ord-antisym)
+     where
+
+       ord : ▸ (λ t → ⟨ X t ⟩) → ▸ (λ t → ⟨ X t ⟩) → Type ℓ-zero
+       -- ord x1~ x2~ =  ▸ (λ t → (str (X t) PosetStr.≤ (x1~ t)) (x2~ t))
+       ord x1~ x2~ =  ▸ (λ t → (PosetStr._≤_ (str (X t)) (x1~ t)) (x2~ t))
+     
+
+       isset-later : isSet (▸ (λ t → ⟨ X t ⟩))
+       isset-later = λ x y p1 p2 i j t →
+         isSet-poset (X t) (x t) (y t) (λ i' → p1 i' t) (λ i' → p2 i' t) i j
+
+       ord-refl : (a : ▸ (λ t → ⟨ X t ⟩)) -> ord a a
+       ord-refl a = λ t ->
+         IsPoset.is-refl (PosetStr.isPoset (str (X t))) (a t)
+
+       ord-trans : BinaryRelation.isTrans ord
+       ord-trans = λ a b c ord-ab ord-bc t →
+         IsPoset.is-trans
+           (PosetStr.isPoset (str (X t))) (a t) (b t) (c t) (ord-ab t) (ord-bc t)
+
+       ord-antisym : BinaryRelation.isAntisym ord
+       ord-antisym = λ a b ord-ab ord-ba i t ->
+         IsPoset.is-antisym
+           (PosetStr.isPoset (str (X t))) (a t) (b t) (ord-ab t) (ord-ba t) i
+
+
+  -- Delay for predomains
+  ▸''_ : Predomain → Predomain
+  â–¸'' X = â–¸' (next X)
+
diff --git a/formalizations/guarded-cubical/Semantics/Semantics.agda b/formalizations/guarded-cubical/Semantics/Semantics.agda
index f8b1242c005438640639a19b9b72f9886a9fed11..ec86c7c87ea66a063e010144dc3c299c65e3cfbc 100644
--- a/formalizations/guarded-cubical/Semantics/Semantics.agda
+++ b/formalizations/guarded-cubical/Semantics/Semantics.agda
@@ -28,11 +28,16 @@ open import Cubical.Foundations.Function
 
 open import Common.Common
 
+open import Semantics.Predomains
+open import Semantics.Lift k
 open import Semantics.StrongBisimulation k
 open import Syntax.GradualSTLC
 -- open import SyntacticTermPrecision k
-open import Common.Lemmas k
-open import Common.MonFuns k
+
+open import Semantics.Monotone.Base
+open import Semantics.Monotone.Lemmas k
+open import Semantics.Monotone.MonFunCombinators k
+
 
 private
   variable
diff --git a/formalizations/guarded-cubical/Semantics/StrongBisimulation.agda b/formalizations/guarded-cubical/Semantics/StrongBisimulation.agda
index 0e4b10b004a8c884374b373bbc4b6def7dd2e392..66ce8736779cc7669b15c74f299c307228063172 100644
--- a/formalizations/guarded-cubical/Semantics/StrongBisimulation.agda
+++ b/formalizations/guarded-cubical/Semantics/StrongBisimulation.agda
@@ -4,6 +4,7 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 
 open import Common.Later
+open import Semantics.Monotone.Base
 
 module Semantics.StrongBisimulation(k : Clock) where
 
@@ -31,6 +32,9 @@ open import Cubical.Data.Unit.Properties
 open import Agda.Primitive
 
 open import Common.Common
+open import Semantics.Predomains
+open import Semantics.Lift k
+open import Semantics.ErrorDomains
 
 private
   variable
@@ -44,397 +48,6 @@ private
 
 
 
-Predomain' : {â„“ â„“' : Level} -> Type (â„“-max (â„“-suc â„“) (â„“-suc â„“'))
-Predomain' {â„“} {â„“'} = Poset â„“ â„“'
-
--- The relation associated to a predomain d
-rel' : (d : Predomain') -> (⟨ d ⟩ -> ⟨ d ⟩ -> Type)
-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 
-
-test : Predomain' -> Predomain' -> Predomain'
-test A B =
-  (Path Predomain' A B) ,
-  posetstr (λ p1 p2 → rel' A {!p1 i0!} {!!} × {!!})
-    (isposet {!!} {!!} (λ a → {!!}) {!!} {!!}) 
-
-
-
-
-
-
-
-
-
--- Define predomains as posets
-
-
-Predomain : Set₁
-Predomain = Poset â„“-zero â„“-zero
-
-
--- The relation associated to a predomain d
-rel : (d : Predomain) -> (⟨ d ⟩ -> ⟨ d ⟩ -> Type)
-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
-
-record MonFun (X Y : Predomain) : Set where
-  module X = PosetStr (X .snd)
-  module Y = PosetStr (Y .snd)
-  _≤X_ = X._≤_
-  _≤Y_ = Y._≤_
-  field
-    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' }
-
-
-compRel : {X Y Z : Type} ->
-  (R1 : Y -> Z -> Type â„“) ->
-  (R2 : X -> Y -> Type â„“) ->
-  (X -> Z -> Type â„“)
-compRel {ℓ} {X} {Y} {Z} R1 R2 x z = Σ[ y ∈ Y ] R2 x y × R1 y z
-
-CompMonRel : {X Y Z : Predomain} ->
-  MonRel {â„“} Y Z ->
-  MonRel {â„“} X Y ->
-  MonRel {â„“} X Z
-CompMonRel {â„“} {X} {Y} {Z} R1 R2 = record {
-  R = compRel (MonRel.R R1) (MonRel.R R2) ;
-  isAntitone = antitone ;
-  isMonotone = {!!} }
-    where
-      antitone : {x x' : ⟨ X ⟩} {z : ⟨ Z ⟩} ->
-        compRel (MonRel.R R1) (MonRel.R R2) x z ->
-        rel X x' x ->
-        compRel (MonRel.R R1) (MonRel.R R2) x' z 
-      antitone (y , xR2y , yR1z) x'≤x = y , (MonRel.isAntitone R2 xR2y x'≤x) , yR1z
-
-      monotone : {x : ⟨ X ⟩} {z z' : ⟨ Z ⟩} ->
-        compRel (MonRel.R R1) (MonRel.R R2) x z ->
-        rel Z z z' ->
-        compRel (MonRel.R R1) (MonRel.R R2) x z'
-      monotone (y , xR2y , yR1z) z≤z' = y , xR2y , (MonRel.isMonotone R1 yR1z z≤z')
-
-
-{-
-record IsMonFun {X Y : Predomain} (f : ⟨ X ⟩ → ⟨ Y ⟩) : Type (ℓ-max ℓ ℓ') where
-  no-eta-equality
-  constructor ismonfun
-
-  module X = PosetStr (X .snd)
-  module Y = PosetStr (Y .snd)
-  _≤X_ = X._≤_
-  _≤Y_ = Y._≤_
-
-  field
-    isMon : ∀ {x y} → x ≤X y → f x ≤Y f y
-
-record MonFunStr (â„“' : Level) (X Y : Predomain) : Type (â„“-max â„“ (â„“-suc â„“')) where
-
-  constructor monfunstr
-
-  field
-    f : ⟨ X ⟩ -> ⟨ Y ⟩
-    isMonFun : IsMonFun {â„“'} f
-
-  open IsMonFun isMonFun public
-
-MonF : ∀ ℓ ℓ' -> Predomain -> Predomain -> Type (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ'))
-MonF â„“ â„“' X Y = TypeWithStr â„“ {!!}
--}
-
-{-
-lem-later : {X~ : â–¹ Type} ->
-  (x~ y~ : ▸ X~) -> (x~ ≡ y~) ≡ ( ▸ λ t -> ( x~ t ≡ y~ t ))
-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
-                (isposet isset-later {!!} ord-refl ord-trans ord-antisym)
-   where
-
-     ord : ▸ (λ t → ⟨ X t ⟩) → ▸ (λ t → ⟨ X t ⟩) → Type ℓ-zero
-     -- ord x1~ x2~ =  ▸ (λ t → (str (X t) PosetStr.≤ (x1~ t)) (x2~ t))
-     ord x1~ x2~ =  ▸ (λ t → (PosetStr._≤_ (str (X t)) (x1~ t)) (x2~ t))
-     
-
-     isset-later : isSet (▸ (λ t → ⟨ X t ⟩))
-     isset-later = λ x y p1 p2 i j t →
-       isSet-poset (X t) (x t) (y t) (λ i' → p1 i' t) (λ i' → p2 i' t) i j
-
-     ord-refl : (a : ▸ (λ t → ⟨ X t ⟩)) -> ord a a
-     ord-refl a = λ t ->
-       IsPoset.is-refl (PosetStr.isPoset (str (X t))) (a t)
-
-     ord-trans : BinaryRelation.isTrans ord
-     ord-trans = λ a b c ord-ab ord-bc t →
-       IsPoset.is-trans
-         (PosetStr.isPoset (str (X t))) (a t) (b t) (c t) (ord-ab t) (ord-bc t)
-
-     ord-antisym : BinaryRelation.isAntisym ord
-     ord-antisym = λ a b ord-ab ord-ba i t ->
-       IsPoset.is-antisym
-         (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
-  module X = PosetStr (X .snd)
-  _≤_ = X._≤_
-  field
-    ℧ : X .fst
-    ℧⊥ : ∀ x → ℧ ≤ x
-    θ : MonFun (▸'' X) X
-
-
--- Lift monad
-
-data L℧ (X : Set) : Set where
-  η : X → L℧ X
-  ℧ : 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 = η
-
-{-
-bind' : ∀ {A B} -> (A -> L℧ B) -> ▹ (L℧ A -> L℧ B) -> L℧ A -> L℧ B
-bind' f bind_rec (η x) = f x
-bind' f bind_rec ℧ = ℧
-bind' f bind_rec (θ l_la) = θ (bind_rec ⊛ l_la)
-
--- fix : ∀ {l} {A : Set l} → (f : ▹ k , A → A) → A
-bind : L℧ A -> (A -> L℧ B) -> L℧ B
-bind {A} {B} la f = (fix (bind' f)) la
-
-ext : (A -> L℧ B) -> L℧ A -> L℧ B
-ext f la = bind la f
--}
-
-ext' : (A -> L℧ B) -> ▹ (L℧ A -> L℧ B) -> L℧ A -> L℧ B
-ext' f rec (η x) = f x
-ext' f rec ℧ = ℧
-ext' f rec (θ l-la) = θ (rec ⊛ l-la)
-
-ext : (A -> L℧ B) -> L℧ A -> L℧ B
-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)
-
-
-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
-
-  module X = PosetStr (p .snd)
-  open X using (_≤_)
-  -- _≤_ = X._≤_
-
-  module Inductive (rec : ▹ (L℧ (U p) -> L℧ (U p) -> Type)) where
-
-    _≾'_ : L℧ (U p) -> L℧ (U p) -> Type
-    ℧ ≾' _ = Unit
-    η x ≾' η y = x ≤ y
-    θ lx ≾' θ ly = ▸ (λ t -> rec t (lx t) (ly t))
-    η _ ≾' _ = ⊥
-    θ _ ≾' _ = ⊥
-
-  open Inductive
-  _≾_ : L℧ (U p) -> L℧ (U p) -> Type
-  _≾_ = fix _≾'_
-
-  ≾-refl : BinaryRelation.isRefl _≾_
-
-  ≾-refl' : ▹ (BinaryRelation.isRefl _≾_) ->
-            BinaryRelation.isRefl _≾_
-  ≾-refl' IH (η x) =
-    transport (sym (λ i -> fix-eq _≾'_ i (η x) (η x)))
-              (IsPoset.is-refl (X.isPoset) x)
-  ≾-refl' IH ℧ =
-    transport (sym (λ i -> fix-eq _≾'_ i ℧ ℧))
-              tt
-  ≾-refl' IH (θ lx~) =
-    transport (sym (λ i -> fix-eq _≾'_ i (θ lx~) (θ lx~)))
-              λ t → IH t (lx~ t)
-
-  ≾-refl = fix ≾-refl'
-
-  
-  ℧-bot : (l : L℧ (U p)) -> ℧ ≾ l
-  ℧-bot l = transport (sym λ i → fix-eq _≾'_ i ℧ l) tt
-
-
-
--- Predomain to lift predomain
-
-𝕃℧' : Predomain -> Predomain
-𝕃℧' X = L℧ (X .fst) ,
-      posetstr (LiftOrder._≾_ X)
-        (isposet {!!} {!!} ≾-refl {!!} {!!})
-  where open LiftOrder X
-
-
--- Predomain to lift Error Domain
-
-𝕃℧ : Predomain → ErrorDomain
-𝕃℧ X = record {
-  X = 𝕃℧' X ; ℧ = ℧ ; ℧⊥ = ℧-bot ;
-  θ = record { f = θ ; isMon = λ t -> {!!} } }
-  where
-    -- module X = PosetStr (X .snd)
-    -- open Relation X
-    open LiftOrder X
-
-𝕌 : ErrorDomain -> Predomain
-𝕌 d = ErrorDomain.X d
--}
-
 
 -- Flat predomain from a set
 
@@ -455,17 +68,9 @@ UnitP : Predomain
 UnitP = flat (Unit , isSetUnit)
 
 
--- Underlying predomain of an error domain
-
-𝕌 : ErrorDomain -> Predomain
-𝕌 d = ErrorDomain.X d
-
-
 
 -- Predomains from arrows (need to ensure monotonicity)
 
-
-
 -- Ordering on functions between predomains. This does not require that the
 -- functions are monotone.
 fun-order-het : (P1 P1' P2 P2' : Predomain) ->
@@ -478,8 +83,6 @@ 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-het
 fun-order : (P1 P2 : Predomain) -> (⟨ P1 ⟩ -> ⟨ P2 ⟩) -> (⟨ P1 ⟩ -> ⟨ P2 ⟩) -> Type ℓ-zero
 fun-order P1 P2 f1 f2 =
@@ -497,6 +100,7 @@ mon-fun-order-refl : {P1 P2 : Predomain} ->
   fun-order P1 P2 f f
 mon-fun-order-refl {P1} {P2} f f-mon = λ x y x≤y → f-mon x≤y
 -}
+  
 
 fun-order-trans : {P1 P2 : Predomain} ->
   (f g h : ⟨ P1 ⟩ -> ⟨ P2 ⟩) ->
@@ -534,8 +138,8 @@ mon-fun-order-trans : {P1 P2 : Predomain} ->
   mon-fun-order P1 P2 f g ->
   mon-fun-order P1 P2 g h ->
   mon-fun-order P1 P2 f h
-mon-fun-order-trans f g h f≤g g≤h =
-  fun-order-trans (MonFun.f f) (MonFun.f g) (MonFun.f h) f≤g g≤h
+mon-fun-order-trans {P1} {P2} f g h f≤g g≤h =
+  fun-order-trans {P1} {P2} (MonFun.f f) (MonFun.f g) (MonFun.f h) f≤g g≤h
 
 
 -- Predomain of monotone functions between two predomains
@@ -556,13 +160,9 @@ arr' P1 P2 =
          (Hf2-f3 x y H≤xy))
       {!!}))
   where
-    -- Two functions from P1 to P2 are related if, when given inputs
-    -- that are related (in P1), the outputs are related (in P2)
     open MonFun
     module P1 = PosetStr (P1 .snd)
     module P2 = PosetStr (P2 .snd)
-    _≤P1_ = P1._≤_
-    _≤P2_ = P2._≤_
 
 
 _==>_ : Predomain -> Predomain -> Predomain
@@ -591,32 +191,8 @@ FunRel {A} {A'} {B} {B'} RAA' RBB' =
       MonRel.isMonotone RBB' (f≤f' a a' a≤a') {!!} } -- (f'≤g' a' a' (reflexive A' a')) }
 
 
-arr : Predomain -> ErrorDomain -> ErrorDomain
-arr dom cod =
-  record {
-    X = arr' dom (𝕌 cod) ;
-    ℧ = const-err ;
-    ℧⊥ = const-err-bot ;
-    θ = {!!} }
-    where
-       -- open LiftOrder
-       const-err : ⟨ arr' dom (𝕌 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)
- 
-
-
--- Delay function
-δ : {X : Type} -> L℧ X -> L℧ X
-δ = θ ∘ next
-  where open L℧
-
-
 
+ 
 -- Lifting a heterogeneous relation between A and B to a
 -- relation between L A and L B
 -- (We may be able to reuse this logic to define the homogeneous ordering on 𝕃 below)
@@ -671,37 +247,6 @@ module LiftPredomain (p : Predomain) where
 
   module X = PosetStr (p .snd)
   open X using (_≤_)
-      -- _≤_ = X._≤_
-
-  {-
-  ord' : ▹ ( L℧ ⟨ p ⟩ → L℧ ⟨ p ⟩ → Type) ->
-                 L℧ ⟨ p ⟩ → L℧ ⟨ p ⟩ → Type
-  ord' _ ℧ _ = Unit
-  ord' _ (η x) (η y) = x ≤ y
-  ord' _ (η _) _ = ⊥
-  ord' rec (θ lx~) (θ ly~) = ▸ (λ t -> (rec t) (lx~ t) (ly~ t))
-        -- or: ▸ ((rec ⊛ lx~) ⊛ ly~)
-  ord' _ (θ _) _ = ⊥
-
-  ord :  L℧ ⟨ p ⟩ → L℧ ⟨ p ⟩ → Type
-  ord = fix ord'
-  -}
-
-  -- _≾_ : L℧ ⟨ p ⟩ -> L℧ ⟨ p ⟩ -> Type
-  -- _≾_ = LiftRelation._≾_ p p (_≤_)
-
-  -- unfold-ord : ord ≡ ord' (next ord)
-  -- unfold-ord = fix-eq ord'
-
-   {-
-   ≈->≈' : {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
-   -}
 
 
   -- Open the more general definitions from the heterogeneous
@@ -714,10 +259,6 @@ module LiftPredomain (p : Predomain) where
   open Inductive (next _≾_) public
   open Properties public
 
-  {-
-  ord-η-monotone : {x y : ⟨ p ⟩} -> x ≤ y -> (η x) ≾ (η y)
-  ord-η-monotone {x} {y} x≤y = transport (sym λ i → unfold-≾ i (η x) (η y)) x≤y
-  -}
 
   -- TODO move to heterogeneous lifting module
   ord-δ-monotone : {lx ly : L℧ ⟨ p ⟩} -> lx ≾ ly -> (δ lx) ≾ (δ ly)
@@ -729,12 +270,6 @@ module LiftPredomain (p : Predomain) where
         Inductive._≾'_ (next _≾_) (δ lx) (δ ly)
       ord-δ-monotone' {lx} {ly} lx≤ly = λ t → lx≤ly
 
-  {-
-  ord-bot : (lx : L℧ ⟨ p ⟩) -> ℧ ≾ lx
-  ord-bot lx = transport (sym λ i → unfold-≾ i ℧ lx) tt
-  -}
-
-  -- lift-ord : (A -> A -> Type) -> (L℧ A -> L℧ A -> Type)
 
   ord-refl-ind : ▹ ((a : L℧ ⟨ p ⟩) -> a ≾ a) ->
                     (a : L℧ ⟨ p ⟩) -> a ≾ a
@@ -797,7 +332,7 @@ module LiftRelMon
   -- Bring the heterogeneous relation between 𝕃 A and 𝕃 B into scope
   open LiftRelation A B (MonRel.R RAB)
     using (_≾_ ; module Inductive ; module Properties) -- brings _≾_ into scope
-  open Inductive (next _≾_)            -- brings _≾'_ into scope
+  open Inductive (next _≾_)  -- brings _≾'_ into scope
   open Properties -- brings conversion between _≾_ and _≾'_ into scope
 
   -- Bring the homogeneous lifted relations on A and B into scope 
@@ -812,47 +347,31 @@ module LiftRelMon
   _≾'LA_ = LiftPredomain._≾'_ A
   _≾'LB_ = LiftPredomain._≾'_ B
 
-
   R : MonRel (𝕃 A) (𝕃 B)
   R = record {
     R = _≾_ ;
-    isAntitone = {!!} ;
+    isAntitone = λ {la} {la'} {lb} la≤lb la'≤la -> {!!} ;
     isMonotone = {!!} }
-
-  antitone' :
-    ▹ ({la la' : L℧ ⟨ A ⟩} -> {lb : L℧ ⟨ B ⟩} ->
-        la ≾' lb -> la' ≾'LA la -> la' ≾' lb) ->
-       {la la' : L℧ ⟨ A ⟩} -> {lb : L℧ ⟨ B ⟩} ->
-        la ≾' lb -> la' ≾'LA la -> la' ≾' lb
-  antitone' IH {η a2} {η a1} {η a3} la≤lb la'≤la =
-    MonRel.isAntitone RAB la≤lb la'≤la
-  antitone' IH {la} {℧} {lb} la≤lb la'≤la = tt
-  antitone' IH {θ la2~} {θ la1~} {θ lb~} la≤lb la'≤la =
-    λ t → ≾'->≾ (IH t (≾->≾' (la≤lb t)) ({!!} ))
-
-  monotone : {!!}
-  monotone = {!!}
+    where
+      antitone' :
+        ▹ ({la la' : L℧ ⟨ A ⟩} -> {lb : L℧ ⟨ B ⟩} ->
+            la ≾' lb -> la' ≾'LA la -> la' ≾' lb) ->
+           {la la' : L℧ ⟨ A ⟩} -> {lb : L℧ ⟨ B ⟩} ->
+            la ≾' lb -> la' ≾'LA la -> la' ≾' lb
+      antitone' IH {η a2} {η a1} {η a3} la≤lb la'≤la =
+        MonRel.isAntitone RAB la≤lb la'≤la
+      antitone' IH {la} {℧} {lb} la≤lb la'≤la = tt
+      antitone' IH {θ la2~} {θ la1~} {θ lb~} la≤lb la'≤la =
+        λ t → ≾'->≾ (IH t {!!} {!!})
+
+      monotone : {!!}
+      monotone = {!!}
 
  -- 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 to lift Error Domain
-
-𝕃℧ : Predomain → ErrorDomain
-𝕃℧ X = record {
-  X = 𝕃 X ; ℧ = ℧ ; ℧⊥ = ord-bot X ;
-  θ = record { f = θ ; isMon = λ t -> {!!} } }
-  where
-    -- module X = PosetStr (X .snd)
-    -- open Relation X
-    open LiftPredomain
-
-
-
-
-
 
 -- Product of predomains
 
@@ -903,23 +422,6 @@ A ×d B =
        IsPoset.is-trans B.isPoset b1 b2 b3 b1≤b2 b2≤b3
     
 
-    {-
-    order : ⟨ A ⟩ × ⟨ B ⟩ → ⟨ A ⟩ × ⟨ B ⟩ → Type ℓ-zero
-    order (a1 , b1) (a2 , b2) = (a1 A.≤ a2) ⊎ ((a1 ≡ a2) × b1 B.≤ b2)
-
-    order-trans : BinaryRelation.isTrans order
-    order-trans (a1 , b1) (a2 , b2) (a3 , b3) (inl a1≤a2) (inl a2≤a3) =
-      inl (IsPoset.is-trans A.isPoset a1 a2 a3 a1≤a2 a2≤a3)
-    order-trans (a1 , b1) (a2 , b2) (a3 , b3) (inl a1≤a2) (inr (a2≡a3 , b2≤b3)) =
-      inl (transport (λ i → a1 A.≤ a2≡a3 i) a1≤a2)
-    order-trans (a1 , b1) (a2 , b2) (a3 , b3) (inr (a1≡a2 , b1≤b2)) (inl a2≤a3) =
-      inl (transport (sym (λ i → a1≡a2 i A.≤ a3)) a2≤a3)
-    order-trans (a1 , b1) (a2 , b2) (a3 , b3) (inr (a1≡a2 , b1≤b2)) (inr (a2≡a3 , b2≤b3)) =
-      inr (
-        (a1 ≡⟨ a1≡a2 ⟩ a2 ≡⟨ a2≡a3 ⟩ a3 ∎) ,
-        IsPoset.is-trans B.isPoset b1 b2 b3 b1≤b2 b2≤b3)
-    -}
-
     is-poset : IsPoset order
     is-poset = isposet
       isSet-prod
@@ -1060,25 +562,12 @@ module Bisimilarity (d : Predomain) where
     ≈'->≈ : {lx ly : L℧ ⟨ d ⟩} ->
      lx ≈' ly -> lx ≈ ly
     ≈'->≈ {lx} {ly} lx≈'ly = transport (sym (λ i → unfold-≈ i lx ly)) lx≈'ly
-
-    {-
-    ≈-℧ : (lx : L℧ ⟨ d ⟩) ->
-     lx ≈' ℧ -> (lx ≡ ℧) ⊎ (Σ Nat λ n -> lx ≡ (δ ^ n) ℧)
-    ≈-℧ ℧ H = inl refl
-    ≈-℧ (θ x) H = inr H
-    -}
     
-    -- Simpler version of the above:
     ≈-℧ : (lx : L℧ ⟨ d ⟩) ->
      lx ≈' ℧ -> (Σ Nat λ n -> lx ≡ (δ ^ n) ℧)
     ≈-℧ ℧ H = zero , refl
     ≈-℧ (θ x) H = H
 
-{-
-    bisim-θ : (lx~ ly~ : L℧ ⟨ d ⟩) ->
-       ▸ (λ t → lx~ t ≈ ly~ t) ->
-       θ lx~ ≈ θ ly~
--} 
 
     symmetric' :
       ▹ ((lx ly : L℧ ⟨ d ⟩) -> lx ≈' ly -> ly ≈' lx) ->
@@ -1095,12 +584,9 @@ module Bisimilarity (d : Predomain) where
       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')
+    symmetric = {!!} -- fix {k} (subst {!!} {!!}) 
 
    {-
-
         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) →
@@ -1160,9 +646,6 @@ module Bisimilarity (d : Predomain) where
       (fix x≈'δx)
 
 
-    -- ¬_ : Set → Set
-    -- ¬ A = A → ⊥
-
     contradiction : {A : Type} -> A -> ¬ A -> ⊥
     contradiction HA ¬A = ¬A HA
 
@@ -1187,8 +670,8 @@ module Bisimilarity (d : Predomain) where
 
 
     fixθ-lem1 : (n : Nat) ->
-      (▹ (¬ (θ (next (fix θ)) ≡ (δ ^ n) ℧))) ->
-          ¬ (θ (next (fix θ)) ≡ (δ ^ n) ℧)
+      (▹ (¬ (θ {Nat} (next (fix θ)) ≡ (δ ^ n) ℧))) ->
+          ¬ (θ {Nat} (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 {!!}
@@ -1196,254 +679,4 @@ module Bisimilarity (d : Predomain) where
 
     ℧-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)
-
--}
-
-
-
-
-{-
--- Weak bisimulation relaion
--- Define compositionally
-
-module WeakRel (d : ErrorDomain) where
-
-  -- make this a module so we can avoid having to make the IH
-  -- a parameter of the comparison function
-  module Inductive (IH : ▹ (L℧ (U d) -> L℧ (U d) -> Type)) where
-
-    open ErrorDomain d renaming (θ to θ')
-
-    _≾'_ : L℧ (U d) -> L℧ (U d) -> Type
-    ℧ ≾' _ = Unit
-      
-    η x ≾' η y = x ≤ y
-    
-    θ lx ≾' θ ly = ▸ (λ t -> IH t (lx t) (ly t))
-    -- or equivalently: θ lx ≾' θ ly = ▸ ((IH ⊛ lx) ⊛ ly)
-      
-    η x ≾' θ t = Σ ℕ λ 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 = Σ ℕ λ n ->
-       (θ s ≡ (δ ^ n) L℧.℧) ⊎
-       (Σ (U d) (λ x -> (θ s ≡ (δ ^ n) (η x)) × (x ≤ y)))
-      
-    _ ≾' ℧ = ⊥
-   
-  _≾_ : L℧ (U d) -> L℧ (U d) -> Type
-  _≾_ = 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.
-
-
-
-
--}