More code refactoring/cleanup

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
   _ ≋'' _ = ⊥

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)

formalizations/guarded-cubical/Semantics/ErrorDomains.agda

+
+{-# 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
+-}

formalizations/guarded-cubical/Semantics/Lift.agda

+{-# 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~
+

formalizations/guarded-cubical/Semantics/Monotone/Base.agda

+{-# 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')

formalizations/guarded-cubical/Semantics/Monotone/Lemmas.agda

+{-# 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₁)
+
+

formalizations/guarded-cubical/Semantics/Monotone/MonFunCombinators.agda

+{-# 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))
+ -}
+
+-}

formalizations/guarded-cubical/Semantics/Predomains.agda

+{-# 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)
+

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