predomains as posets; monotone function combinators

formalizations/guarded-cubical/ErrorDomains.agda

@@ -16,7 +16,12 @@ open import Cubical.Foundations.Transport
 
 open import Cubical.Data.Sigma
 
-open import Cubical.Data.Nat
+open import Cubical.Data.Nat hiding (_^_)
+open import Cubical.Data.Bool.Base
+open import Cubical.Data.Empty hiding (rec)
+open import Cubical.Data.Sum hiding (rec)
+
+open import Agda.Primitive
 
 private
   variable
@@ -24,7 +29,17 @@ private
     A B : Set l
 private
   ▹_ : Set l → Set l
-  ▹_ A = ▹_,_ k A 
+  ▹_ A = ▹_,_ k A
+
+
+id : {ℓ : Level} -> {A : Type ℓ} -> A -> A
+id x = x
+
+_^_ : {ℓ : Level} -> {A : Type ℓ} -> (A -> A) -> ℕ -> A -> A
+f ^ zero = id
+f ^ suc n = f ∘ (f ^ n)
+
+
 
 Predomain : Set₁
 Predomain = Poset ℓ-zero ℓ-zero
@@ -61,6 +76,18 @@ data L℧ (X : Set) : Set where
   ℧ : L℧ X
   θ : ▹ (L℧ X) → L℧ X
 
+
+EofP : Predomain → ErrorDomain
+EofP X = record {
+  X = L℧X ; ℧ = ℧ ; ℧⊥ = {!!} ;
+  θ = record { f = θ ; isMon = λ t -> {!!} } }
+  where
+    module X = PosetStr (X .snd)
+    L℧X : Predomain
+    L℧X = L℧ (X .fst) , posetstr {!X._≤_!} {!!}
+
+
+
 -- Although tempting from an equational perspective,
 -- we should not add the restriction that θ (next x) ≡ x
 -- for all x. If we did do this, we would end up collapsing
@@ -163,6 +190,7 @@ trivialize3 {X} _R_ hTrans hCong hθR = fix trivialize3'
 
 -- Showing that L is a monad
 
+{-
 mapL' : (A -> B) -> ▹ (L℧ A -> L℧ B) -> L℧ A -> L℧ B
 mapL' f map_rec (η x) = η (f x)
 mapL' f map_rec ℧ = ℧
@@ -175,7 +203,7 @@ mapL f = fix (mapL' f)
 mapL-comp : {A B C : Set} (g : B -> C) (f : A -> B) (x : L℧ A) ->
  mapL g (mapL f x) ≡ mapL (g ∘ f) x
 mapL-comp g f x = {!!}
-
+-}
 
 
 ret : {X : Set} -> X -> L℧ X
@@ -195,6 +223,8 @@ bind {A} {B} la f = (fix (bind' f)) la
 ext : (A -> L℧ B) -> L℧ A -> L℧ B
 ext f la = bind la f
 
+mapL : (A -> B) -> L℧ A -> L℧ B
+mapL f la = bind la (λ a -> ret (f a))
 
 
 bind-eta : ∀ (a : A) (f : A -> L℧ B) -> bind (η a) f ≡ f a
@@ -228,8 +258,7 @@ bind-theta f l =
   θ (fix (bind' f) <$> l) ∎
 
 
-id : {A : Set} -> A -> A
-id x = x
+
 
 
 
@@ -357,27 +386,225 @@ Dyn : Type
 Dyn = fix Dyn'
 
 -- Embedding-projection pairs
+
 record EP (A B : Set) : Set where
   field
     emb  : A -> B
     proj : B -> L℧ A
 
+=======
+data Maybe {ℓ : Level} (A : Set ℓ) : Set ℓ where
+  η : A -> Maybe A
+  ℧ : Maybe A
+
+ret-Maybe : {A : Set} -> A -> Maybe A
+ret-Maybe = η
+
+bind-Maybe : {A B : Set} ->
+  Maybe A -> (A -> Maybe B) -> Maybe B
+bind-Maybe (η x) f = f x
+bind-Maybe ℧ f = ℧
+
+data L (X : Set) : Set where
+  η : X -> L X
+  θ : ▹ (L X) -> L X
+
+Lret : {A : Set} -> A -> L A
+Lret = η
+
+Lbind' : ∀ {A B} -> (A -> L B) -> ▹ (L A -> L B) -> L A -> L B
+Lbind' f bind_rec (η x) = f x
+Lbind' f bind_rec (θ l_la) = θ (bind_rec ⊛ l_la)
+
+Lbind : L A -> (A -> L B) -> L B
+Lbind {A} {B} la f = (fix (Lbind' f)) la
+
+-- Try to show that Maybe (L A) is a monad by defining bind...
+
+mapMaybe : (A -> B) -> (Maybe A) -> Maybe B
+mapMaybe = {!!}
+
+joinMaybe : Maybe (Maybe A) -> Maybe A
+joinMaybe = {!!}
+
+joinL : L (L A) -> L A
+joinL = {!!}
+
+Lmap : (A -> B) -> L A -> L B
+Lmap = {!!}
+
+
+ret-Maybe-L : A -> Maybe (L A)
+ret-Maybe-L a = η (η a)
+
+bind-Maybe-L' :
+  (A -> Maybe (L B)) ->
+  ▹ (Maybe (L A) -> Maybe (L B)) ->
+  Maybe (L A) -> Maybe (L B)
+bind-Maybe-L' f bind-rec (η (η x)) = f x
+bind-Maybe-L' f bind-rec (η (θ l_la)) = {!!}
+ --  joinMaybe (η ( mapMaybe joinL (swap (θ λ t -> Lmap (bind-rec t) (η (η (l_la t)))))))
+bind-Maybe-L' f bind-rec ℧ = ℧
+
+bind-Maybe-L : Maybe (L A) -> (A -> Maybe (L B)) ->  Maybe (L B)
+bind-Maybe-L mla f = (fix (bind-Maybe-L' f)) mla
+
+
+MaybeL-monad-unit-l : ∀ (a : A) (f : A -> Maybe (L B)) ->
+  bind-Maybe-L (ret-Maybe-L a) f ≡ f a
+MaybeL-monad-unit-l a f = {!!}
+
+MaybeL-monad-unit-r : (mla : Maybe (L A)) -> bind-Maybe-L mla ret-Maybe-L ≡ mla
+MaybeL-monad-unit-r = fix lem
+  where
+    lem : ▹ ((mla : Maybe (L A)) -> bind-Maybe-L mla ret-Maybe-L ≡ mla) ->
+             (mla : Maybe (L A)) -> bind-Maybe-L mla ret-Maybe-L ≡ mla
+    lem IH (η (η x)) = {!!}
+    lem IH (η (θ x)) = {!!}
+    lem IH ℧ = {!!}
+
+
+record EP' (A B : Set) : Set where
+  field
+    emb : A -> B
+    proj : B -> Maybe (▹ A)
+
+record EP'' (A B : Set) : Set where
+  field
+    emb : A -> B
+    proj : B -> Maybe (L A)
+
+record EP''' (A B : Set) : Set where
+  field
+    emb : A -> B
+    proj : ▸ (λ _ -> B -> ▹ (Maybe A))
+
+record EP4 (A B : Set) : Set where
+  field
+    emb : ▹ (A -> B)
+    proj : ▹ (B -> Maybe A)
+
+record EP5 (A B : Set) : Set where
+  field
+    emb : A -> B
+    proj : B -> ▹ (Maybe A)
+
+
+
+
+fin-later : {ℓ : Level} -> Type ℓ -> Type ℓ
+fin-later A = Σ ℕ λ n -> (_^_ ▹_ n) (Maybe A)
+
+fin-later-bind' : (A -> fin-later B) ->
+  ▹ (fin-later A -> fin-later B) ->
+     fin-later A -> fin-later B
+fin-later-bind' f rec (n , ▹^n-f) = {!!} , {!!}
+
+many▹intro : (n : ℕ) -> (A -> B) -> (▹_ ^ n) A -> (▹_ ^ n) B
+many▹intro zero = id
+many▹intro (suc n) f l_ln_a = λ t → (many▹intro n f) (l_ln_a t)
+
+lemma : (n m : ℕ) -> (▹_ ^ m) ((▹_ ^ n) B) ≡ (▹_ ^ (m + n)) B
+lemma = {!!}
+
+many▹bind : {n m p : ℕ} -> n + m ≡ p -> (▹_ ^ n) A -> (A -> (▹_ ^ m) B) -> (▹_ ^ (n + m)) B
+many▹bind {n = n} {m = m} {p = p} eq a f =
+  transport (lemma m n) (many▹intro n f a) --  (many▹intro {!!} f a)
+  -- many▹intro {!!} f a
+-- many▹bind {n = zero} {m = m} eq a f = {!!}
+-- many▹bind {n = suc n} {m = m} eq = {!!}
+
+record EP6 (A B : Type) (n : ℕ) : Type where
+  field
+    emb : A -> B
+    proj : B -> (▹_ ^ n) (Maybe A)
+
+
 -- E-P Pair for a type with itself
 EP-id : (A : Type) -> EP A A
 EP-id A = record {
   emb = id;
   proj = ret }
 
--- Composing EP pairs
+EP'''-id : (A : Type) -> EP''' A A
+EP'''-id A = record {
+  emb = {!!};
+  proj = {!!} }
 
+EP4-id : (A : Type) -> EP4 A A
+EP4-id A = record {
+  emb = {!!};
+  proj = next (ret-Maybe) }
+
+EP6-id : (A : Type) (n : ℕ) -> EP6 A A n
+EP6-id A n = record {
+  emb = {!!};
+  proj = {!!} }
+
+-- Composing EP pairs
 EP-comp : {A B C : Type} -> EP A B -> EP B C -> EP A C
 EP-comp epAB epBC = record {
   emb =  λ a -> emb epBC (emb epAB a) ;
   proj = λ c -> bind (proj epBC c) (proj epAB) }
   where open EP
 
--- E-P pair between a type and its lift
 
+EP-later : {A : Type} -> EP' A B -> EP' (▹ A) (▹ B)
+EP-later epAB = record {
+  emb = λ a -> next (emb epAB {!!});
+  proj = λ lb -> {!!} }
+  where open EP'
+   
+EP-comp-precise : {A B C : Type} -> EP' A (▹ B) -> EP' (B) (C) -> EP' A (▹ C)
+EP-comp-precise epAB epBC = record {
+  emb =  λ a -> {!!};
+  proj = λ c -> bind-Maybe (proj epBC {!!}) (proj {!!}) }
+  where open EP'
+
+   
+EP-comp4 : {A B C : Type} -> EP4 A B -> EP4 B C -> EP4 A C
+EP-comp4 epAB epBC = record {
+  emb =  λ t a -> emb epBC t (emb epAB t a) ;
+  proj = λ t c -> bind-Maybe (proj epBC t c) λ b -> proj epAB t b}
+  where open EP4
+
+EP-comp5 : {A B C : Type} -> EP5 A B -> EP5 B C -> EP5 A C
+EP-comp5 epAB epBC = record {
+  emb =  λ a -> emb epBC (emb epAB a) ;
+  proj = λ c t -> bind-Maybe (proj epBC c t) (λ b -> {!!}) } -- proj epAB b t is invalid
+  where open EP5
+
+EP-comp6 : {A B C : Type} -> {n m : ℕ} -> EP6 A B n -> EP6 B C m -> EP6 A C (n + m)
+EP-comp6 {n = n} {m = m} epAB epBC = record {
+  emb =  λ a -> emb epBC (emb epAB a) ;
+  proj = λ c -> {!!} }
+  -- many▹bind {n = m} {m = n} {p = n + m} {!!} (proj epBC c) (λ b -> proj epAB b) }
+  -- many▹bind (proj epBC c) (λ b -> proj epAB b) }
+  where open EP6
+
+
+
+{-
+EP-comp-precise2 : {A B C : Type} -> EP'' A B -> EP'' B C -> EP'' A C
+EP-comp-precise2 epAB epBC = record {
+  emb =  λ a -> emb epBC (emb epAB a) ;
+  proj = λ c -> bind-Maybe
+    (proj epBC c)
+    (λ lb -> bind-Maybe {!!} {!!}) }
+  where open EP'' 
+-}
+
+{-
+EP'''-comp : {A B C : Type} -> EP''' A B -> EP''' B C -> EP''' A C
+EP'''-comp epAB epBC = record {
+  emb = λ t -> λ a -> emb epBC t (emb epAB t a) ;
+  proj = λ t -> λ c -> λ t' ->
+    bind-Maybe (proj epBC t c t) (λ b -> proj epAB t b t) }
+  where open EP'''
+-}
+
+
+-- E-P pair between a type and its lift
 EP-L : {A : Type} -> EP A B -> EP (L℧ A) (L℧ B)
 EP-L epAB = record {
   emb = λ la -> mapL (emb epAB) la;
@@ -386,7 +613,6 @@ EP-L epAB = record {
 
 
 -- E-P Pair for nat
-
 e-nat : ℕ -> Dyn
 e-nat n = transport (sym (fix-eq Dyn')) (nat n) 
 
@@ -409,7 +635,6 @@ EP-nat = record {
 
 
 -- E-P Pair for functions Dyn to L℧ Dyn
-
 e-fun : (Dyn -> L℧ Dyn) -> Dyn
 e-fun f = transport (sym (fix-eq Dyn'))
   (arr (next f))
@@ -440,9 +665,57 @@ EP-fun = record {
 
 
 
--- Lifting retractions to functions
 
-module LiftRetraction
+p-fun-precise' : Dyn' (next Dyn) -> (Maybe (▹ (Dyn -> L℧ Dyn)))
+p-fun-precise' (nat x) = ℧
+p-fun-precise' (arr x) = η x -- (ret <$> x) -- could also define using tick
+
+p-fun-precise : Dyn -> (Maybe (▹ (Dyn -> L℧ Dyn)))
+p-fun-precise d = p-fun-precise' (transport (fix-eq Dyn') d)
+
+
+fun-retract-precise : (f : (Dyn -> L℧ Dyn)) ->
+  p-fun-precise (e-fun f) ≡ η (next f)
+fun-retract-precise f =
+  p-fun-precise' (transport (fix-eq Dyn') (transport (sym (fix-eq Dyn')) (arr (next f))))
+                         ≡⟨ {!!} ⟩
+  p-fun-precise' (arr (next f)) ∎
+
+
+e-fun4 : ▹ ((Dyn -> L℧ Dyn) -> Dyn)
+e-fun4 = next (λ f -> transport (sym (fix-eq Dyn')) (arr (next f)))
+
+p-fun4' : (Dyn' (next Dyn) -> Maybe (Dyn -> L℧ Dyn))
+p-fun4' (nat x) = ℧
+p-fun4' (arr f) = η λ d -> θ (λ t -> f t d)
+ 
+p-fun4 : ▹ (Dyn -> Maybe (Dyn -> L℧ Dyn))
+p-fun4 = next λ d -> p-fun4' (transport (fix-eq Dyn') d)
+
+EP4-fun : EP4 (Dyn -> L℧ Dyn) Dyn
+EP4-fun = record {
+  emb = e-fun4;
+  proj = p-fun4 }
+
+
+EP4-fun-retract : (f : (Dyn -> L℧ Dyn)) (t : Tick k) ->
+  p-fun4 t (e-fun4 t f) ≡ η f
+EP4-fun-retract f t =
+  p-fun4' (transport (fix-eq Dyn') (e-fun4 t f)) ≡⟨ refl ⟩
+  p-fun4' (transport (fix-eq Dyn') (transport (sym (fix-eq Dyn')) (arr (next f)))) ≡⟨ {!!} ⟩
+  p-fun4' (arr (next f)) ≡⟨ refl ⟩
+  (η λ d -> θ (λ t' -> (next f) t' d)) ≡⟨ refl ⟩
+  (η λ d -> θ (λ t' -> f d)) ≡⟨ refl ⟩
+  (η λ d -> θ (next (f d))) ≡⟨ {!!} ⟩
+  (η ((next f) t)) ≡⟨  refl ⟩
+  η f ∎
+
+
+-- transport (sym (fix-eq Dyn')) (arr (next f))
+
+
+-- Lifting retractions to functions
+module ArrowRetraction
   {A A' B B' : Set}
   (epAA' : EP A A')
   (epBB' : EP B B') where
@@ -468,9 +741,95 @@ EP-lift : {A A' B B' : Set} ->
 EP-lift epAA' epBB' = record {
   emb = e-lift;
   proj = p-lift  }
-  where open LiftRetraction epAA' epBB'
+  where open ArrowRetraction epAA' epBB'
+
+
+
+
+--------------------------------------------------------------------------
+
+
+-- Ordering on terms
+
+  {-
+  record Predomain (ℓ ℓ' : Level) (X : Type ℓ) : Type (ℓ-max ℓ (ℓ-suc ℓ')) where
+      _≾X_ : X -> X -> Type
+      pst : IsPoset _≾X_
+  -}
+
+
+U : ErrorDomain -> Type
+U d = (ErrorDomain.X d) .fst
+
+δ : {X : Type} -> L℧ X -> L℧ X
+δ = θ ∘ next
+  where open L℧
+
+
+      
+
+-- Should this be on Predomains?
+module Relation (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
+
+
+  module Properties where
+
+  -- To show that this is not transitive:
+  -- Prove that it's not trivial (i.e., η true is not related to η false.
+  -- Should follow by definition.)
+  -- Appeal to lemma: it is a congruence with respect to θ,
+  -- so if it were transitive, then by the lemma, it would be trivial.
+
+
+    non-trivial : Σ (U d) (λ x -> Σ (U d) (λ y -> x ≡ y -> ⊥)) ->
+                  Σ (U d) (λ x -> Σ (U d) (λ y -> (η x) ≾ (η y) -> ⊥))
+    non-trivial (x , y , H-contra) = x , (y , (λ H-contra2 → H-contra {!!}))
+
+    lem-rewrite : (lx ly : ▹ (L℧ (U d))) ->
+           (θ lx ≾ θ ly) ≡ (Inductive._≾'_ (next (_≾_)) (θ lx) (θ ly))
+    lem-rewrite lx ly =
+      (fix Inductive._≾'_) (θ lx) (θ ly)
+
+             -- can't come up with this through refining:
+             ≡⟨ (λ i -> fix-eq (Inductive._≾'_) i (θ lx) (θ ly)) ⟩
+                      
+      (Inductive._≾'_ (next (_≾_)) (θ lx) (θ ly)) ∎
+
+   -- fix _≾'_ ≡ _≾'_ (next (_≾_))
+   -- fix _≾'_ (θ lx) (θ ly) ≡  _≾'_ (next (_≾_)) (θ lx) (θ ly)
+
 
+    θ-cong : congruence _≾_
+    θ-cong {lx} {ly} h = transport (sym (lem-rewrite lx ly)) h
 
+                
 
 
 

formalizations/guarded-cubical/GradualSTLC.agda

@@ -26,6 +26,59 @@ data _⊑_ : Ty -> Ty -> Set where
     A ⊑ (dyn => dyn) -> A ⊑ dyn
   -- inj-arrow : {A A' : Ty} ->
   --   (A => A') ⊑ (dyn => dyn) -> (A => A') ⊑ dyn
+  
+  -- inj-arrow could be made more compositional by having a
+  -- case for composition of EP pairs and a case for
+  -- dyn => dyn ⊑ dyn
+
+⊑ref : (A : Ty) -> A ⊑ A
+⊑ref nat = nat
+⊑ref dyn = dyn
+⊑ref (A1 => A2) = (⊑ref A1) => (⊑ref A2)
+
+{-
+data ltdyn : ℕ -> Ty -> Ty -> Set where
+  dyn : {n : ℕ} -> ltdyn n dyn dyn
+  _=>_ : {A A' B B' : Ty} {n m p : ℕ} ->
+    {eq : p ≡ n + m} ->
+    ltdyn n A A' -> ltdyn m B B' ->
+    ltdyn p (A => B) (A' => B')
+  nat : {n : ℕ} -> ltdyn n nat nat
+  inj-nat : {n : ℕ} -> ltdyn n nat dyn
+  inj-arrow : {A : Ty} -> {n : ℕ} ->
+    ltdyn n A (dyn => dyn) -> ltdyn n A dyn
+
+
+_⊑[_]_ : Ty -> ℕ -> Ty -> Set
+A ⊑[ n ] B = ltdyn n A B
+-}
+
+
+{-
+max-sum : (a b c d : ℕ) ->
+  max (a + b) (c + d) ≡ max a c + max b d
+max-sum zero b zero d = refl
+max-sum zero b (suc c) d = {!!}
+max-sum (suc a) b c d = {!!}
+-}
+
+{-
+ltdyn-transitive : {A B C : Ty} -> {n m p : ℕ} ->
+   p ≡ n + m -> A ⊑[ n ] B -> B ⊑[ m ] C -> A ⊑[ p ] C
+ltdyn-transitive _ dyn dyn = dyn
+ltdyn-transitive {A => B} {A' => B'} {A'' => B''} {n} {m} {p}
+  eq (_=>_ {eq = eq1} dAA' dBB') (_=>_ {eq = eq2} dA'A'' dB'B'') =
+  _=>_ {n = {!?!}} {m = {!!}} {p = {!!}} {eq = {!!}}
+    (ltdyn-transitive {!!} dAA' dA'A'')
+    (ltdyn-transitive {!!} dBB' dB'B'')
+ltdyn-transitive eq (dAA' => dBB') (inj-arrow dBC) = {!!}
+ltdyn-transitive _ nat nat = nat
+ltdyn-transitive _ nat inj-nat = inj-nat
+ltdyn-transitive _ inj-nat dyn = inj-nat
+ltdyn-transitive eq (inj-arrow dA-dyn-dyn) dyn =
+  inj-arrow (ltdyn-transitive _ dA-dyn-dyn (dyn => dyn))
+-}
+
 
 module ⊑-properties where
   -- experiment with modules
@@ -85,6 +138,8 @@ data Tm : Ctx -> Ty -> Set where
   err : ∀ {Γ A} -> Tm Γ A
   up  : ∀ {Γ A B} -> A ⊑ B -> Tm Γ A -> Tm Γ B
   dn  : ∀ {Γ A B} -> A ⊑ B -> Tm Γ B -> Tm Γ A
+  zro : ∀ {Γ} -> Tm Γ nat
+  suc : ∀ {Γ} -> Tm Γ nat -> Tm Γ nat
 
 -- infix 4 _▸_
 
@@ -141,6 +196,8 @@ trav K τ (app f s) = app (trav K τ f) (trav K τ s)
 trav K τ (up deriv t') = up deriv (trav K τ t')
 trav K τ (dn deriv t') = dn deriv (trav K τ t')
 trav K τ err = err
+trav K τ zro = zro
+trav K τ (suc t') = suc (trav K τ t')
 
 -- Renaming --
 
@@ -168,3 +225,36 @@ termKit = kit var idTerm weakenTerm
 
 sub : (Δ Γ : Ctx) (σ : Subst Δ Γ Tm) (T : Ty) (t : Tm Γ T) -> Tm Δ T
 sub Δ Γ σ T t = trav termKit σ t
+
+-- Single substitution
+-- N[M/x]
+
+_[_] : ∀ {Γ A B}
+  → Tm (Γ :: B) A
+  → Tm Γ B
+  → Tm Γ A
+_[_] {Γ} {A} {B} N M = sub Γ (Γ :: B) σ A N -- sub {!!} {!!} {!!} {!!} {!!}
+  where
+    σ : Subst Γ (Γ :: B) Tm -- i.e., {T : Ty} → Γ :: B ∋ T → Tm Γ T
+    σ vz = M
+    σ (vs x) = var x
+
+
+-- Values --
+
+data Value : ∀ {Γ} {A} -> Tm Γ A -> Set where
+  VLam : ∀ {Γ A B} -> {N : Tm (Γ :: A) B} -> Value (lda N)
+  VZero : ∀ {Γ} -> Value {Γ} zro
+  VSuc : ∀ {Γ} -> {V : Tm Γ nat} ->
+    Value V ->
+    Value (suc V)
+  VUpFun : ∀ {Γ} {Ain Aout Bin Bout} ->
+    {cin : Ain ⊑ Bin} {cout : Aout ⊑ Bout} ->
+    {V : Tm Γ (Ain => Aout)} ->
+    Value V ->
+    Value (up (cin => cout) V)
+  VDnFun : ∀ {Γ} {Ain Aout Bin Bout} ->
+    {cin : Ain ⊑ Bin} {cout : Aout ⊑ Bout} ->
+    {V : Tm Γ (Bin => Bout)} ->
+    Value V ->
+    Value (dn (cin => cout) V)

formalizations/guarded-cubical/Interpretation.agda

@@ -44,12 +44,7 @@ module Interpretation (k : Clock)  where
   look env A vz = proj₂ env
   look env A (vs {Γ} {S} {T} x) = look (proj₁ env) A x
 
-  {-
-  lookup : (Γ : Ctx) -> (A : Ty) -> (x : Γ ∋ A) -> ⟦ A ⟧ty
-  lookup (Γ :: A) A vz =  proj₂ {!!}
-  lookup Γ A (vs y) = {!!}
-  -}
-
+{-
   ⟦_⟧lt : {A B : Ty} -> A ⊑ B -> EP ⟦ A ⟧ty ⟦ B ⟧ty
   ⟦ dyn ⟧lt = EP-id Dyn
   ⟦ A⊑A' => B⊑B' ⟧lt = EP-lift ⟦ A⊑A' ⟧lt ⟦ B⊑B' ⟧lt
@@ -57,6 +52,11 @@ module Interpretation (k : Clock)  where
   ⟦ inj-nat ⟧lt = EP-nat
   ⟦ inj-arrow (A-dyn => B-dyn) ⟧lt =
     EP-comp (EP-lift  ⟦ A-dyn ⟧lt  ⟦ B-dyn ⟧lt) EP-fun
+-}
+
+  ⟦_⟧lt : {A B : Ty} {n : ℕ} -> A ⊑[ n ] B -> EP ⟦ A ⟧ty ⟦ B ⟧ty
+  
+  
 
 
   ⟦_⟧tm : {Γ : Ctx} {A : Ty} -> Tm Γ A -> (⟦ Γ ⟧ctx -> L℧ ⟦ A ⟧ty)

formalizations/guarded-cubical/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 Later
+
+module 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 StrongBisimulation k
+open import GradualSTLC
+open import SyntacticTermPrecision k
+
+private
+  variable
+    l : Level
+    A B : Set l
+private
+  ▹_ : Set l → Set l
+  ▹_ A = ▹_,_ k A
+
+open 𝕃
+
+{-
+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 
+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-ord B i (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 (next (ord B))
+          (ext' f  (next (ext f))  la)
+          (ext' f' (next (ext f')) la')) ->
+     (la la' : ⟨ 𝕃 A ⟩) ->
+       ord' A (next (ord A)) la la' ->
+       ord' B (next (ord B))
+        (ext' f  (next (ext f))  la)
+        (ext' f' (next (ext f')) la')
+    monotone-ext' f f' f≤f' IH (η x) (η y) x≤y =
+      transport
+      (λ i → unfold-ord 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-ord 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-ord 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 : {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/MonFuns.agda

+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Later
+
+module MonFuns (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 StrongBisimulation k
+open import GradualSTLC
+open import SyntacticTermPrecision k
+open import Lemmas k
+
+
+private
+  variable
+    l : Level
+    A B : Set l
+private
+  ▹_ : Set l → Set l
+  ▹_ A = ▹_,_ k A
+
+
+open 𝕃
+
+abstract
+
+  -- Composing monotone functions
+  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 → mComp' 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) }
+    where
+      mComp' : {A B C : Predomain} -> MonFun B C -> MonFun A B -> MonFun A C
+      mComp' f1 f2 = record {
+        f = λ a -> f1 .f (f2 .f a) ;
+        isMon = λ x≤y -> f1 .isMon (f2 .isMon x≤y) }
+        where open MonFun
+
+
+  -- 𝕃's return as a monotone function
+  mRet : {A : Predomain} -> ⟨ A ==> 𝕃 A ⟩
+  mRet {A} = record { f = ret ; isMon = ord-η-monotone A }
+
+
+  -- Extending a monotone function to 𝕃
+  mExt : {A B : Predomain} -> ⟨ (A ==> 𝕃 B) ==> (𝕃 A ==> 𝕃 B) ⟩
+  mExt = record {
+    f = mExt' ;
+    isMon = λ {f1} {f2} f1≤f2  -> ext-monotone (MonFun.f f1) (MonFun.f f2) f1≤f2 }
+    where
+      mExt' : {A B : Predomain} -> MonFun A (𝕃 B) -> MonFun (𝕃 A) (𝕃 B)
+      mExt' f = record {
+        f = λ la -> bind la (MonFun.f f) ;
+        isMon = monotone-bind-mon f }
+
+
+  -- Monotone successor function
+  mSuc : ⟨ ℕ ==> ℕ ⟩
+  mSuc = record {
+    f = suc ;
+    isMon = λ {n1} {n2} n1≤n2 -> λ i -> suc (n1≤n2 i) }
+
+
+  -- Combinators
+
+  S : {Γ A B : Predomain} ->
+    ⟨ Γ ==> A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+  S f g =
+    record {
+      f = λ γ -> MonFun.f (MonFun.f f γ) (MonFun.f g γ) ;
+      isMon = λ {γ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} -> ⟨ Γ ==> 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 f = record { f = λ γ →
+    record { f = λ a → MonFun.f f (γ , a) ; isMon = {!!} } ; isMon = {!!} }
+
+  Uncrry : {Γ A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ (Γ ×d A) ==> B ⟩
+  Uncrry = {!!}
+
+  swap : {Γ 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 → {!!} }
+
+
+  -- Convenience versions of comp, ext, and ret using combinators
+
+  mComp' : {Γ A B C : Predomain} ->
+    ⟨ (Γ ==> B ==> C) ⟩ -> ⟨ (Γ ==> A ==> B) ⟩ -> ⟨ (Γ ==> A ==> C) ⟩
+  mComp' f g = (K mComp) <*> f <*> g
+
+  _∘m_ :  {Γ A B C : Predomain} ->
+    ⟨ (Γ ==> B ==> C) ⟩ -> ⟨ (Γ ==> A ==> B) ⟩ -> ⟨ (Γ ==> A ==> C) ⟩
+  f ∘m g = mComp' f g
+  infixl 20 _∘m_
+
+  mExt' : {Γ A B : Predomain} ->
+    ⟨ (Γ ==> A ==> 𝕃 B) ⟩ -> ⟨ (Γ ==> 𝕃 A ==> 𝕃 B) ⟩
+  mExt' f = K mExt <*> f
+
+  mRet' : {Γ A : Predomain} -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> 𝕃 A ⟩
+  mRet' a = K mRet <*> a
+
+
+  -- Mapping a monotone function
+  mMap : {A B : Predomain} -> ⟨ (A ==> B) ==> (𝕃 A ==> 𝕃 B) ⟩
+  mMap = {!!} -- mExt' (mComp' (Curry {!!}) {!!}) -- mExt (mComp mRet f)
+
+
+  mMap' : {Γ A B : Predomain} ->
+    ⟨ (Γ ==> A ==> B) ⟩ -> ⟨ (Γ ==> 𝕃 A ==> 𝕃 B) ⟩
+  mMap' = {!!}
+
+
+  {-
+  -- 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 fA'LA fBB' = (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 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)

formalizations/guarded-cubical/Results.agda

+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+open import Later
+
+module Results (k : Clock) where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat renaming (ℕ to Nat) hiding (_·_)
+open import Cubical.Foundations.Structure
+
+open import StrongBisimulation k
+open import Semantics k
+open import SyntacticTermPrecision k
+open import GradualSTLC
+
+private
+  variable
+    l : Level
+    A B : Set l
+private
+  ▹_ : Set l → Set l
+  ▹_ A = ▹_,_ k A
+
+
+gradual_guarantee : (M : Tm · nat) (N : Tm · nat) ->
+                    · |- M ⊑tm N # nat ->
+                    ⟦ M ⟧ ≲ ⟦ N ⟧

formalizations/guarded-cubical/Semantics.agda

+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Later
+
+module Semantics (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.Prod
+open import Cubical.Data.Sigma
+open import Cubical.Data.Empty
+
+open import Cubical.Foundations.Function
+
+open import StrongBisimulation k
+open import GradualSTLC
+open import SyntacticTermPrecision k
+open import Lemmas k
+open import MonFuns k
+
+private
+  variable
+    l : Level
+    A B : Set l
+private
+  ▹_ : Set l → Set l
+  ▹_ A = ▹_,_ k A
+
+
+
+open 𝕃
+
+-- Denotations of Types
+
+{-
+
+-- First definition of Dyn'
+
+data Dyn' (D : ▹ Type) : Type where
+  nat : Nat -> Dyn' D
+  fun : (▸ D -> L℧ (Dyn' D)) -> Dyn' D
+
+-- Dyn' is a recursive sum type, so we can
+-- define the ordering inductively
+-- (same way as you'd define an ordering on lists)
+
+DynP' : (D : ▹ Predomain) -> Predomain
+DynP' D = Dyn' (λ t -> ⟨ D t ⟩) ,
+          posetstr order {!!}
+
+      where
+
+      order : Dyn' (λ t → ⟨ D t ⟩) → Dyn' (λ t → ⟨ D t ⟩) → Type ℓ-zero
+      order (nat n1) (nat n2) = n1 ≡ n2
+      order (fun f) (fun g) = ∀ x y ->
+        rel (▸' D) x y ->
+        cust-order (f x) (g y)
+          where
+            cust-order' :
+             ▹ (L℧ (Dyn' (λ t → ⟨ D t ⟩)) -> L℧ (Dyn' (λ t → ⟨ D t ⟩)) -> Type) ->
+                L℧ (Dyn' (λ t → ⟨ D t ⟩)) -> L℧ (Dyn' (λ t → ⟨ D t ⟩)) -> Type
+            cust-order' _ ℧ _ = Unit
+            cust-order' rec (η x) (η y) = order x y
+            cust-order' _ (η _) _ = ⊥
+            cust-order' rec (θ lx~) (θ ly~) = {!!}
+            cust-order' _ (θ _) _ = ⊥
+
+            cust-order :  L℧ (Dyn' (λ t → ⟨ D t ⟩)) -> L℧ (Dyn' (λ t → ⟨ D t ⟩)) -> Type
+            cust-order = fix cust-order'
+         
+      order _ _ = ⊥
+-}
+
+-- Alternate definition of Dyn' (different encoding of function case)
+
+{-
+data Dyn' (T : ▹ Type) : Type where
+  nat : Nat -> Dyn' T
+  fun  : ▸ (λ t → T t -> L℧ (T t)) -> Dyn' T
+
+DynP' : (D : ▹ Predomain) -> Predomain
+DynP' D = Dyn' (λ t -> ⟨ D t ⟩) , posetstr order {!!}
+  where
+    order : Dyn' (λ t → ⟨ D t ⟩) → Dyn' (λ t → ⟨ D t ⟩) → Type ℓ-zero
+    order (nat n1) (nat n2) = n1 ≡ n2
+    order (fun f) (fun g) = ∀ x y ->
+      rel (▸' D) x y ->
+      ▸ λ t -> rel (𝕃 (D t)) (f t (x t)) (g t (y t))
+    order _ _ = ⊥
+-}
+
+----------------------------------------------------------
+-- Third definition of DynP, where we build in the requirement that
+-- the functions must be monotone
+
+data Dyn' (D : ▹ Predomain) : Type where
+  nat : Nat -> Dyn' D
+  fun : ▸ (λ t → MonFun (D t) (𝕃 (D t))) -> Dyn' D
+
+DynP' : (D : ▹ Predomain) -> Predomain
+DynP' D = (Dyn' D) ,
+  (posetstr order
+    (isposet (λ x y pf1 pf2 → {!!}) {!!} order-refl order-trans {!!}))
+  where
+    order : Dyn' D → Dyn' D → Type ℓ-zero
+    order (nat n1) (nat n2) = n1 ≡ n2
+    order (fun f) (fun g) = ▸ λ t ->
+      mon-fun-order (D t) (𝕃 (D t)) (f t) (g t)
+    order _ _ = ⊥
+
+    {-
+    order (fun f) (fun g) = ∀ x y ->
+      rel (▸' D) x y ->
+      ▸ λ t -> rel (𝕃 (D t)) (MonFun.f (f t) (x t)) (MonFun.f (g t) (y t))
+    -}
+
+    order-refl : (d : Dyn' D) -> order d d
+    order-refl (nat n) = refl
+    order-refl (fun f) = λ t → mon-fun-order-refl (f t)
+
+    order-trans : BinaryRelation.isTrans order
+    order-trans (nat n1) (nat n2) (nat n3) n1≡n2 n2≡n3 =
+      n1 ≡⟨ n1≡n2 ⟩ n2 ≡⟨ n2≡n3 ⟩ n3 ∎
+    order-trans (fun f1) (fun f2) (fun f3) later-f1≤f2 later-f2≤f3 =
+      λ t →
+        mon-fun-order-trans (f1 t) (f2 t) (f3 t) (later-f1≤f2 t) (later-f2≤f3 t)
+
+
+
+----------------------------------------------------------
+
+--DynP P = (▸ (λ t -> Dyn' (next ⟨ P t ⟩))) , posetstr {!!} {!!}
+
+DynP : Predomain
+DynP = fix DynP'
+
+unfold-DynP : DynP ≡ DynP' (next DynP)
+unfold-DynP = fix-eq DynP'
+
+
+
+-- Equation for the underlying set of DynP
+{-
+unfold-⟨DynP⟩ : ⟨ DynP ⟩ ≡ Dyn' (next ⟨ DynP ⟩)
+unfold-⟨DynP⟩ =
+  ⟨ fix DynP' ⟩                    ≡⟨ (λ i → ⟨ unfold-DynP i ⟩ ) ⟩
+  ⟨ DynP' (next DynP) ⟩            ≡⟨ refl ⟩
+  Dyn' (λ t -> ⟨ (next DynP) t ⟩)  ≡⟨ refl ⟩
+  Dyn' (next ⟨ DynP ⟩) ∎
+-}
+
+
+unfold-⟨DynP⟩ : ⟨ DynP ⟩ ≡ ⟨ DynP' (next DynP) ⟩
+unfold-⟨DynP⟩ = λ i → ⟨ unfold-DynP i ⟩
+
+-- Converting from the underlying set of DynP' to the underlying
+-- set of DynP
+DynP'-to-DynP : ⟨ DynP' (next DynP) ⟩ -> ⟨ DynP ⟩
+DynP'-to-DynP d = transport (sym (λ i -> ⟨ unfold-DynP i ⟩)) d
+
+DynP-to-DynP' : ⟨ DynP ⟩ -> ⟨ DynP' (next DynP) ⟩
+DynP-to-DynP' d = transport (λ i → ⟨ unfold-DynP i ⟩) d
+
+
+-- This basically is a monotonicity result, and could be
+-- incorporated as a constant into the combinator language.
+DynP-rel : ∀ d1 d2 ->
+  rel (DynP' (next DynP)) d1 d2 ->
+  rel DynP (DynP'-to-DynP d1) (DynP'-to-DynP d2)
+DynP-rel d1 d2 d1≤d2 = transport
+  (λ i → rel (unfold-DynP (~ i))
+    (transport-filler (λ j -> ⟨ unfold-DynP (~ j) ⟩) d1 i)
+    (transport-filler (λ j -> ⟨ unfold-DynP (~ j) ⟩) d2 i))
+  d1≤d2
+
+
+{-
+rel-lemma : ∀ d1 d2 ->
+  rel (DynP' (next DynP)) d1 d2 ->
+  rel DynP (transport (sym unfold-⟨DynP⟩) d1) (transport (sym unfold-⟨DynP⟩) d2)
+rel-lemma d1 d2 d1≤d2 = {!!}
+transport
+  (λ i -> rel (unfold-DynP (~ i))
+    (transport-filler (λ j -> sym unfold-⟨DynP⟩ j ) d1 i)
+    {!!}
+    --(transport-filler (sym unfold-⟨DynP⟩) d1 i)
+    --(transport-filler (sym unfold-⟨DynP⟩) d2 i)
+  )
+  d1≤d2
+-}
+
+
+
+-------------------------------------
+-- *** Embedding-projection pairs ***
+
+
+record EP (A B : Predomain) : Set where
+  field
+    emb : MonFun A B
+    proj : MonFun B (𝕃 A)
+
+
+-- Identity E-P pair
+
+EP-id : (A : Predomain) -> EP A A
+EP-id A = record {
+  emb = record { f = id ; isMon = λ x≤y → x≤y };
+  proj = record { f = ret ; isMon = ord-η-monotone A }}
+
+
+
+-- E-P Pair for nats
+
+≤ℕ-eq : {x y : ⟨ ℕ ⟩} -> (rel ℕ) x y -> x ≡ y
+≤ℕ-eq {x} {y} x≤y = x≤y
+
+e-nat : ⟨ ℕ ==> DynP ⟩
+e-nat = record {
+  f = λ n -> DynP'-to-DynP (nat n) ;  -- transport (sym unfold-⟨DynP⟩) (nat n) ;
+  isMon = λ {x} {y} x≤y → DynP-rel (nat x) (nat y) (≤ℕ-eq x≤y) }
+
+p-nat' : ⟨ DynP' (next DynP) ==> 𝕃 ℕ ⟩
+p-nat' = record { f = g ; isMon = g-mon }
+  where
+    g : ⟨ DynP' (next DynP) ⟩ → ⟨ 𝕃 ℕ ⟩ 
+    g (nat n) = ret n
+    g (fun f) = ℧
+
+    g-mon : {x y : ⟨ DynP' (next DynP) ⟩} →
+      (rel (DynP' (next DynP)) x y) →
+      (rel (𝕃 ℕ) (g x) (g y))
+    g-mon {nat n} {nat m} x≤y = ord-η-monotone ℕ x≤y
+    g-mon {fun f} {fun g} x≤y = ord-bot ℕ ℧
+
+p-nat : MonFun DynP (𝕃 ℕ)
+p-nat = S (K p-nat') (mTransport unfold-DynP)
+  -- or:
+  -- mTransportDomain (sym unfold-DynP) p-nat'
+
+
+EP-nat : EP ℕ DynP
+EP-nat = record {
+  emb = e-nat;
+  proj = p-nat }
+
+
+-- E-P Pair for monotone functions Dyn to L℧ Dyn
+
+e-fun : MonFun (arr' DynP (𝕃 DynP)) DynP
+e-fun = record { f = e-fun-f ; isMon = e-fun-mon }
+  where
+    e-fun-f : ⟨ arr' DynP (𝕃 DynP) ⟩ -> ⟨ DynP ⟩
+    e-fun-f f = DynP'-to-DynP (fun (next f))
+
+    e-fun-mon :
+      {f1 f2 : ⟨ arr' DynP (𝕃 DynP) ⟩} ->
+      rel (arr' DynP (𝕃 DynP)) f1 f2 ->
+      rel DynP (e-fun-f f1) (e-fun-f f2)
+    e-fun-mon {f1} {f2} f1≤f2 =
+      DynP-rel (fun (next f1)) (fun (next f2)) (λ t d1 d2 d1≤d2 → {!!})
+
+
+p-fun : MonFun DynP (𝕃 (arr' DynP (𝕃 DynP)))
+p-fun = record { f = p-fun-f ; isMon = {!!} }
+  where
+
+    p-fun-f' : ⟨ DynP' (next DynP) ⟩ -> ⟨ 𝕃 (arr' DynP (𝕃 DynP)) ⟩
+    p-fun-f' (nat n) = ℧
+    p-fun-f' (fun f) = η {!!}
+
+    p-fun-f : ⟨ DynP ⟩ -> ⟨ 𝕃 (arr' DynP (𝕃 DynP)) ⟩
+    -- p-fun-f d = p-fun-f' (transport unfold-⟨DynP⟩ d)
+    p-fun-f d = p-fun-f' (transport (λ i -> ⟨ unfold-DynP i ⟩) d)
+
+
+EP-fun : EP (arr' DynP (𝕃 DynP)) DynP
+EP-fun = record {
+  emb = e-fun;
+  proj = p-fun }
+
+
+
+
+-- Composing EP pairs
+
+module EPComp
+  {A B C : Predomain}
+  (epAB : EP A B)
+  (epBC : EP B C) where
+
+  open EP
+  open MonFun
+
+  comp-emb : ⟨ A ==> C ⟩
+  comp-emb = K (emb epBC) <*> (emb epAB) -- mComp (emb epBC) (emb epAB)
+
+  comp-proj : ⟨ C ==> 𝕃 A ⟩
+  comp-proj = (mExt' (K (proj epAB))) <*> (proj epBC) -- mComp (mExt (proj epAB)) (proj epBC)
+  --  comp-proj-f =
+  --    λ c -> bind (f (proj epBC) c) (f (proj epAB)) ==
+  --    λ c -> ext  (f (proj epAB)) (f (proj epBC) c) ==
+  --    (ext (f (proj epAB))) ∘ (f (proj epBC c)) 
+
+  EP-comp : EP A C
+  EP-comp = record {
+    emb = comp-emb;
+    proj = comp-proj }
+
+
+-- Lifting EP pairs to functions
+
+module EPArrow
+  {A A' B B' : Predomain}
+  (epAA' : EP A A')
+  (epBB' : EP B B') where
+
+    e-arrow : ⟨ (A ==> 𝕃 B) ==> (A' ==> 𝕃 B') ⟩
+    e-arrow = mFunEmb (EP.proj epAA') (EP.emb epBB')
+
+    p-arrow : ⟨ (A' ==> (𝕃 B')) ==> (𝕃 (A ==> (𝕃 B))) ⟩
+    p-arrow = mFunProj (EP.emb epAA') (EP.proj epBB')
+
+{-
+    p-lift :
+      (A' -> L℧ B') -> L℧ (A -> L℧ B)
+    p-lift f =
+      ret (λ a → bind (f (EP.emb epAA' a)) (EP.proj epBB'))
+-}
+
+
+EP-arrow : {A A' B B' : Predomain} ->
+  EP A A' ->
+  EP B B' ->
+  EP (arr' A (𝕃 B)) (arr' A' (𝕃 B'))
+EP-arrow epAA' epBB' = record {
+  emb = e-arrow;
+  proj = p-arrow  }
+  where open EPArrow epAA' epBB'
+
+
+
+-------------------------------------------
+-- *** Denotation of types and contexts ***
+
+open EPComp
+
+
+⟦_⟧ty : Ty -> Predomain
+⟦ nat ⟧ty = ℕ
+⟦ dyn ⟧ty = DynP
+⟦ A => B ⟧ty = arr' ⟦ A ⟧ty (𝕃 ⟦ B ⟧ty)
+-- ⟦ A ⟧ty -> L℧ ⟦ B ⟧ty
+
+⟦_⟧ctx : Ctx -> Predomain
+⟦ · ⟧ctx = UnitP
+⟦ Γ :: A ⟧ctx = ⟦ Γ ⟧ctx ×d ⟦ A ⟧ty -- ⟦ Γ ⟧ctx × ⟦ A ⟧ty
+
+-- Agda can infer that the context is not empty, so
+-- ⟦ Γ ⟧ctx must be a product
+-- Make A implicit
+look : {Γ : Ctx} ->
+  (env : ⟨ ⟦ Γ ⟧ctx ⟩) ->
+  (A : Ty) ->
+  (x : Γ ∋ A) ->
+  ⟨ ⟦ A ⟧ty ⟩
+look env A vz = proj₂ env
+look env A (vs {Γ} {S} {T} x) = look (proj₁ env) A x
+
+look-mon : {Γ : Ctx} ->
+  (env1 env2 : ⟨ ⟦ Γ ⟧ctx ⟩) ->
+  (A : Ty) ->
+  (z : Γ ∋ A) ->
+  rel ⟦ Γ ⟧ctx env1 env2 ->
+  rel ⟦ A ⟧ty (look env1 A z) (look env2 A z)
+look-mon env1 env2 A z env1≤env2 = {!!}
+
+mLook : {Γ : Ctx} ->
+  (A : Ty) ->
+  (x : Γ ∋ A) ->
+  ⟨ ⟦ Γ ⟧ctx ==> ⟦ A ⟧ty ⟩
+mLook A x = record {
+  f = λ env -> look env A x ;
+  isMon = λ {env1} {env2} env1≤env2 → look-mon env1 env2 A x env1≤env2 }
+
+
+
+---------------------------------------
+-- *** Denotation of type precision ***
+
+⟦_⟧lt : {A B : Ty} -> A ⊑ B -> EP ⟦ A ⟧ty ⟦ B ⟧ty
+-- ⟦_⟧lt = {!!}
+⟦ dyn ⟧lt = EP-id DynP
+⟦ A⊑A' => B⊑B' ⟧lt = EP-arrow ⟦ A⊑A' ⟧lt ⟦ B⊑B' ⟧lt
+⟦ nat ⟧lt = EP-id ℕ
+⟦ inj-nat ⟧lt = EP-nat
+⟦ inj-arrow (A-dyn => B-dyn) ⟧lt =
+  EP-comp (EP-arrow  ⟦ A-dyn ⟧lt  ⟦ B-dyn ⟧lt) EP-fun
+
+
+
+------------------------------
+-- *** Denotation of terms ***
+
+tm-sem : {A : Ty} {Γ : Ctx} -> Tm Γ A -> ⟨ ⟦ Γ ⟧ctx ==> (𝕃 ⟦ A ⟧ty) ⟩
+tm-sem (var z) = mRet' (mLook _ z)
+tm-sem (lda M) = mRet' (K (tm-sem M) ∘m Pair)
+
+{-
+record {
+  f = λ ⟦Γ⟧ -> ret
+    (record {
+      f = λ N -> MonFun.f (tm-sem M) (⟦Γ⟧ , N);
+      isMon = {!!} }) ;
+  isMon = {!!} }
+-}
+  
+tm-sem {A} {Γ} (app {S = B} M1 M2) =
+    let kont = (K (swap mExt) <*> tm-sem M2) in
+    (mExt' kont <*> tm-sem M1)
+
+
+-- mExt :      ⟨ (⟦ B ⟧ty ==> 𝕃 ⟦ A ⟧ty) ==> 𝕃 ⟦ B ⟧ty ==> 𝕃 ⟦ A ⟧ty ⟩
+-- swap mExt : ⟨ 𝕃 ⟦ B ⟧ty ==> ( ⟦ B ⟧ty ==> 𝕃 ⟦ A ⟧ty ) ==> 𝕃 ⟦ A ⟧ty ⟩
+-- K (swap mExt) : ⟨ ⟦ Γ ⟧ctx ==> 𝕃 ⟦ B ⟧ty ==> ( ⟦ B ⟧ty ==> 𝕃 ⟦ A ⟧ty ) ==> 𝕃 ⟦ A ⟧ty ⟩
+-- tm-sem M2 : ⟨ ⟦ Γ ⟧ctx ==> 𝕃 ⟦ B ⟧ty ⟩
+-- kont :      ⟨  ⟦ Γ ⟧ctx ==> ( ⟦ B ⟧ty ==> 𝕃 ⟦ A ⟧ty ) ==> 𝕃 ⟦ A ⟧ty ⟩
+
+-- mExt' kont : ⟨ ⟦ Γ ⟧ctx ==> 𝕃 ( ⟦ B ⟧ty ==> 𝕃 ⟦ A ⟧ty ) ==> 𝕃 ⟦ A ⟧ty ⟩
+-- tm-sem M1 : ⟨ ⟦ Γ ⟧ctx ==> 𝕃 ( ⟦ B ⟧ty ==> 𝕃 ⟦ A ⟧ty ) ⟩
+-- result : ⟨ ⟦ Γ ⟧ctx ==> 𝕃 ⟦ A ⟧ty ⟩
+
+{-
+ 
+Idea:
+  
+  ext f : 𝕃 ⟦ S1 ⟧ty ==> 𝕃 ⟦ A ⟧ty
+ (ext f) (tm-sem M2 ⟦Γ⟧) : 𝕃 ⟦ A ⟧ty
+
+-}
+
+
+{-
+record {
+  f = λ ⟦Γ⟧ ->
+    bind ((MonFun.f (tm-sem M1)) ⟦Γ⟧)
+         (λ f -> bind (MonFun.f (tm-sem M2) ⟦Γ⟧) (MonFun.f f)) ;
+    isMon = {!!} }
+-}
+    
+tm-sem {A} err = K ℧
+-- record { f = λ _ -> ℧ ; isMon = λ _ -> ord-bot ⟦ A ⟧ty ℧ }
+
+tm-sem (up A⊑B M) = (mMap' (K (EP.emb ⟦ A⊑B ⟧lt))) <*> (tm-sem M)
+
+{-
+record {
+  f =  λ ⟦Γ⟧ -> mapL (MonFun.f (EP.emb ⟦ A⊑B ⟧lt)) ((MonFun.f (tm-sem  M)) ⟦Γ⟧) ;
+  isMon = {!!} }
+-}
+  
+tm-sem (dn A⊑B M) = (mExt' (K (EP.proj ⟦ A⊑B ⟧lt))) <*> (tm-sem M)
+
+{-
+record { f =
+  λ ⟦Γ⟧ -> bind ((MonFun.f (tm-sem M)) ⟦Γ⟧) (MonFun.f (EP.proj ⟦ A⊑B ⟧lt)) ;
+  isMon = {!!} }
+-}
+  
+tm-sem zro = K (η zero)
+-- record { f = λ _ -> η zero ; isMon = λ _ → ord-refl ℕ (η zero) }
+
+tm-sem (suc M) = (mExt' (K (mRet' mSuc))) <*> (tm-sem M)
+{-
+record {
+  f =  λ ⟦Γ⟧ -> bind (MonFun.f (tm-sem M) ⟦Γ⟧) (λ n -> η (suc n)) ;
+  isMon = λ _ → {!!} }
+-}
+
+-- ⟦_⟧tm : {A : Ty} -> {Γ : Ctx} -> Tm Γ A -> (⟨ ⟦ Γ ⟧ctx ⟩ -> L℧ ⟨ ⟦ A ⟧ty ⟩)
+⟦_⟧tm : {A : Ty} -> {Γ : Ctx} -> Tm Γ A -> MonFun ( ⟦ Γ ⟧ctx)  (𝕃 ⟦ A ⟧ty )
+⟦ M ⟧tm = tm-sem M
+
+
+
+
+
+---------------------------------------
+-- *** Denotation of term precision ***
+--  ⟦ M ⟧ ≲ ⟦ N ⟧
+
+open WeakRel
+
+-- Homogeneous term precision relation
+lttm-hom : {A : Ty} ->
+  (Γ : Ctx) ->
+  (M : Tm (lhs (Ctx-ref Γ)) A) ->
+  (N : Tm (rhs (Ctx-ref Γ)) A) ->
+  (Ctx-ref Γ) |- M ⊑tm N # (⊑ref A) ->
+  (⟦ A ⟧ty ≾ ((MonFun.f ⟦ M ⟧tm) {!!})) ((MonFun.f ⟦ N ⟧tm) {!!})
+lttm-hom Γ M N M⊑N = {!!}
+
+
+{-
+mapL-emb : {A A' : Type} -> (epAA' : EP A A') (a : L℧ A) ->
+  mapL (EP.emb epAA') a ≡ EP.emb (EP-L epAA') a
+mapL-emb epAA' a = refl
+-}
+
+
+------------------------------------------------------------------
+-- *** Relational interpretation of type precision derivations ***
+-- c : A ⊑ B
+-- ⟦c⟧ : relation between ⟦ A ⟧ty and ⟦ B ⟧ty
+
+typrecd-sem : {A B : Ty} ->
+  (c : A ⊑ B) -> (⟨ ⟦ A ⟧ty ⟩ -> ⟨ ⟦ B ⟧ty ⟩ -> Type)
+typrecd-sem dyn = rel DynP
+typrecd-sem {Ain => Aout} {Bin => Bout} (cin => cout) =
+  λ f1 f2 -> fun-order-het
+    ⟦ Ain ⟧ty ⟦ Bin ⟧ty (𝕃 ⟦ Aout ⟧ty) (𝕃 ⟦ Bout ⟧ty)
+    (typrecd-sem cin)
+    (LiftRelation.ord ⟦ Aout ⟧ty ⟦ Bout ⟧ty (typrecd-sem cout))
+    (MonFun.f f1) (MonFun.f f2)
+typrecd-sem nat = rel ℕ
+typrecd-sem inj-nat = λ n d -> rel' n (DynP-to-DynP' d)
+  where
+    rel' : ⟨ ℕ ⟩ -> ⟨ DynP' (next DynP) ⟩ -> Type
+    rel' n (nat n') = n ≡ n'
+    rel' n (fun _) = ⊥
+typrecd-sem (inj-arrow c) = {!!}
+
+
+
+
+------------------------------
+-- *** Beta/eta properties ***
+
+
+
+-- Semantic meaning of substitution
+
+sub-lemma : (Γ : Ctx) (A B : Ty) -> (M : Tm (Γ :: A) B) -> (N : Tm Γ A) ->
+  ⟦ M [ N ] ⟧tm ≡ {!!}
+sub-lemma = {!!}
+
+{-
+
+lem1 : ∀ (Γ : Ctx) (A B : Ty) -> (M : Tm (Γ :: A) B) (N : Tm Γ A) ->
+   ⟦ app (lda M) N ⟧tm ≡ {!!}
+lem1 Γ A B M N =
+  let kont = (K (swap mExt) <*> tm-sem N) in
+  (mExt' kont <*> tm-sem (lda M))
+    ≡⟨ refl ⟩
+  let kont = (K (swap mExt) <*> tm-sem N) in
+  (mExt' kont <*> (mRet' (K (tm-sem M) ∘m Pair)))
+    ≡⟨ {! refl!} ⟩
+  mExt' (K (swap mExt) <*> tm-sem N) <*> (mRet' (K (tm-sem M) ∘m Pair))
+    ≡⟨ {!!} ⟩
+  {!!}
+    ≡⟨ {!!} ⟩
+  {!!}
+
+-}
+
+-- TODO need to stipulate that N is a value?
+beta-lt : (Γ : Ctx) (A B : Ty) -> (M : Tm (Γ :: A) B) -> (N : Tm Γ A) ->
+  rel (⟦ Γ ⟧ctx ==> 𝕃 ⟦ B ⟧ty)   ⟦ app (lda M) N ⟧tm   ⟦ M [ N ] ⟧tm
+beta-lt Γ A B (var x) N = {!!}
+beta-lt Γ A .(_ => _) (lda M) N = {!!}
+beta-lt Γ A B (app M M₁) N = {!!}
+beta-lt Γ A B err N = {!!}
+beta-lt Γ A B (up x M) N = {!!}
+beta-lt Γ A B (dn x M) N = {!!}
+beta-lt Γ A .nat zro N = {!!}
+beta-lt Γ A .nat (suc M) N = {!!}
+
+eta : (Γ : Ctx) (A B : Ty) -> (M : Tm Γ (A => B)) ->
+  rel {!!}  ⟦ M ⟧tm ⟦ {!lda!} ⟧tm
+eta = {!!}
+
+
+{-
+
+-}

formalizations/guarded-cubical/StrongBisimulation.agda

+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Later
+
+module StrongBisimulation(k : Clock) where
+
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Binary.Poset
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Transport
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Data.Nat hiding (_^_) renaming (ℕ to Nat)
+open import Cubical.Data.Bool.Base
+open import Cubical.Data.Bool.Properties hiding (_≤_)
+open import Cubical.Data.Empty hiding (rec)
+open import Cubical.Data.Sum hiding (rec)
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Unit.Properties
+
+open import Agda.Primitive
+
+private
+  variable
+    l : Level
+    A B : Set l
+    ℓ ℓ' : Level
+private
+  ▹_ : Set l → Set l
+  ▹_ A = ▹_,_ k A
+
+
+id : {ℓ : Level} -> {A : Type ℓ} -> A -> A
+id x = x
+
+_^_ : {ℓ : Level} -> {A : Type ℓ} -> (A -> A) -> Nat -> A -> A
+f ^ zero = id
+f ^ suc n = f ∘ (f ^ n)
+
+
+-- 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
+
+
+-- 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
+
+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))
+
+▸' : ▹ 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
+
+
+▸''_ : Predomain → Predomain
+▸'' X = ▸' (next X)
+
+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
+
+
+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
+
+unfold-ext : (f : A -> L℧ B) -> ext f ≡ ext' f (next (ext f))
+unfold-ext f = fix-eq (ext' f)
+
+mapL : (A -> B) -> L℧ A -> L℧ B
+mapL f la = bind la (λ a -> ret (f a))
+
+
+-- 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
+
+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)
+
+
+-- 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) ->
+  (⟨ 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-general
+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 f g h f≤g g≤h =
+  fun-order-trans (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
+    -- 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._≤_
+
+    {-
+    mon-fun-order : MonFun P1 P2 → MonFun P1 P2 → Type ℓ-zero
+    mon-fun-order mon-f1 mon-f2 =
+      fun-order P1 P2 (MonFun.f mon-f1) (MonFun.f mon-f2)
+    -}
+
+    {-
+    fun-order : MonFun P1 P2 → MonFun P1 P2 → Type ℓ-zero
+    fun-order mon-f1 mon-f2 =
+      (x y : ⟨ P1 ⟩) -> x ≤P1 y -> (mon-f1 .f) x ≤P2 (mon-f2 .f) y
+    -}
+
+_==>_ : Predomain -> Predomain -> Predomain
+A ==> B = arr' A B
+
+infixr 20 _==>_
+
+
+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)
+       
+
+
+
+
+-- 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)
+
+module LiftRelation
+  (A B : Predomain)
+  (ordAB : ⟨ A ⟩ -> ⟨ B ⟩ -> Type)
+  where
+
+  module A = PosetStr (A .snd)
+  module B = PosetStr (B .snd)
+
+  open A renaming (_≤_ to _≤A_)
+  open B renaming (_≤_ to _≤B_)
+
+  ord' : ▹ ( L℧ ⟨ A ⟩ → L℧ ⟨ B ⟩ → Type) ->
+             L℧ ⟨ A ⟩ → L℧ ⟨ B ⟩ → Type
+  ord' rec (η a) (η b) = ordAB a b
+  ord' rec ℧ lb = Unit
+  ord' rec (θ la~) (θ lb~) = ▸ (λ t → rec t (la~ t) (lb~ t))
+  ord' _ _ _ = ⊥
+
+  ord : L℧ ⟨ A ⟩ -> L℧ ⟨ B ⟩ -> Type
+  ord = fix ord'
+
+  unfold-ord : ord ≡ ord' (next ord)
+  unfold-ord = fix-eq ord'
+
+  ord-η-monotone : {a : ⟨ A ⟩} -> {b : ⟨ B ⟩} -> ordAB a b -> ord (η a) (η b)
+  ord-η-monotone {a} {b} a≤b = transport (sym (λ i → unfold-ord i (η a) (η b))) a≤b
+
+  ord-bot : (lb : L℧ ⟨ B ⟩) -> ord ℧ lb
+  ord-bot lb = transport (sym (λ i → unfold-ord i ℧ lb)) tt
+
+
+  -- ord-trans-IH
+
+
+module LiftRelTransitive
+  (A B C : Predomain)
+  (ordAB : ⟨ A ⟩ -> ⟨ B ⟩ -> Type)
+  (ordBC : ⟨ B ⟩ -> ⟨ C ⟩ -> Type)
+  where
+
+  module A = PosetStr (A .snd)
+  module B = PosetStr (B .snd)
+  module C = PosetStr (C .snd)
+
+  open A renaming (_≤_ to _≤A_)
+  open B renaming (_≤_ to _≤B_)
+  open C renaming (_≤_ to _≤C_)
+
+  open LiftRelation A B ordAB renaming (ord to ordLALB; unfold-ord to unfold-ordLALB)
+  open LiftRelation B C ordBC renaming (ord to ordLBLC; unfold-ord to unfold-ordLBLC)
+
+  ordAC : ⟨ A ⟩ -> ⟨ C ⟩ -> Type
+  ordAC a c = Σ ⟨ B ⟩ λ b → ordAB a b × ordBC b c
+
+  open LiftRelation A C ordAC renaming (ord to ordLALC; unfold-ord to unfold-ordLALC)
+
+
+  {-
+  ord-trans-ind :
+        ▹ ((a b c : L℧ ⟨ p ⟩) ->
+           ord' (next ord) a b ->
+           ord' (next ord) b c ->
+           ord' (next ord) a c) ->
+        (a b c : L℧ ⟨ p ⟩) ->
+         ord' (next ord) a b ->
+         ord' (next ord) b c ->
+         ord' (next ord) a c
+  -}
+
+
+  ord-trans :
+    (la : L℧ ⟨ A ⟩) (lb : L℧ ⟨ B ⟩) (lc : L℧ ⟨ C ⟩) ->
+    ordLALB la lb -> ordLBLC lb lc -> ordLALC la lc
+  ord-trans la lb lc la≤lb lb≤lc = {!!}
+ 
+
+  {- ord-trans = fix (transport (sym (λ i ->
+         (▹ ((a b c : L℧ ⟨ p ⟩) →
+            unfold-ord i a b → unfold-ord i b c → unfold-ord i a c) →
+             (a b c : L℧ ⟨ p ⟩) →
+            unfold-ord i a b → unfold-ord i b c → unfold-ord i a c))) ord-trans-ind)
+  -}
+  
+
+
+-- Predomain to lift predomain
+module 𝕃 (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'
+
+  unfold-ord : ord ≡ ord' (next ord)
+  unfold-ord = fix-eq ord'
+
+  ord-η-monotone : {x y : ⟨ p ⟩} -> x ≤ y -> ord (η x) (η y)
+  ord-η-monotone {x} {y} x≤y = transport (sym λ i → unfold-ord i (η x) (η y)) x≤y
+
+  ord-bot : (lx : L℧ ⟨ p ⟩) -> ord ℧ lx
+  ord-bot lx = transport (sym λ i → unfold-ord i ℧ lx) tt
+
+  -- lift-ord : (A -> A -> Type) -> (L℧ A -> L℧ A -> Type)
+
+  ord-refl-ind : ▹ ((a : L℧ ⟨ p ⟩) -> ord a a) ->
+                    (a : L℧ ⟨ p ⟩) -> ord a a
+
+  ord-refl-ind IH (η x) =
+    transport (sym (λ i -> fix-eq ord' i (η x) (η x))) (IsPoset.is-refl X.isPoset x)
+  ord-refl-ind IH ℧ =
+    transport (sym (λ i -> fix-eq ord' i ℧ ℧)) tt
+  ord-refl-ind IH (θ x) =
+    transport (sym (λ i -> fix-eq ord' i (θ x) (θ x))) λ t → IH t (x t)
+
+  ord-refl : (a : L℧ ⟨ p ⟩) -> ord a a
+  ord-refl = fix ord-refl-ind
+
+ 
+
+  𝕃 : Predomain
+  𝕃 =
+    (L℧ ⟨ p ⟩) ,
+    (posetstr ord (isposet {!!} {!!} ord-refl ord-trans {!!}))
+    where
+
+      ord-trans-ind :
+        ▹ ((a b c : L℧ ⟨ p ⟩) ->
+           ord' (next ord) a b ->
+           ord' (next ord) b c ->
+           ord' (next ord) a c) ->
+        (a b c : L℧ ⟨ p ⟩) ->
+         ord' (next ord) a b ->
+         ord' (next ord) b c ->
+         ord' (next ord) a c
+      ord-trans-ind IH (η x) (η y) (η z) ord-ab ord-bc =
+        IsPoset.is-trans X.isPoset x y z ord-ab ord-bc
+        -- x ≡⟨ ord-ab ⟩ y ≡⟨ ord-bc ⟩ z ∎
+      ord-trans-ind IH (η x) (η y) ℧ ord-ab ord-bc = ord-bc
+      ord-trans-ind IH (η x) (θ y) ℧ contra ord-bc = contra
+      ord-trans-ind IH (η x) (η y) (θ z) ord-ab contra = contra
+      ord-trans-ind IH (η x) ℧ (θ y) ord-ab ord-bc = ord-ab
+      ord-trans-ind IH (η x) (θ y) (θ z) ord-ab ord-bc = ord-ab
+      ord-trans-ind IH ℧ b c ord-ab ord-bc = tt
+      ord-trans-ind IH (θ lx~) (θ ly~) (θ lz~) ord-ab ord-bc =
+        λ 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)))
+
+      ord-trans : (a b c : L℧ ⟨ p ⟩) -> ord a b -> ord b c -> ord a c
+      ord-trans = fix (transport (sym (λ i ->
+         (▹ ((a b c : L℧ ⟨ p ⟩) →
+            unfold-ord i a b → unfold-ord i b c → unfold-ord i a c) →
+             (a b c : L℧ ⟨ p ⟩) →
+            unfold-ord i a b → unfold-ord i b c → unfold-ord i a c))) ord-trans-ind)
+
+
+-- 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 𝕃
+
+
+
+-- 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
+    
+
+    {-
+    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
+      {!!}
+      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 }
+
+
+-- Weak bisimulation relaion
+-- Define compositionally
+
+δ : {X : Type} -> L℧ X -> L℧ X
+δ = θ ∘ next
+  where open L℧
+
+module WeakRel (d : Predomain) where
+
+  module D = PosetStr (d .snd)
+  _≤_ = D._≤_
+
+  -- make this a module so we can avoid having to make the IH
+  -- a parameter of the comparison function
+  module Inductive (IH : ▹ (L℧ ⟨ d ⟩ -> L℧ ⟨ d ⟩ -> Type)) where
+
+
+    _≾'_ : L℧ (U d) -> L℧ (U d) -> Type
+    ℧ ≾' _ = Unit
+      
+    η x ≾' η y = x ≤ y
+    
+    θ lx ≾' θ ly = ▸ (λ t -> IH t (lx t) (ly t))
+    -- or equivalently: θ lx ≾' θ ly = ▸ ((IH ⊛ lx) ⊛ ly)
+      
+    η x ≾' θ t = Σ Nat λ n -> Σ (U d) (λ y -> (θ t ≡ (δ ^ n) (η y)) × (x ≤ y))
+
+    -- need to account for error (θ s ≡ delay of η x or delay of ℧, in which case we're done)
+    θ s ≾' η y = Σ Nat λ n ->
+       (θ s ≡ (δ ^ n) L℧.℧) ⊎
+       (Σ (U d) (λ x -> (θ s ≡ (δ ^ n) (η x)) × (x ≤ y)))
+      
+    _ ≾' ℧ = ⊥
+   
+  _≾_ : L℧ (U d) -> L℧ (U d) -> Type
+  _≾_ = fix _≾'_
+    where open Inductive
+
+
+
+
+
+
+{-
+-- 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
+
+-}