Refactoring

formalizations/guarded-cubical/Semantics/ErrorDomains.agda

@@ -5,21 +5,36 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 
 open import Common.Later
+open import Common.Common
 
-module Semantics.ErrorDomains (k : Clock) where
+module Semantics.ErrorDomains where -- (k : Clock) where
 
+open import Cubical.Foundations.Prelude
 open import Cubical.Relation.Binary.Poset
 open import Cubical.Foundations.Structure
-
-open import Semantics.Predomains
 open import Cubical.Data.Sigma
 
 
+open import Semantics.Predomains
+import Semantics.Lift as L℧
+import Semantics.Monotone.MonFunCombinators
+open import Semantics.StrongBisimulation
+open import Semantics.PredomainInternalHom
+
 open import Semantics.Monotone.Base
 
--- Error domains
 
-record ErrorDomain : Set₁ where
+
+private
+  variable
+    ℓ : Level
+
+
+_$_ : {A B : Predomain} -> ⟨ A ==> B ⟩ -> ⟨ A ⟩ -> ⟨ B ⟩
+_$_ f = MonFun.f f
+
+-- Error domains
+record ErrorDomain' {ℓ : Level} (k : Clock) : Type (ℓ-suc ℓ) where
   field
     X : Predomain
   module X = PosetStr (X .snd)
@@ -29,32 +44,241 @@ record ErrorDomain : Set₁ where
     ℧⊥ : ∀ x → ℧ ≤ x
     θ : MonFun (▸''_ k X) X
 
+ErrorDomain : {ℓ : Level} -> Type (ℓ-suc ℓ)
+ErrorDomain = Σ[ k ∈ Clock ] ErrorDomain' k
+
+
+-- Isomorphic error domains (with potentially different clocks) have
+-- * Isomorphic predomains
+-- * The same error element and proof that it's the bottom element
+-- * Potentially different θ functions (since they're indexed by potentially different clocks)
+
+-- A family of error domains indexed by a clock k is
+
+-- Morphism of error domains
+record ErrorDomainFun {k k' : Clock} (A : ErrorDomain' {ℓ} k) (B : ErrorDomain' {ℓ} k') : Type where
+  open ErrorDomain'
+  θA = A .θ
+  θB = B .θ
+  field
+    f :  MonFun (A .X) (B .X)
+    f℧ : MonFun.f f (A .℧) ≡ (B .℧)
+    fθ : (x~ : ▹ k , ⟨ A .X ⟩) -> (f $ (θA $ x~)) ≡ (θB $ λ t → f $ {!x~ t!})
+    
+
 
 -- Underlying predomain of an error domain
+𝕌 : {k : Clock} -> ErrorDomain' {ℓ} k -> Predomain
+𝕌 d = ErrorDomain'.X d
 
-𝕌 : ErrorDomain -> Predomain
-𝕌 d = ErrorDomain.X d
 
-{-
-arr : Predomain -> ErrorDomain -> ErrorDomain
-arr dom cod =
+-- Later structure on error domains
+module _ (k : Clock)  where
+  -- open import Semantics.ErrorDomains k
+  open ErrorDomain'
+  open import Semantics.Monotone.MonFunCombinators
+  Domain-▹ : ErrorDomain' {ℓ} k -> ErrorDomain' {ℓ} k
+  Domain-▹ A =
+    record {
+      X  = (▸'' k) (𝕌 A) ;
+      ℧ = λ t → ErrorDomain'.℧ A ;
+      ℧⊥ = λ x t → ℧⊥ A (x t) ;
+      θ = Map▹ k (ErrorDomain'.θ A) }
+
+
+
+-- View the lift of a predomain as an error domain (under the provided clock)
+𝕃℧ : Predomain → (k : Clock) -> ErrorDomain' {ℓ} k
+𝕃℧ A k' = record {
+  X = 𝕃 A ; ℧ = L℧.℧ ; ℧⊥ = ord-bot A ;
+  θ = record { f = L℧.θ ; isMon = ord-θ-monotone A } }
+  where
+    open LiftPredomain k'
+
+
+-- Error domain of monotone functions between a predomain A and an error domain B
+arr : (k : Clock) -> Predomain -> ErrorDomain' {ℓ} k -> ErrorDomain' {ℓ} k
+arr k A B =
   record {
-    X = arr' dom (𝕌 cod) ;
+    X = A ==> (𝕌 B) ;
     ℧ = const-err ;
     ℧⊥ = const-err-bot ;
-    θ = {!!} }
+    θ = θf }
     where
-       -- open LiftOrder
-       const-err : ⟨ arr' dom (𝕌 cod) ⟩
+       open ErrorDomain'
+       open import Semantics.Monotone.MonFunCombinators k
+       const-err : ⟨ A ==> (𝕌 B) ⟩
        const-err = record {
-         f = λ _ -> ErrorDomain.℧ cod ;
-         isMon = λ _ -> reflexive (𝕌 cod) (ErrorDomain.℧ cod) }
+         f = λ _ -> ErrorDomain'.℧ B ;
+         isMon = λ _ -> reflexive (𝕌 B) (ErrorDomain'.℧ B) }
+
+       const-err-bot : (f : ⟨ A ==> (𝕌 B) ⟩) -> rel (A ==> (𝕌 B)) const-err f
+       const-err-bot f = λ x y x≤y → ErrorDomain'.℧⊥ B (MonFun.f f y)
+
+       θf : MonFun ((▸'' k) (A ==> 𝕌 B)) (A ==> 𝕌 B)
+       θf = mCompU {!!} Ap▹
+
+       -- Goal: MonFun (▹ (A ==> 𝕌 B)) (A ==> 𝕌 B)
+       -- We will factor this as
+       --  (▹ (A ==> 𝕌 B))  ==>  (▹ A ==> ▹ (𝕌 B))  ==>  (A ==> 𝕌 B)
+       -- The first function is Ap▹
+       -- The second is θB ∘ App ∘ next
+
+
+module ClockInv
+  (A : (k : Clock) -> ErrorDomain' {ℓ} k) where
+
+  open ErrorDomain'
+
+  {-
+  to' : {k k' : Clock} ->
+    (▹ k' , ▹ k , (⟨ 𝕌 (A k) ⟩ -> ⟨ 𝕌 (A k') ⟩)) ->
+                  (⟨ 𝕌 (A k) ⟩ -> ⟨ 𝕌 (A k') ⟩)
+  to' {k} {k'} rec = fix (λ rec' x → A k' .θ $ λ t' → rec' t' x)
+  -}
+
+
+  to : {k k' : Clock} -> ⟨ 𝕌 (A k) ⟩ -> ⟨ 𝕌 (A k') ⟩
+  
+
+
+module ClockInvariant
+  (A : (k : Clock) -> ErrorDomain' {ℓ} k) where
+
+  open ErrorDomain'
+
+  open import Cubical.Data.Empty
+
+  absurd : {k : Clock} ->
+    (▹ k , (⊥ -> ⟨ 𝕌 (A k) ⟩)) -> (⊥ -> ⟨ 𝕌 (A k) ⟩)
+  absurd {k} IH fls = (A k .θ) $ λ t → IH t fls
+  
+  -- Given a family of ErrorDomains indexed by a clock, we can define a function
+  -- between the underlying sets of any two members of the family.
+  -- TODO this function doesn't do anything, it just keeps adding θ's
+  to' : {k k' : Clock} ->
+    (▹ k' , (⟨ 𝕌 (A k) ⟩ -> ⟨ 𝕌 (A k') ⟩)) ->
+             ⟨ 𝕌 (A k) ⟩ -> ⟨ 𝕌 (A k') ⟩
+  to' {k} {k'} rec x1 = (A k' .θ) $ λ t → rec t x1
+
+  to : {k k' : Clock} -> ⟨ 𝕌 (A k) ⟩ -> ⟨ 𝕌 (A k') ⟩
+  to = fix to'
+
+  unfold-to : {k k' : Clock} -> to {k} {k'} ≡ to' (next to)
+  unfold-to = fix-eq to'
+
+  to'-refl : {k : Clock} ->
+    (▹ k , (to' {k} {k} (next to) ≡ id)) ->
+            to' {k} {k} (next to) ≡ id
+  to'-refl IH = funExt (λ x → {!!})
+
+
+  to'-mon : {k k' : Clock} ->
+    ▹ k' , ({x y : ⟨ 𝕌 (A k) ⟩} -> (rel (𝕌 (A k)) x y) ->
+               (rel (𝕌 (A k')) (to' (next to) x) (to' (next to) y))) ->
+            {x y : ⟨ 𝕌 (A k) ⟩} -> (rel (𝕌 (A k)) x y) ->
+               (rel (𝕌 (A k')) (to' (next to) x) (to' (next to) y))
+  to'-mon {k} {k'} IH {x} {y} x≤y = MonFun.isMon (θ (A k')) λ t ->
+    transport (sym (λ i → rel (𝕌 (A k')) (unfold-to i x) (unfold-to i y))) (IH t x≤y)
 
-       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)
+  to'-mon' : {k k' : Clock} -> {x y : ⟨ 𝕌 (A k) ⟩} -> (rel (𝕌 (A k)) x y) ->
+    ▹ k' , (rel (𝕌 (A k')) (to' (next to) x) (to' (next to) y)) ->
+           (rel (𝕌 (A k')) (to' (next to) x) (to' (next to) y))
+  to'-mon' {k} {k'} {x} {y} x≤y IH = MonFun.isMon (θ (A k')) λ t ->
+    transport (sym (λ i → rel (𝕌 (A k')) (unfold-to i x) (unfold-to i y))) (IH t)
+
+{- NTS:
+ (rel (𝕌 (A k')) (to' (next to) x) (to' (next to) y) ≡
+ (rel (𝕌 (A k')) (to x)            (to y)
 -}
 
 
+  to-mon : {k k' : Clock} ->
+     {x y : ⟨ 𝕌 (A k) ⟩} -> (rel (𝕌 (A k)) x y) ->
+       (rel (𝕌 (A k')) (to x) (to y))
+  to-mon {k} {k'} {x} {y} x≤y = transport
+    (sym (λ i → rel (𝕌 (A k')) (unfold-to i x) (unfold-to i y)))
+    (fix (to'-mon' x≤y))
+
+
+  To : {k k' : Clock} -> ⟨ 𝕌 (A k) ==> 𝕌 (A k') ⟩
+  To {k} {k'} = record { f = to ; isMon = to-mon }
+
+{-
+  to' : ∀ k' -> (▹ k , (ErrorDomain' {ℓ} k -> ErrorDomain' {ℓ} k')) -> (ErrorDomain' k -> ErrorDomain' {ℓ} k')
+  to' k' rec A =
+    record {
+      X = A .X ;
+      ℧ = A .℧ ;
+      ℧⊥ = A .℧⊥ ;
+      θ = record {
+        f = λ a~ -> MonFun.f (A .θ) λ t -> let foo = rec t A in {!!} ;
+        isMon = {!!} } }
+-}
+
+
+{-
+bad : {k : Clock} -> {X : Type} ->  ▹ k , ▹ k , X -> ▹ k , X
+bad x = λ t → x t t
+-}
+
+module _ (k k' : Clock) {A : Type} where
+  -- open ErrorDomain
+  open import Cubical.Foundations.Isomorphism 
+  open import Semantics.Lift
+  
+  to' : (▹ k' , (L℧ k A -> L℧ k' A)) -> (L℧ k A -> L℧ k' A)
+  to' _ (η x) = η x
+  to' _ L℧.℧ = L℧.℧
+  to' rec (L℧.θ l~) = L℧.θ λ t → rec t (L℧.θ l~)
+
+  to : (L℧ k A -> L℧ k' A)
+  to = fix to'
+
+  inv' : (▹ k , (L℧ k' A -> L℧ k A)) -> (L℧ k' A -> L℧ k A)
+  inv' _ (η x) = η x
+  inv' _ L℧.℧ = L℧.℧
+  inv' rec (L℧.θ l~) = L℧.θ (λ t → rec t (L℧.θ l~))
+
+  inv : (L℧ k' A -> L℧ k A)
+  inv = fix inv'
+
+  unfold-to : fix (to') ≡ to' (next to)
+  unfold-to = fix-eq to'
+
+  unfold-inv : fix (inv') ≡ inv' (next inv)
+  unfold-inv = fix-eq inv'
+
+
+  L℧-Iso :  Iso (L℧ k A) (L℧ k' A)
+  L℧-Iso = iso to inv sec retr
+    where
+      sec' : ▹ k' , (section (to' (next to)) (inv' (next inv))) -> (section (to' (next to)) (inv' (next inv)))
+      sec' _ (η x) = refl
+      sec' _ L℧.℧ = refl
+      sec' IH (L℧.θ l~) = {!!}
+        -- cong L℧.θ (later-ext (λ t → let foo = IH t (L℧.θ l~) in let foo' = inj-θ k' _ _ foo in {!t!}))
+        -- λ i -> L℧.θ (λ t → IH t (L℧.θ l~) {!i!})
+--  L℧.θ (λ t → next to t (L℧.θ (λ t₁ → next inv t₁ (L℧.θ l~))))
+--      ≡ L℧.θ l~
+
+
+      -- cong L℧.θ (later-ext (λ t → let foo = IH t (L℧.θ l~) in {!!}))
+
+      sec : {!!}
+      sec = {!!}
+
+      retr' : retract to inv
+      retr' = {!!}
+
+      retr : {!!}
+      retr = {!!}
+
+
+
+
+
+
 {-
 -- Predomain to lift Error Domain
 
@@ -67,3 +291,45 @@ arr dom cod =
     -- open Relation X
     open LiftPredomain
 -}
+
+
+
+-- Experiment with composing relations on error domains
+{-
+
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Sigma
+open import Cubical.HITs.PropositionalTruncation
+
+record MyRel {ℓ} (B1 B2 : ErrorDomain) : Type (ℓ-suc ℓ) where
+  open ErrorDomain
+  open MonFun
+  private
+    UB1 = ⟨ 𝕌 B1 ⟩
+    UB2 = ⟨ 𝕌 B2 ⟩
+    ℧B1 = B1 .℧
+    θB1 = B1 .θ
+    θB2 = B2 .θ
+  field
+    Rel : UB1 -> UB2 -> hProp ℓ
+    Rel℧ : ∀ (b2 : UB2) -> ⟨ Rel ℧B1 b2 ⟩
+    RelΘ : ∀ (b1~ : ▹_,_ k UB1) -> (b2~ : ▹_,_ k UB2) ->
+      (▸ (λ t -> ⟨ Rel (b1~ t) (b2~ t) ⟩)) ->
+      ⟨ Rel (θB1 .f b1~) (θB2 .f b2~) ⟩
+
+_⊙_ : {ℓ : Level} {B1 B2 B3 : ErrorDomain}
+  (S : MyRel {ℓ} B1 B2) (R : MyRel {ℓ} B2 B3) ->  MyRel {ℓ} B1 B3
+_⊙_ {ℓ} {B1} {B2} {B3} S R = record {
+  Rel = λ b1 b3 → (∃[ b2 ∈ UB2 ] ⟨ S .Rel b1 b2 ⟩ × ⟨ R .Rel b2 b3 ⟩) , {!!} ;
+  Rel℧ = λ b3 -> ∣ (B2 .℧ , (S .Rel℧ (B2 .℧)) , R .Rel℧ b3) ∣₁ ;
+  RelΘ = λ b1~ b2~ H → ∣ (θB2 .f {!!} , {!!}) ∣₁ }
+  where
+    open ErrorDomain
+    open MonFun
+    open MyRel
+    UB1 = ⟨ 𝕌 B1 ⟩
+    UB2 = ⟨ 𝕌 B2 ⟩
+    UB3 = ⟨ 𝕌 B3 ⟩
+    θB2 = B2 .θ
+-}
+

formalizations/guarded-cubical/Semantics/Lift.agda

@@ -12,6 +12,8 @@ open import Cubical.Foundations.Function
 open import Cubical.Relation.Nullary
 open import Cubical.Data.Empty hiding (rec)
 
+open import Common.Common
+
 private
   variable
     l : Level
@@ -70,6 +72,9 @@ inj-θ : {X : Set} -> (lx~ ly~ : ▹ (L℧ X)) ->
 inj-θ lx~ ly~ H = let lx~≡ly~ = cong pred H in
   λ t i → lx~≡ly~ i t
 
+
+-- Monadic structure
+
 ret : {X : Set} -> X -> L℧ X
 ret = η
 
@@ -86,8 +91,6 @@ 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)
@@ -117,6 +120,31 @@ ext-theta f l =
   θ (fix (ext' f) <$> l) ∎
 
 
+
+monad-unit-l : ∀ (a : A) (f : A -> L℧ B) -> ext f (ret a) ≡ f a
+monad-unit-l = ext-eta
+
+monad-unit-r : (la : L℧ A) -> ext ret la ≡ la
+monad-unit-r = fix lem
+  where
+    lem : ▹ ((la : L℧ A) -> ext ret la ≡ la) ->
+          (la : L℧ A) -> ext ret la ≡ la
+    lem IH (η x) = monad-unit-l x ret
+    lem IH ℧ = ext-err ret
+    lem IH (θ x) = fix (ext' ret) (θ x)
+                     ≡⟨ ext-theta ret x ⟩
+                   θ (fix (ext' ret) <$> x)
+                     ≡⟨ refl ⟩
+                   θ ((λ la -> ext ret la) <$> x)
+                     ≡⟨ (λ i → θ λ t → IH t (x t) i) ⟩
+                   θ (id <$> x)
+                     ≡⟨ refl ⟩
+                   θ x ∎
+
+
+mapL : (A -> B) -> L℧ A -> L℧ B
+mapL f la = bind la (λ a -> ret (f a))
+
 mapL-eta : (f : A -> B) (a : A) ->
   mapL f (η a) ≡ η (f a)
 mapL-eta f a = ext-eta a λ a → ret (f a)
@@ -125,3 +153,7 @@ mapL-theta : (f : A -> B) (la~ : ▹ (L℧ A)) ->
   mapL f (θ la~) ≡ θ (mapL f <$> la~)
 mapL-theta f la~ = ext-theta (ret ∘ f) la~
 
+
+mapL-id : (la : L℧ A) -> mapL id la ≡ la
+mapL-id la = monad-unit-r la
+

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

@@ -47,6 +47,26 @@ record MonRel {ℓ' : Level} (X Y : Predomain) : Type (ℓ-suc ℓ') where
     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'
 
+module MonReasoning {ℓ' : Level} {X Y : Predomain} where
+  --open MonRel
+  module X = PosetStr (X .snd)
+  module Y = PosetStr (Y .snd)
+  _≤X_ = X._≤_
+  _≤Y_ = Y._≤_
+  
+  
+  -- _Anti⟨_⟩_: R x y -> x'≤X x -> R x' y
+  [_]_Anti⟨_⟩_ : (S : MonRel {ℓ'} X Y) ->
+    (x' : ⟨ X ⟩) -> {x : ⟨ X ⟩} -> {y : ⟨ Y ⟩} ->
+    x' ≤X x -> (S .MonRel.R) x y -> (S .MonRel.R) x' y
+  [ S ] x' Anti⟨ x'≤x ⟩ x≤y = S .MonRel.isAntitone x≤y x'≤x
+
+
+  [_]_Mon⟨_⟩_ : (S : MonRel {ℓ'} X Y) ->
+    (x : ⟨ X ⟩) -> {y y' : ⟨ Y ⟩} ->
+    (S .MonRel.R) x y -> y ≤Y y' -> (S .MonRel.R x y')
+  [ S ] x Mon⟨ x≤y ⟩ y≤y' = S .MonRel.isMonotone x≤y y≤y'
+
 predomain-monrel : (X : Predomain) -> MonRel X X
 predomain-monrel X = record {
   R = rel X ;

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

@@ -25,8 +25,9 @@ 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
+open import Semantics.PredomainInternalHom
+-- open import Syntax.GradualSTLC
+-- open import Syntax.SyntacticTermPrecision k
 
 private
   variable

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

@@ -26,6 +26,7 @@ open import Common.Common
 
 open import Semantics.Lift k
 open import Semantics.Predomains
+open import Semantics.PredomainInternalHom
 open import Semantics.Monotone.Base
 open import Semantics.Monotone.Lemmas k
 
@@ -67,7 +68,73 @@ mComp = record {
         λ a1 a2 a1≤a2 ->
           f1≤f2 (MonFun.f fAB1 a1) (MonFun.f fAB2 a2)
             (fAB1≤fAB2 a1 a2 a1≤a2) }
-     
+
+
+
+π1 : {A B : Predomain} -> ⟨ (A ×d B) ==> A ⟩
+π1 {A} {B} = record {
+  f = g;
+  isMon = g-mon }
+  where
+    g : ⟨ A ×d B ⟩ -> ⟨ A ⟩
+    g (a , b) = a
+
+    g-mon  : {p1 p2 : ⟨ A ×d B ⟩} → rel (A ×d B) p1 p2 → rel A (g p1) (g p2)
+    g-mon {γ1 , a1} {γ2 , a2} (a1≤a2 , b1≤b2) = a1≤a2
+
+
+π2 : {A B : Predomain} -> ⟨ (A ×d B) ==> B ⟩
+π2 {A} {B} = record {
+  f = g;
+  isMon = g-mon }
+  where
+    g : ⟨ A ×d B ⟩ -> ⟨ B ⟩
+    g (a , b) = b
+
+    g-mon  : {p1 p2 : ⟨ A ×d B ⟩} → rel (A ×d B) p1 p2 → rel B (g p1) (g p2)
+    g-mon {γ1 , a1} {γ2 , a2} (a1≤a2 , b1≤b2) = b1≤b2
+
+
+
+Pair : {A B : Predomain} -> ⟨ A ==> B ==> (A ×d B) ⟩
+Pair {A} = record {
+  f = λ a →
+    record {
+      f = λ b -> a , b ;
+      isMon = λ b1≤b2 → (reflexive A a) , b1≤b2 } ;
+  isMon = λ {a1} {a2} a1≤a2 b1 b2 b1≤b2 → a1≤a2 , b1≤b2 }
+
+
+
+ -- map and ap functions for later as monotone functions
+Map▹ : {A B : Predomain} ->
+  ⟨ A ==> B ⟩ -> ⟨ ▸''_ k A ==> ▸''_ k B ⟩
+Map▹ {A} {B} f = record {
+  f = map▹ (MonFun.f f) ;
+  isMon = λ {a1} {a2} a1≤a2 t → isMon f (a1≤a2 t) }
+
+Ap▹ : {A B : Predomain} ->
+  ⟨ (▸''_ k (A ==> B)) ==> (▸''_ k A ==> ▸''_ k B) ⟩
+Ap▹ {A} {B} = record { f = UAp▹ ; isMon = UAp▹-mon }
+  where
+    UAp▹ : {A B : Predomain} ->
+      ⟨ ▸''_ k (A ==> B) ⟩ -> ⟨ ▸''_ k A ==> ▸''_ k B ⟩
+    UAp▹ {A} {B} f~ = record {
+      f = _⊛_ λ t → MonFun.f (f~ t) ;
+      isMon = λ {a1} {a2} a1≤a2 t → isMon (f~ t) (a1≤a2 t) }
+
+    UAp▹-mon : {f1~ f2~ : ▹ ⟨ A ==> B ⟩} ->
+      ▸ (λ t -> rel (A ==> B) (f1~ t) (f2~ t)) ->
+      rel ((▸''_ k A) ==> (▸''_ k B)) (UAp▹ f1~) (UAp▹ f2~)
+    UAp▹-mon {f1~} {f2~} f1~≤f2~ a1~ a2~ a1~≤a2~ t = f1~≤f2~ t (a1~ t) (a2~ t) (a1~≤a2~ t)
+
+
+
+
+Next : {A : Predomain} ->
+  ⟨ A ==> ▸''_ k A ⟩
+Next = record { f = next ; isMon = λ {a1} {a2} a1≤a2 t → a1≤a2 }
+
 
 
   -- 𝕃's return as a monotone function
@@ -86,6 +153,7 @@ 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 {
@@ -214,6 +282,10 @@ IntroArg : {Γ B B' : Predomain} ->
   ⟨ B ==> B' ⟩ -> ⟨ (Γ ==> B) ==> (Γ ==> B') ⟩
 IntroArg f = Curry (mCompU f App)
 
+IntroArg1' : {Γ Γ' B : Predomain} ->
+    ⟨ Γ' ==> Γ ⟩ -> ⟨ Γ ==> B ⟩ -> ⟨ Γ' ==> B ⟩
+IntroArg1' f = {!!}
+
 
 PairAssocLR : {A B C : Predomain} ->
   ⟨ A ×d B ×d C ==> A ×d (B ×d C) ⟩

formalizations/guarded-cubical/Semantics/PredomainInternalHom.agda

+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module Semantics.PredomainInternalHom where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Relation.Binary.Poset
+
+
+open import Semantics.Predomains
+open import Semantics.Monotone.Base
+
+-- 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) ->
+  (⟨ P1 ⟩ -> ⟨ P1' ⟩ -> Type) ->
+  (⟨ P2 ⟩ -> ⟨ P2' ⟩ -> Type) ->
+  (⟨ P1 ⟩ -> ⟨ P2 ⟩) -> (⟨ P1' ⟩ -> ⟨ P2' ⟩) -> Type ℓ-zero
+fun-order-het P1 P1' P2 P2' rel-P1P1' rel-P2P2' fP1P2 fP1'P2' =
+  (p : ⟨ P1 ⟩) -> (p' : ⟨ P1' ⟩) ->
+  rel-P1P1' p p' ->
+  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 =
+  (x y : ⟨ P1 ⟩) -> x ≤P1 y -> (f1 x) ≤P2 (f2 y)
+  where
+    module P1 = PosetStr (P1 .snd)
+    module P2 = PosetStr (P2 .snd)
+    _≤P1_ = P1._≤_
+    _≤P2_ = P2._≤_
+
+{-
+mon-fun-order-refl : {P1 P2 : Predomain} ->
+  (f : ⟨ P1 ⟩ -> ⟨ P2 ⟩) ->
+  ({x y : ⟨ P1 ⟩} -> rel P1 x y -> rel P2 (f x) (f y)) ->
+  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 ⟩) ->
+  fun-order P1 P2 f g ->
+  fun-order P1 P2 g h ->
+  fun-order P1 P2 f h
+fun-order-trans {P1} {P2} f g h f≤g g≤h =
+  λ x y x≤y ->
+    P2.is-trans (f x) (g x) (h y)
+    (f≤g x x (reflexive P1 x))
+    (g≤h x y x≤y)
+   where
+     module P1 = PosetStr (P1 .snd)
+     module P2 = PosetStr (P2 .snd)
+
+
+
+mon-fun-order : (P1 P2 : Predomain) -> MonFun P1 P2 → MonFun P1 P2 → Type ℓ-zero
+mon-fun-order P1 P2 mon-f1 mon-f2 =
+  fun-order P1 P2 (MonFun.f mon-f1) (MonFun.f mon-f2)
+
+
+mon-fun-order-refl : {P1 P2 : Predomain} ->
+  (f : MonFun P1 P2) ->
+  fun-order P1 P2 (MonFun.f f) (MonFun.f f)
+mon-fun-order-refl f = λ x y x≤y -> MonFun.isMon f x≤y
+
+mon-fun-order-trans : {P1 P2 : Predomain} ->
+  (f g h : MonFun P1 P2) ->
+  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 {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
+arr' : Predomain -> Predomain -> Predomain
+arr' P1 P2 =
+  MonFun P1 P2 ,
+  -- (⟨ P1 ⟩ -> ⟨ P2 ⟩) ,
+  (posetstr
+    (mon-fun-order P1 P2)
+    (isposet {!!} {!!}
+      mon-fun-order-refl
+      
+      -- TODO can use fun-order-trans
+      (λ f1 f2 f3 Hf1-f2 Hf2-f3 x y H≤xy ->
+      -- Goal: f1 .f x ≤P2 f3 .f y
+       P2.is-trans (f1 .f x) (f2 .f x) (f3 .f y)
+         (Hf1-f2 x x (IsPoset.is-refl (P1.isPoset) x))
+         (Hf2-f3 x y H≤xy))
+      {!!}))
+  where
+    open MonFun
+    module P1 = PosetStr (P1 .snd)
+    module P2 = PosetStr (P2 .snd)
+
+
+_==>_ : Predomain -> Predomain -> Predomain
+A ==> B = arr' A B
+
+infixr 20 _==>_
+
+-- TODO show that this is a monotone relation
+
+-- TODO define version where the arguments are all monotone relations
+-- instead of arbitrary relations
+
+FunRel : {A A' B B' : Predomain} ->
+  MonRel {ℓ-zero} A A' ->
+  MonRel {ℓ-zero} B B' ->
+  MonRel {ℓ-zero} (A ==> B) (A' ==> B')
+FunRel {A} {A'} {B} {B'} RAA' RBB' =
+  record {
+    R = λ f f' → fun-order-het A A' B B'
+                   (MonRel.R RAA') (MonRel.R RBB')
+                   (MonFun.f f) (MonFun.f f') ;
+    isAntitone = {!!} ;
+    isMonotone = λ {f} {f'} {g'} f≤f' f'≤g' a a' a≤a' →
+      MonRel.isMonotone RBB' (f≤f' a a' a≤a') {!!} } -- (f'≤g' a' a' (reflexive A' a')) }

formalizations/guarded-cubical/Semantics/Predomains.agda

@@ -9,9 +9,18 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
 open import Cubical.Relation.Binary
 open import Cubical.Relation.Binary.Poset
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Bool
+open import Cubical.Data.Nat renaming (ℕ to Nat)
+open import Cubical.Data.Unit
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum
+open import Cubical.Data.Empty
 
 open import Common.Later
 
+open BinaryRelation
+
 -- Define predomains as posets
 Predomain : Set₁
 Predomain = Poset ℓ-zero ℓ-zero
@@ -29,9 +38,129 @@ transitive : (d : Predomain) -> (x y z : ⟨ d ⟩) ->
 transitive d x y z x≤y y≤z =
   IsPoset.is-trans (PosetStr.isPoset (str d)) x y z x≤y y≤z
 
+antisym : (d : Predomain) -> (x y : ⟨ d ⟩) ->
+  rel d x y -> rel d y x -> x ≡ y
+antisym d x y x≤y y≤x = IsPoset.is-antisym (PosetStr.isPoset (str d)) x y x≤y y≤x
+
+isSet-poset : {ℓ ℓ' : Level} -> (P : Poset ℓ ℓ') -> isSet ⟨ P ⟩
+isSet-poset P = IsPoset.is-set (PosetStr.isPoset (str P))
+
+isPropValued-poset : {ℓ ℓ' : Level} -> (P : Poset ℓ ℓ') -> isPropValued (PosetStr._≤_ (str P))
+isPropValued-poset P = IsPoset.is-prop-valued (PosetStr.isPoset (str P))
+
+
+-- Some common predomains
+
+-- Flat predomain from a set
+flat : hSet ℓ-zero -> Predomain
+flat h = ⟨ h ⟩ ,
+         (posetstr _≡_ (isposet (str h) (str h)
+           (λ _ → refl)
+           (λ a b c a≡b b≡c → a ≡⟨ a≡b ⟩ b ≡⟨ b≡c ⟩ c ∎)
+           λ a b a≡b _ → a≡b))
+
+𝔹 : Predomain
+𝔹 = flat (Bool , isSetBool)
+
+ℕ : Predomain
+ℕ = flat (Nat , isSetℕ)
+
+UnitP : Predomain
+UnitP = flat (Unit , isSetUnit)
+
+
+
+-- Product of predomains
+
+-- We can't use Cubical.Data.Prod.Base for products, because this version of _×_
+-- is not a subtype of the degenerate sigma type Σ A (λ _ → B), and this is needed
+-- when we define the lookup function.
+-- So we instead use Cubical.Data.Sigma.
+
+-- These aren't included in Cubical.Data.Sigma, so we copy the
+-- definitions from Cubical.Data.Prod.Base.
+proj₁ : {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} → A × B → A
+proj₁ (x , _) = x
+
+proj₂ : {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} → A × B → B
+proj₂ (_ , x) = x
+
+
+infixl 21 _×d_
+_×d_  : Predomain -> Predomain -> Predomain
+A ×d B =
+  (⟨ A ⟩ × ⟨ B ⟩) ,
+  (posetstr order (isposet isSet-prod {!!} order-refl order-trans {!!}))
+  where
+    module A = PosetStr (A .snd)
+    module B = PosetStr (B .snd)
+   
+
+    prod-eq : {a1 a2 : ⟨ A ⟩} -> {b1 b2 : ⟨ B ⟩} ->
+      (a1 , b1) ≡ (a2 , b2) -> (a1 ≡ a2) × (b1 ≡ b2)
+    prod-eq p = (λ i → proj₁ (p i)) , λ i -> proj₂ (p i)
 
+    isSet-prod : isSet (⟨ A ⟩ × ⟨ B ⟩)
+    isSet-prod (a1 , b1) (a2 , b2) p1 p2 =
+      let (p-a1≡a2 , p-b1≡b2) = prod-eq p1 in
+      let (p'-a1≡a2 , p'-b1≡b2) = prod-eq p2 in
+      {!!}
 
--- Theta for predomains
+    order : ⟨ A ⟩ × ⟨ B ⟩ -> ⟨ A ⟩ × ⟨ B ⟩ -> Type ℓ-zero
+    order (a1 , b1) (a2 , b2) = (a1 A.≤ a2) × (b1 B.≤ b2)
+
+    order-refl : BinaryRelation.isRefl order
+    order-refl = λ (a , b) → reflexive A a , reflexive B b
+
+    order-trans : BinaryRelation.isTrans order
+    order-trans (a1 , b1) (a2 , b2) (a3 , b3) (a1≤a2 , b1≤b2) (a2≤a3 , b2≤b3) =
+      (IsPoset.is-trans A.isPoset a1 a2 a3 a1≤a2 a2≤a3) ,
+       IsPoset.is-trans B.isPoset b1 b2 b3 b1≤b2 b2≤b3
+
+
+-- Sum of predomains
+
+_⊎d_ : Predomain -> Predomain -> Predomain
+A ⊎d B =
+  (⟨ A ⟩ ⊎ ⟨ B ⟩) ,
+  posetstr order (isposet {!!} {!!} order-refl order-trans order-antisym)
+  where
+    module A = PosetStr (A .snd)
+    module B = PosetStr (B .snd)
+
+    order : ⟨ A ⟩ ⊎ ⟨ B ⟩ -> ⟨ A ⟩ ⊎ ⟨ B ⟩ -> Type ℓ-zero
+    order (inl a1) (inl a2) = a1 A.≤ a2
+    order (inl a1) (inr b1) = ⊥
+    order (inr b1) (inl a1) = ⊥
+    order (inr b1) (inr b2) = b1 B.≤ b2
+
+    order-refl : BinaryRelation.isRefl order
+    order-refl (inl a) = reflexive A a
+    order-refl (inr b) = reflexive B b
+
+    order-trans : BinaryRelation.isTrans order
+    order-trans (inl a1) (inl a2) (inl a3) = transitive A a1 a2 a3
+    order-trans (inr b1) (inr b2) (inr b3) = transitive B b1 b2 b3
+
+    order-antisym : BinaryRelation.isAntisym order
+    order-antisym (inl a1) (inl a2) a1≤a2 a2≤a1 = cong inl (antisym A a1 a2 a1≤a2 a2≤a1)
+    order-antisym (inr b1) (inr b2) b1≤b2 b2≤b1 = cong inr (antisym B b1 b2 b1≤b2 b2≤b1)
+
+
+-- Functions from clocks into predomains inherit the predomain structure of the codomain.
+-- (Note: Nothing here is specific to clocks.)
+𝔽 : (Clock -> Predomain) -> Predomain
+𝔽 A = (∀ k -> ⟨ A k ⟩) ,
+  posetstr (λ x y → ∀ k -> rel (A k) (x k) (y k))
+  (isposet
+    (λ f g pf1 pf2 → λ i1 i2 k → isSet-poset (A k) (f k) (g k) (λ i' -> pf1 i' k) (λ i' -> pf2 i' k) i1 i2)
+    (λ f g pf1 pf2 i k → isPropValued-poset (A k) (f k) (g k) (pf1 k) (pf2 k) i )
+    (λ f k → reflexive (A k) (f k))
+    (λ f g h f≤g g≤h k → transitive (A k) (f k) (g k) (h k) (f≤g k) (g≤h k))
+    λ f g f≤g g≤f i k → antisym (A k) (f k) (g k) (f≤g k) (g≤f k) i)
+
+
+-- Later structure on predomains
 
 module _ (k : Clock) where
 
@@ -43,11 +172,27 @@ module _ (k : Clock) where
     ▹_ A = ▹_,_ k A
 
 
-  
-  isSet-poset : {ℓ ℓ' : Level} -> (P : Poset ℓ ℓ') -> isSet ⟨ P ⟩
-  isSet-poset P = IsPoset.is-set (PosetStr.isPoset (str P))
+  ▹' : Predomain -> Predomain
+  ▹' X = (▹ ⟨ X ⟩) ,
+         (posetstr ord (isposet isset {!!} ord-refl ord-trans ord-antisym))
+    where
+      ord : ▹ ⟨ X ⟩ → ▹ ⟨ X ⟩ → Type ℓ-zero
+      ord = λ x1~ x2~ → ▸ (λ t -> PosetStr._≤_ (str X) (x1~ t) (x2~ t))
 
+      isset : isSet (▹ ⟨ X ⟩)
+      isset = λ x y p1 p2 i j t → isSet-poset X (x t) (y t) (λ i' -> p1 i' t) (λ i' -> p2 i' t) i j
 
+      ord-refl : (a : ▹ ⟨ X ⟩) -> ord a a
+      ord-refl a = λ t → reflexive X (a t)
+
+      ord-trans : BinaryRelation.isTrans ord
+      ord-trans = λ a b c a≤b b≤c t → transitive X (a t) (b t) (c t) (a≤b t) (b≤c t)
+
+      ord-antisym : BinaryRelation.isAntisym ord
+      ord-antisym = λ a b a≤b b≤a i t -> antisym X (a t) (b t) (a≤b t) (b≤a t) i
+      
+ 
+  -- Theta for predomains
   ▸' : ▹ Predomain → Predomain
   ▸' X = (▸ (λ t → ⟨ X t ⟩)) ,
          posetstr ord
@@ -78,6 +223,12 @@ module _ (k : Clock) where
            (PosetStr.isPoset (str (X t))) (a t) (b t) (ord-ab t) (ord-ba t) i
 
 
+  -- This is the analogue of the equation for types that says that
+  -- ▸ (next A) ≡ ▹ A
+  ▸'-next : (X : Predomain) -> ▸' (next X) ≡ ▹' X
+  ▸'-next X = refl
+
+
   -- Delay for predomains
   ▸''_ : Predomain → Predomain
   ▸'' X = ▸' (next X)

formalizations/guarded-cubical/Semantics/StrongBisimulation.agda

@@ -34,7 +34,8 @@ open import Agda.Primitive
 open import Common.Common
 open import Semantics.Predomains
 open import Semantics.Lift k
-open import Semantics.ErrorDomains
+-- open import Semantics.ErrorDomains
+open import Semantics.PredomainInternalHom
 
 private
   variable
@@ -47,151 +48,6 @@ private
 
 
 
-
-
--- Flat predomain from a set
-
-flat : hSet ℓ-zero -> Predomain
-flat h = ⟨ h ⟩ ,
-         (posetstr _≡_ (isposet (str h) (str h)
-           (λ _ → refl)
-           (λ a b c a≡b b≡c → a ≡⟨ a≡b ⟩ b ≡⟨ b≡c ⟩ c ∎)
-           λ a b a≡b _ → a≡b))
-
-𝔹 : Predomain
-𝔹 = flat (Bool , isSetBool)
-
-ℕ : Predomain
-ℕ = flat (Nat , isSetℕ)
-
-UnitP : Predomain
-UnitP = flat (Unit , isSetUnit)
-
-
-
--- 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) ->
-  (⟨ P1 ⟩ -> ⟨ P1' ⟩ -> Type) ->
-  (⟨ P2 ⟩ -> ⟨ P2' ⟩ -> Type) ->
-  (⟨ P1 ⟩ -> ⟨ P2 ⟩) -> (⟨ P1' ⟩ -> ⟨ P2' ⟩) -> Type ℓ-zero
-fun-order-het P1 P1' P2 P2' rel-P1P1' rel-P2P2' fP1P2 fP1'P2' =
-  (p : ⟨ P1 ⟩) -> (p' : ⟨ P1' ⟩) ->
-  rel-P1P1' p p' ->
-  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 =
-  (x y : ⟨ P1 ⟩) -> x ≤P1 y -> (f1 x) ≤P2 (f2 y)
-  where
-    module P1 = PosetStr (P1 .snd)
-    module P2 = PosetStr (P2 .snd)
-    _≤P1_ = P1._≤_
-    _≤P2_ = P2._≤_
-
-{-
-mon-fun-order-refl : {P1 P2 : Predomain} ->
-  (f : ⟨ P1 ⟩ -> ⟨ P2 ⟩) ->
-  ({x y : ⟨ P1 ⟩} -> rel P1 x y -> rel P2 (f x) (f y)) ->
-  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 ⟩) ->
-  fun-order P1 P2 f g ->
-  fun-order P1 P2 g h ->
-  fun-order P1 P2 f h
-fun-order-trans {P1} {P2} f g h f≤g g≤h =
-  λ x y x≤y ->
-    P2.is-trans (f x) (g x) (h y)
-    (f≤g x x (reflexive P1 x))
-    (g≤h x y x≤y)
-   where
-     module P1 = PosetStr (P1 .snd)
-     module P2 = PosetStr (P2 .snd)
-
-
-
-mon-fun-order : (P1 P2 : Predomain) -> MonFun P1 P2 → MonFun P1 P2 → Type ℓ-zero
-mon-fun-order P1 P2 mon-f1 mon-f2 =
-  fun-order P1 P2 (MonFun.f mon-f1) (MonFun.f mon-f2)
-   where
-     module P1 = PosetStr (P1 .snd)
-     module P2 = PosetStr (P2 .snd)
-     _≤P1_ = P1._≤_
-     _≤P2_ = P2._≤_
-
-
-mon-fun-order-refl : {P1 P2 : Predomain} ->
-  (f : MonFun P1 P2) ->
-  fun-order P1 P2 (MonFun.f f) (MonFun.f f)
-mon-fun-order-refl f = λ x y x≤y -> MonFun.isMon f x≤y
-
-mon-fun-order-trans : {P1 P2 : Predomain} ->
-  (f g h : MonFun P1 P2) ->
-  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 {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
-arr' : Predomain -> Predomain -> Predomain
-arr' P1 P2 =
-  MonFun P1 P2 ,
-  -- (⟨ P1 ⟩ -> ⟨ P2 ⟩) ,
-  (posetstr
-    (mon-fun-order P1 P2)
-    (isposet {!!} {!!}
-      mon-fun-order-refl
-      
-      -- TODO can use fun-order-trans
-      (λ f1 f2 f3 Hf1-f2 Hf2-f3 x y H≤xy ->
-      -- Goal: f1 .f x ≤P2 f3 .f y
-       P2.is-trans (f1 .f x) (f2 .f x) (f3 .f y)
-         (Hf1-f2 x x (IsPoset.is-refl (P1.isPoset) x))
-         (Hf2-f3 x y H≤xy))
-      {!!}))
-  where
-    open MonFun
-    module P1 = PosetStr (P1 .snd)
-    module P2 = PosetStr (P2 .snd)
-
-
-_==>_ : Predomain -> Predomain -> Predomain
-A ==> B = arr' A B
-
-infixr 20 _==>_
-
-
-
--- TODO show that this is a monotone relation
-
--- TODO define version where the arguments are all monotone relations
--- instead of arbitrary relations
-
-FunRel : {A A' B B' : Predomain} ->
-  MonRel {ℓ-zero} A A' ->
-  MonRel {ℓ-zero} B B' ->
-  MonRel {ℓ-zero} (A ==> B) (A' ==> B')
-FunRel {A} {A'} {B} {B'} RAA' RBB' =
-  record {
-    R = λ f f' → fun-order-het A A' B B'
-                   (MonRel.R RAA') (MonRel.R RBB')
-                   (MonFun.f f) (MonFun.f f') ;
-    isAntitone = {!!} ;
-    isMonotone = λ {f} {f'} {g'} f≤f' f'≤g' a a' a≤a' →
-      MonRel.isMonotone RBB' (f≤f' a a' a≤a') {!!} } -- (f'≤g' a' a' (reflexive A' a')) }
-
-
-
  
 -- Lifting a heterogeneous relation between A and B to a
 -- relation between L A and L B
@@ -241,6 +97,10 @@ module LiftRelation
      ord-bot : (lb : L℧ ⟨ B ⟩) -> ℧ ≾ lb
      ord-bot lb = transport (sym (λ i → unfold-≾ i ℧ lb)) tt
 
+     ord-θ-monotone : {la~ : ▹ L℧ ⟨ A ⟩} -> {lb~ : ▹ L℧ ⟨ B ⟩} ->
+       ▸ (λ t -> la~ t ≾ lb~ t) -> θ la~ ≾ θ lb~
+     ord-θ-monotone H = ≾'->≾ H
+
 
 -- Predomain to lift predomain
 module LiftPredomain (p : Predomain) where
@@ -373,100 +233,6 @@ module LiftRelMon
 
 
 
--- Product of predomains
-
-
--- We can't use Cubical.Data.Prod.Base for products, because this version of _×_
--- is not a subtype of the degenerate sigma type Σ A (λ _ → B), and this is needed
--- when we define the lookup function.
--- So we instead use Cubical.Data.Sigma.
-
--- These aren't included in Cubical.Data.Sigma, so we copy the
--- definitions from Cubical.Data.Prod.Base.
-proj₁ : {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} → A × B → A
-proj₁ (x , _) = x
-
-proj₂ : {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} → A × B → B
-proj₂ (_ , x) = x
-
-
-infixl 21 _×d_
-_×d_  : Predomain -> Predomain -> Predomain
-A ×d B =
-  (⟨ A ⟩ × ⟨ B ⟩) ,
-  (posetstr order {!!})
-  where
-    module A = PosetStr (A .snd)
-    module B = PosetStr (B .snd)
-   
-
-    prod-eq : {a1 a2 : ⟨ A ⟩} -> {b1 b2 : ⟨ B ⟩} ->
-      (a1 , b1) ≡ (a2 , b2) -> (a1 ≡ a2) × (b1 ≡ b2)
-    prod-eq p = (λ i → proj₁ (p i)) , λ i -> proj₂ (p i)
-
-    isSet-prod : isSet (⟨ A ⟩ × ⟨ B ⟩)
-    isSet-prod (a1 , b1) (a2 , b2) p1 p2 =
-      let (p-a1≡a2 , p-b1≡b2) = prod-eq p1 in
-      let (p'-a1≡a2 , p'-b1≡b2) = prod-eq p2 in
-      {!!}
-
-    order : ⟨ A ⟩ × ⟨ B ⟩ -> ⟨ A ⟩ × ⟨ B ⟩ -> Type ℓ-zero
-    order (a1 , b1) (a2 , b2) = (a1 A.≤ a2) × (b1 B.≤ b2)
-
-    order-refl : BinaryRelation.isRefl order
-    order-refl = λ (a , b) → reflexive A a , reflexive B b
-
-    order-trans : BinaryRelation.isTrans order
-    order-trans (a1 , b1) (a2 , b2) (a3 , b3) (a1≤a2 , b1≤b2) (a2≤a3 , b2≤b3) =
-      (IsPoset.is-trans A.isPoset a1 a2 a3 a1≤a2 a2≤a3) ,
-       IsPoset.is-trans B.isPoset b1 b2 b3 b1≤b2 b2≤b3
-    
-
-    is-poset : IsPoset order
-    is-poset = isposet
-      isSet-prod
-      {!!}
-      order-refl
-      order-trans
-      {!!}
-
-
-
-π1 : {A B : Predomain} -> ⟨ (A ×d B) ==> A ⟩
-π1 {A} {B} = record {
-  f = g;
-  isMon = g-mon }
-  where
-    g : ⟨ A ×d B ⟩ -> ⟨ A ⟩
-    g (a , b) = a
-
-    g-mon  : {p1 p2 : ⟨ A ×d B ⟩} → rel (A ×d B) p1 p2 → rel A (g p1) (g p2)
-    g-mon {γ1 , a1} {γ2 , a2} (a1≤a2 , b1≤b2) = a1≤a2
-
-
-π2 : {A B : Predomain} -> ⟨ (A ×d B) ==> B ⟩
-π2 {A} {B} = record {
-  f = g;
-  isMon = g-mon }
-  where
-    g : ⟨ A ×d B ⟩ -> ⟨ B ⟩
-    g (a , b) = b
-
-    g-mon  : {p1 p2 : ⟨ A ×d B ⟩} → rel (A ×d B) p1 p2 → rel B (g p1) (g p2)
-    g-mon {γ1 , a1} {γ2 , a2} (a1≤a2 , b1≤b2) = b1≤b2
-
-
-
-Pair : {A B : Predomain} -> ⟨ A ==> B ==> (A ×d B) ⟩
-Pair {A} = record {
-  f = λ a →
-    record {
-      f = λ b -> a , b ;
-      isMon = λ b1≤b2 → (reflexive A a) , b1≤b2 } ;
-  isMon = λ {a1} {a2} a1≤a2 b1 b2 b1≤b2 → a1≤a2 , b1≤b2 }
-
-
-
 
 
 -- Induced equivalence relation on a Predomain
@@ -548,8 +314,6 @@ module Bisimilarity (d : Predomain) where
   unfold-≈ : _≈_ ≡ Inductive._≈'_ (next _≈_)
   unfold-≈ = fix-eq Inductive._≈'_
 
-  
-  
 
   module Properties where
     open Inductive (next _≈_)