Work on intensional and extensional theories

formalizations/guarded-cubical/GradualSTLC.agda

@@ -36,6 +36,33 @@ data _⊑_ : Ty -> Ty -> Set where
 ⊑ref dyn = dyn
 ⊑ref (A1 => A2) = (⊑ref A1) => (⊑ref A2)
 
+⊑comp : {A B C : Ty} ->
+  A ⊑ B -> B ⊑ C -> A ⊑ C
+⊑comp dyn dyn = dyn
+⊑comp {Ai => Ao} {Bi => Bo} {Ci => Co} (cin => cout) (din => dout) =
+  (⊑comp cin din) => (⊑comp cout dout)
+⊑comp {Ai => Ao} {Bi => Bo} (cin => cout) (inj-arrow (cin' => cout')) =
+  inj-arrow ((⊑comp cin cin') => (⊑comp cout cout'))
+⊑comp nat nat = nat
+⊑comp nat inj-nat = inj-nat
+⊑comp inj-nat dyn = inj-nat
+⊑comp (inj-arrow c) dyn = inj-arrow c
+
+{-
+ltdyn-transitive {A => B} {A' => B'} {A'' => B''} {n} {m} {p}
+  eq (_=>_ {eq = eq1} dAA' dBB') (_=>_ {eq = eq2} dA'A'' dB'B'') =
+  _=>_ {n = {!?!}} {m = {!!}} {p = {!!}} {eq = {!!}}
+    (ltdyn-transitive {!!} dAA' dA'A'')
+    (ltdyn-transitive {!!} dBB' dB'B'')
+ltdyn-transitive eq (dAA' => dBB') (inj-arrow dBC) = {!!}
+ltdyn-transitive _ nat nat = nat
+ltdyn-transitive _ nat inj-nat = inj-nat
+ltdyn-transitive _ inj-nat dyn = inj-nat
+ltdyn-transitive eq (inj-arrow dA-dyn-dyn) dyn =
+  inj-arrow (ltdyn-transitive _ dA-dyn-dyn (dyn => dyn))
+
+-}
+
 {-
 data ltdyn : ℕ -> Ty -> Ty -> Set where
   dyn : {n : ℕ} -> ltdyn n dyn dyn
@@ -258,3 +285,14 @@ data Value : ∀ {Γ} {A} -> Tm Γ A -> Set where
     {V : Tm Γ (Bin => Bout)} ->
     Value V ->
     Value (dn (cin => cout) V)
+
+-- Upcasts are values, downcasts are evaluation contexts
+
+{-
+data Value : Type where
+  Zero : {Γ} -> Value
+  Suc : Value -> Value
+-}
+
+
+

formalizations/guarded-cubical/Later.agda

@@ -79,3 +79,70 @@ postulate
 postulate
   force-beta : ∀ {A : Set l} (x : A) → force (λ k _ → x) ≣ λ k → x
 
+
+
+
+
+-- ########################################################## --
+--
+-- Added by Eric (not part of original file from Niccolò Veltri
+-- and Andrea Vezzosi)
+
+
+-- Tick irrelevance axiom. This is needed in the development.
+-- There is likely a better way to do this, see
+-- https://arxiv.org/pdf/2102.01969.pdf (in particular Section 3.2).
+postulate
+  tick-irrelevance : {A : Type} -> (M : ▹ k , A) (t t' : Tick k) ->
+    M t ≡ M t'
+
+  tr' : {A : Type} -> (M : ▹ k , A) ->
+    ▸ λ t -> ▸ λ t' -> M t ≡ M t'
+
+{-
+tr→tr' : {M : ▹ k , A} -> tick-irrelevance M -> tr' M
+-}
+
+-- The tick constant.
+postulate
+  _◇ : (k : Clock) -> Tick k
+
+-- From Section V.C of Bahr et. al
+-- (See https://bahr.io/pubs/files/bahr17lics-paper.pdf).
+postulate
+  tick-irrelevance-◇-refl : {A : Type} -> (M : ▹ k , A) ->
+    (tick-irrelevance M (k ◇) (k ◇)) ≡ Cubical.Foundations.Everything.refl
+      -- Should this use _≣_.refl instead?
+
+
+-- This relies on tick irrelevance.
+next-Mt≡M : {A : Type} -> (M : ▹ k , A) ->
+  ▸ λ t -> (next (M t) ≡ M)
+next-Mt≡M M t = later-ext (λ t' → tick-irrelevance M t t')
+
+
+next-Mt≡M' : {A : Type} -> (M : ▹ k , A) -> (t : Tick k) ->
+  next (M t) ≡ M
+next-Mt≡M' M t = next-Mt≡M M t
+
+
+
+
+
+-- Clock-related postulates.
+postulate
+  clock-iso : {A : Type} -> (∀ (k : Clock) -> A) ≡ A
+
+postulate
+  k0 : Clock
+
+postulate
+  clock-irrel : {ℓ : Level} -> {A : Type ℓ} ->
+    (M : ∀ (k : Clock) -> A) ->
+    (k k' : Clock) ->
+    M k ≡ M k'
+
+
+
+
+

formalizations/guarded-cubical/MonFuns.agda

@@ -39,16 +39,22 @@ private
 
 open 𝕃
 
-abstract
+-- abstract
 
-  -- Composing monotone functions
-  mComp : {A B C : Predomain} ->
+-- Composing monotone functions
+mCompU : {A B C : Predomain} -> MonFun B C -> MonFun A B -> MonFun A C
+mCompU f1 f2 = record {
+    f = λ a -> f1 .f (f2 .f a) ;
+    isMon = λ x≤y -> f1 .isMon (f2 .isMon x≤y) }
+  where open MonFun
+
+mComp : {A B C : Predomain} ->
     -- MonFun (arr' B C) (arr' (arr' A B) (arr' A C))
     ⟨ (B ==> C) ==> (A ==> B) ==> (A ==> C) ⟩
-  mComp = record {
+mComp = record {
     f = λ fBC →
       record {
-        f = λ fAB → mComp' fBC fAB ;
+        f = λ fAB → mCompU fBC fAB ;
         isMon = λ {f1} {f2} f1≤f2 ->
           λ a1 a2 a1≤a2 → MonFun.isMon fBC (f1≤f2 a1 a2 a1≤a2) } ;
     isMon = λ {f1} {f2} f1≤f2 →
@@ -56,73 +62,105 @@ abstract
         λ a1 a2 a1≤a2 ->
           f1≤f2 (MonFun.f fAB1 a1) (MonFun.f fAB2 a2)
             (fAB1≤fAB2 a1 a2 a1≤a2) }
-    where
-      mComp' : {A B C : Predomain} -> MonFun B C -> MonFun A B -> MonFun A C
-      mComp' f1 f2 = record {
-        f = λ a -> f1 .f (f2 .f a) ;
-        isMon = λ x≤y -> f1 .isMon (f2 .isMon x≤y) }
-        where open MonFun
+     
 
 
   -- 𝕃's return as a monotone function
-  mRet : {A : Predomain} -> ⟨ A ==> 𝕃 A ⟩
-  mRet {A} = record { f = ret ; isMon = ord-η-monotone A }
+mRet : {A : Predomain} -> ⟨ A ==> 𝕃 A ⟩
+mRet {A} = record { f = ret ; isMon = ord-η-monotone A }
 
 
-  -- Extending a monotone function to 𝕃
-  mExt : {A B : Predomain} -> ⟨ (A ==> 𝕃 B) ==> (𝕃 A ==> 𝕃 B) ⟩
-  mExt = record {
-    f = mExt' ;
-    isMon = λ {f1} {f2} f1≤f2  -> ext-monotone (MonFun.f f1) (MonFun.f f2) f1≤f2 }
-    where
-      mExt' : {A B : Predomain} -> MonFun A (𝕃 B) -> MonFun (𝕃 A) (𝕃 B)
-      mExt' f = record {
-        f = λ la -> bind la (MonFun.f f) ;
-        isMon = monotone-bind-mon f }
+  -- Delay as a monotone function
+Δ : {A : Predomain} -> ⟨ 𝕃 A ==> 𝕃 A ⟩
+Δ {A} = record { f = δ ; isMon = λ x≤y → ord-δ-monotone A x≤y }
+
+  -- Lifting a monotone function functorially
+_~->_ : {A B C D : Predomain} ->
+    ⟨ A ==> B ⟩ -> ⟨ C ==> D ⟩ -> ⟨ (B ==> C) ==> (A ==> D) ⟩
+pre ~-> post = {!!}
+  -- λ f -> mCompU post (mCompU f pre)
 
 
+  -- Extending a monotone function to 𝕃
+mExtU : {A B : Predomain} -> MonFun A (𝕃 B) -> MonFun (𝕃 A) (𝕃 B)
+mExtU f = record {
+    f = λ la -> bind la (MonFun.f f) ;
+    isMon = monotone-bind-mon f }
+
+mExt : {A B : Predomain} -> ⟨ (A ==> 𝕃 B) ==> (𝕃 A ==> 𝕃 B) ⟩
+mExt = record {
+    f = mExtU ;
+    isMon = λ {f1} {f2} f1≤f2 -> ext-monotone (MonFun.f f1) (MonFun.f f2) f1≤f2 }
+     
+  -- mBind : ⟨ 𝕃 A ==> (A ==> 𝕃 B) ==> 𝕃 B ⟩
+
   -- Monotone successor function
-  mSuc : ⟨ ℕ ==> ℕ ⟩
-  mSuc = record {
+mSuc : ⟨ ℕ ==> ℕ ⟩
+mSuc = record {
     f = suc ;
     isMon = λ {n1} {n2} n1≤n2 -> λ i -> suc (n1≤n2 i) }
 
 
   -- Combinators
 
-  S : {Γ A B : Predomain} ->
-    ⟨ Γ ==> A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
-  S f g =
+U : {A B : Predomain} -> ⟨ A ==> B ⟩ -> ⟨ A ⟩ -> ⟨ B ⟩
+U f = MonFun.f f
+
+_<$$>_ : {A B : Predomain} -> ⟨ A ==> B ⟩ -> ⟨ A ⟩ -> ⟨ B ⟩
+_<$$>_ = U
+
+S : (Γ : Predomain) -> {A B : Predomain} ->
+    ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+S Γ f g =
     record {
-      f = λ γ -> MonFun.f (MonFun.f f γ) (MonFun.f g γ) ;
-      isMon = λ {γ1} {γ2} γ1≤γ2 →
+      f = λ γ -> MonFun.f f (γ , (U g γ)) ;
+      isMon = λ {γ1} {γ2} γ1≤γ2 ->
+        MonFun.isMon f (γ1≤γ2 , (MonFun.isMon g γ1≤γ2)) }
+
+  {- λ {γ1} {γ2} γ1≤γ2 →
         let fγ1≤fγ2 = MonFun.isMon f γ1≤γ2 in
-          fγ1≤fγ2 (MonFun.f g γ1) (MonFun.f g γ2) (MonFun.isMon g γ1≤γ2) }
+          fγ1≤fγ2 (MonFun.f g γ1) (MonFun.f g γ2) (MonFun.isMon g γ1≤γ2) } -}
 
 
-  _<*>_ : {Γ A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
-  f <*> g = S f g
+_!_<*>_ : {A B : Predomain} ->
+    (Γ : Predomain) -> ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+Γ ! f <*> g = S Γ f g
 
-  infixl 20 _<*>_
+infixl 20 _<*>_
 
 
-  K : {Γ : Predomain} -> {A : Predomain} -> ⟨ A ⟩ -> ⟨ Γ ==> A ⟩
-  K {_} {A} = λ a → record {
+K : (Γ : Predomain) -> {A : Predomain} -> ⟨ A ⟩ -> ⟨ Γ ==> A ⟩
+K _ {A} = λ a → record {
     f = λ γ → a ;
     isMon = λ {a1} {a2} a1≤a2 → reflexive A a }
 
-  Id : {A : Predomain} -> ⟨ A ==> A ⟩
-  Id = record { f = id ; isMon = λ x≤y → x≤y }
 
-  Curry : {Γ A B : Predomain} -> ⟨ (Γ ×d A) ==> B ⟩ -> ⟨ Γ ==> A ==> B ⟩
-  Curry f = record { f = λ γ →
-    record { f = λ a → MonFun.f f (γ , a) ; isMon = {!!} } ; isMon = {!!} }
+Id : {A : Predomain} -> ⟨ A ==> A ⟩
+Id = record { f = id ; isMon = λ x≤y → x≤y }
+
+
+Curry : {Γ A B : Predomain} -> ⟨ (Γ ×d A) ==> B ⟩ -> ⟨ Γ ==> A ==> B ⟩
+Curry f = record {
+    f = λ γ →
+      record {
+        f = λ a → MonFun.f f (γ , a) ;
+        isMon = {!!} } ;
+    isMon = {!!} }
+
+Uncurry : {Γ A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ (Γ ×d A) ==> B ⟩
+Uncurry f = record {
+    f = λ (γ , a) → MonFun.f (MonFun.f f γ) a ;
+    isMon = λ {(γ1 , a1)} {(γ2 , a2)} (γ1≤γ2 , a1≤a2) ->
+      let fγ1≤fγ2 = MonFun.isMon f γ1≤γ2 in
+        fγ1≤fγ2 a1 a2 a1≤a2 }
+
+
+App : {A B : Predomain} -> ⟨ ((A ==> B) ×d A) ==> B ⟩
+App = Uncurry Id
 
-  Uncrry : {Γ A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ (Γ ×d A) ==> B ⟩
-  Uncrry = {!!}
 
-  swap : {Γ A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ A ==> Γ ==> B ⟩
-  swap f = record {
+Swap : (Γ : Predomain) -> {A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ A ==> Γ ==> B ⟩
+Swap Γ f = record {
     f = λ a →
       record {
         f = λ γ → MonFun.f (MonFun.f f γ) a ;
@@ -135,31 +173,88 @@ abstract
 
   -- Convenience versions of comp, ext, and ret using combinators
 
-  mComp' : {Γ A B C : Predomain} ->
-    ⟨ (Γ ==> B ==> C) ⟩ -> ⟨ (Γ ==> A ==> B) ⟩ -> ⟨ (Γ ==> A ==> C) ⟩
-  mComp' f g = (K mComp) <*> f <*> g
+mComp' : (Γ : Predomain) -> {A B C : Predomain} ->
+    ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+mComp' Γ f g = {!!}
+    --_ ! _ ! K Γ mComp <*> f <*> g
+    -- (K Γ mComp) <*> f <*> g
+
+
+_∘m_ : {Γ A B C : Predomain} ->
+   ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+_∘m_ {Γ} = mComp' Γ
+
+_$_∘m_ :  (Γ : Predomain) -> {A B C : Predomain} ->
+    ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+Γ $ f ∘m g = mComp' Γ f g
+infixl 20 _∘m_
+
 
-  _∘m_ :  {Γ A B C : Predomain} ->
-    ⟨ (Γ ==> B ==> C) ⟩ -> ⟨ (Γ ==> A ==> B) ⟩ -> ⟨ (Γ ==> A ==> C) ⟩
-  f ∘m g = mComp' f g
-  infixl 20 _∘m_
+-- Apply a monotone function to the first or second argument of a pair
 
-  mExt' : {Γ A B : Predomain} ->
-    ⟨ (Γ ==> A ==> 𝕃 B) ⟩ -> ⟨ (Γ ==> 𝕃 A ==> 𝕃 B) ⟩
-  mExt' f = K mExt <*> f
+With1st : {Γ A B : Predomain} ->
+    ⟨ Γ ==> B ⟩ -> ⟨ Γ ×d A ==> B ⟩
+-- ArgIntro1 {_} {A} f = Uncurry (Swap A (K A f))
+With1st {_} {A} f = mCompU f π1
 
-  mRet' : {Γ A : Predomain} -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> 𝕃 A ⟩
-  mRet' a = K mRet <*> a
+With2nd : {Γ A B : Predomain} ->
+    ⟨ A ==> B ⟩ -> ⟨ Γ ×d A ==> B ⟩
+With2nd f = mCompU f π2
+-- ArgIntro2 {Γ} f = Uncurry (K Γ f)
 
+{-
+Cong2nd : {Γ A A' B : Predomain} ->
+    ⟨ Γ ×d A ==> B ⟩ -> ⟨ A' ==> A ⟩ -> ⟨ Γ ×d A' ==> B ⟩
+Cong2nd = {!!}
+-}
 
-  -- Mapping a monotone function
-  mMap : {A B : Predomain} -> ⟨ (A ==> B) ==> (𝕃 A ==> 𝕃 B) ⟩
-  mMap = {!!} -- mExt' (mComp' (Curry {!!}) {!!}) -- mExt (mComp mRet f)
 
 
-  mMap' : {Γ A B : Predomain} ->
-    ⟨ (Γ ==> A ==> B) ⟩ -> ⟨ (Γ ==> 𝕃 A ==> 𝕃 B) ⟩
-  mMap' = {!!}
+IntroArg : {Γ B B' : Predomain} ->
+    ⟨ Γ ==> B ⟩ -> ⟨ B ==> B' ⟩ -> ⟨ Γ ==> B' ⟩
+IntroArg {Γ} {B} {B'} fΓB fBB' = S Γ (With2nd fBB') fΓB
+-- S : ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+
+
+TransformDomain : {Γ A A' B : Predomain} ->
+    ⟨ Γ ×d A ==> B ⟩ ->
+    ⟨ ( A ==> B ) ==> ( A' ==> B ) ⟩ ->
+    ⟨ Γ ×d A' ==> B ⟩
+TransformDomain f1 f2 = Uncurry (IntroArg (Curry f1) f2)
+
+
+mExt' : (Γ : Predomain) -> {A B : Predomain} ->
+    ⟨ (Γ ×d A ==> 𝕃 B) ⟩ -> ⟨ (Γ ×d 𝕃 A ==> 𝕃 B) ⟩
+mExt' Γ f = TransformDomain f mExt
+
+mRet' : (Γ : Predomain) -> { A : Predomain} -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> 𝕃 A ⟩
+mRet' Γ a = {!!} -- _ ! K _ mRet <*> a
+
+Bind : (Γ : Predomain) -> {A B : Predomain} ->
+    ⟨ Γ ==> 𝕃 A ⟩ -> ⟨ Γ ×d A ==> 𝕃 B ⟩ -> ⟨ Γ ==> 𝕃 B ⟩
+Bind Γ la f = S Γ (mExt' Γ f) la
+
+Comp : (Γ : Predomain) -> {A B C : Predomain} ->
+    ⟨ Γ ×d B ==> C ⟩ -> ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ×d A ==> C ⟩
+Comp Γ f g = {!!}
+
+
+
+
+
+-- Mapping a monotone function
+mMap : {A B : Predomain} -> ⟨ (A ==> B) ==> (𝕃 A ==> 𝕃 B) ⟩
+mMap {A} {B} = Curry (mExt' (A ==> B) ((With2nd mRet) ∘m App))
+-- Curry (mExt' {!!} {!!}) -- mExt' (mComp' (Curry {!!}) {!!}) -- mExt (mComp mRet f)
+
+
+mMap' : {Γ A B : Predomain} ->
+    ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d 𝕃 A ==> 𝕃 B) ⟩
+mMap' f = Uncurry {!!}
+
+Map : {Γ A B : Predomain} ->
+    ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ==> 𝕃 A) ⟩ -> ⟨ (Γ ==> 𝕃 B) ⟩
+Map {Γ} f la = S Γ (mMap' f) la -- Γ ! mMap' f <*> la
 
 
   {-
@@ -190,18 +285,23 @@ abstract
   -}
 
   -- Embedding of function spaces is monotone
-  mFunEmb : {A A' B B' : Predomain} ->
+mFunEmb : (A A' B B' : Predomain) ->
     ⟨ A' ==> 𝕃 A ⟩ ->
     ⟨ B ==> B' ⟩ ->
     ⟨ (A ==> 𝕃 B) ==> (A' ==> 𝕃 B') ⟩
-  mFunEmb fA'LA fBB' = (mExt' (mMap' (K fBB') ∘m Id)) ∘m (K fA'LA)
+mFunEmb A A' B B' fA'LA fBB' =
+    Curry (Bind ((A ==> 𝕃 B) ×d A')
+      (mCompU fA'LA π2)
+      (Map (mCompU fBB' π2) ({!!})))
+  --  _ $ (mExt' _ (_ $ (mMap' (K _ fBB')) ∘m Id)) ∘m (K _ fA'LA)
   -- mComp' (mExt' (mComp' (mMap' (K fBB')) Id)) (K fA'LA)
 
-  mFunProj : {A A' B B' : Predomain} ->
+mFunProj : (A A' B B' : Predomain) ->
    ⟨ A ==> A' ⟩ ->
    ⟨ B' ==> 𝕃 B ⟩ ->
    ⟨ (A' ==> 𝕃 B') ==> 𝕃 (A ==> 𝕃 B) ⟩
-  mFunProj fAA' fB'LB = mRet' (mExt' (K fB'LB) ∘m Id ∘m (K fAA'))
+mFunProj A A' B B' fAA' fB'LB = {!!}
+  -- mRet' (mExt' (K fB'LB) ∘m Id ∘m (K fAA'))
 
   -- 
 
@@ -219,3 +319,42 @@ abstract
 
   -- mComp (mExt (mComp (mMap fBB') f1)) fA'LA ≤ mComp (mExt (mComp (mMap fBB') f2)) fA'LA
   -- ((ext ((mapL fBB') ∘ f1)) ∘ fA'LA) (a'1) ≤ ((ext ((mapL fBB') ∘ f2)) ∘ fA'LA) (a'2)
+
+
+ -- Properties
+bind-unit-l : {Γ A B : Predomain} ->
+    (f : ⟨ Γ ×d A ==> 𝕃 B ⟩) ->
+    (a : ⟨ Γ ==> A ⟩) ->
+    rel (Γ ==> 𝕃 B)
+      (Bind Γ (mRet' Γ a) f)
+      (Γ ! f <*> a)
+bind-unit-l = {!!}
+
+bind-unit-r : {Γ A B : Predomain} ->
+    (la : ⟨ Γ ==> 𝕃 A ⟩) ->
+    rel (Γ ==> 𝕃 A)
+     la
+     (Bind Γ la (mRet' _ π2))
+bind-unit-r la = {!!}
+
+
+bind-Ret' : {Γ A : Predomain} ->
+    (la : ⟨ Γ ==> 𝕃 A ⟩) ->
+    (a : ⟨ Γ ×d A ==> A ⟩) ->
+    rel (Γ ==> 𝕃 A)
+      la
+      (Bind Γ la ((mRet' _ a)))
+bind-Ret' = {!!}
+      
+
+bind-K : {Γ A B : Predomain} ->
+    (la : ⟨ Γ ==> 𝕃 A ⟩) ->
+    (lb : ⟨ 𝕃 B ⟩) ->
+     rel (Γ ==> 𝕃 B)
+       (K Γ lb)
+       (Bind Γ la ((K (Γ ×d A) lb)))
+bind-K = {!!}
+
+ {- Goal: rel (⟦ Γ ⟧ctx ==> 𝕃 ⟦ B ⟧ty) ⟦ err [ N ] ⟧tm
+      (Bind ⟦ Γ ⟧ctx ⟦ N ⟧tm (Curry ⟦ err ⟧tm))
+ -}

formalizations/guarded-cubical/Results.agda

@@ -5,13 +5,20 @@ open import Later
 module Results (k : Clock) where
 
 open import Cubical.Foundations.Prelude
-open import Cubical.Data.Nat renaming (ℕ to Nat) hiding (_·_)
+open import Cubical.Data.Nat renaming (ℕ to Nat) hiding (_·_ ; _^_)
+open import Cubical.Data.Nat.Order
 open import Cubical.Foundations.Structure
+open import Cubical.Data.Empty.Base renaming (rec to exFalso)
+open import Cubical.Data.Sum
+open import Cubical.Data.Sigma
+open import Cubical.Relation.Nullary
+
 
 open import StrongBisimulation k
 open import Semantics k
 open import SyntacticTermPrecision k
 open import GradualSTLC
+open import MonFuns k
 
 private
   variable
@@ -22,6 +29,223 @@ private
   ▹_ A = ▹_,_ k A
 
 
+
+
+-- Results about the intensional theory
+
+
+module 2Cell
+  (A A' B B' : Predomain)
+  (A▹A' : EP A A')
+  (B▹B' : EP B B')
+ where
+
+  open 𝕃
+  open EP
+
+  _⊑A'_ : ⟨ A' ⟩ -> ⟨ A' ⟩ -> Type
+  _⊑A'_ = rel A'
+
+  _⊑B'_ : ⟨ 𝕃 B' ⟩ -> ⟨ 𝕃 B' ⟩ -> Type
+  _⊑B'_ = rel (𝕃 B')
+
+  _⊑c_ : ⟨ A ⟩ -> ⟨ A' ⟩ -> Type
+  a ⊑c a' = (U (emb A▹A') a) ⊑A' a'
+
+  _⊑d_ : ⟨ 𝕃 B ⟩ -> ⟨ 𝕃 B' ⟩ -> Type
+  lb ⊑d lb' = (mapL (U (emb B▹B')) lb) ⊑B' lb'
+
+  _⊑f_ : ⟨ A ==> 𝕃 B ⟩ -> ⟨ A' ==> 𝕃 B' ⟩ -> Type
+  f ⊑f f' = fun-order-het A A' (𝕃 B) (𝕃 B') _⊑c_ _⊑d_ (MonFun.f f) (MonFun.f f')
+  
+
+module 2CellVertical
+  (A A' A'' B B' B'' : Predomain)
+  (A▹A' : EP A A')
+  (A'▹A'' : EP A' A'')
+  (B▹B' : EP B B')
+  (B'▹B'' : EP B' B'')
+  where
+
+
+
+
+-- Results about the extensional theory
+
+tick-extensionality : (X : Set) -> (lx~ : ▹ (L℧ X)) -> (ly : L℧ X) ->
+  ▸ (λ t -> lx~ t ≡ ly) ->
+  lx~ ≡ next ly
+tick-extensionality X lx~ ly H = λ i t → H t i
+
+
+tick-extensionality' : (X : Set) -> (lx~ : ▹ (L℧ X)) -> (ly : L℧ X) ->
+  ((t : Tick k) -> lx~ t ≡ ly) -> -- is there an implicit ▸ here?
+  lx~ ≡ next ly
+tick-extensionality' X lx~ ly H = λ i t₁ → H t₁ i
+
+
+
+
+
+
+η≢δ : (d : Predomain) -> (x : ⟨ d ⟩) -> (n : Nat) ->
+  ¬ ((η x) ≡ (δ ^ n) ℧)
+η≢δ d x zero contra = {!!}
+η≢δ d x (suc n) = {!!}
+
+
+open 𝕃 ℕ -- defines the lock-step relation
+
+
+-- Bisimilarity is non-trivial at Nat type
+≈-non-trivial : {!!}
+≈-non-trivial = {!!}
+
+-- Bisimilarity is not transitive at Nat type
+
+
+
+-- Adequacy of lock-step relation
+module AdequacyLockstep
+  -- (lx ly : L℧ Nat)
+  -- (lx≾ly : lx ≾ ly)
+  where
+
+  _≾'_ : L℧ Nat → L℧ Nat → Type
+  _≾'_ = ord' (next _≾_)
+
+  {-
+  lx≾'ly : lx ≾' ly
+  lx≾'ly = transport (λ i → unfold-ord i lx ly) lx≾ly
+  -}
+
+  eq-later-eq-now : (X : Set) -> (lx~ : ▹ (L℧ X)) -> (ly : L℧ X) ->
+    ▸ (λ t -> lx~ t ≡ ly) ->
+    θ lx~ ≡ θ (next ly)
+  eq-later-eq-now = {!!}
+
+
+  sigma-later : (X : Set) (A : X -> Tick k -> Type) ->
+    ▸ (λ t -> Σ X λ x -> A x t) ->
+    Σ (▹ X) λ x~ -> ▸ (λ t -> A (x~ t) t)
+  sigma-later X A H = (λ t → fst (H t)) , (λ t → snd (H t))
+
+  ≾->≾' : (lx ly : L℧ Nat) ->
+    lx ≾ ly -> lx ≾' ly
+  ≾->≾' lx ly lx≾ly = transport (λ i → unfold-ord i lx ly) lx≾ly
+
+  adequate-err-baby :
+    ▹ ((lx : L℧ Nat) ->
+      (H-lx : lx ≾' δ ℧) ->
+      (lx ≡ ℧) ⊎ (lx ≡ δ ℧)) ->
+    (lx : L℧ Nat) ->
+    (H-lx : lx ≾' δ ℧) ->
+    (lx ≡ ℧) ⊎ (lx ≡ δ ℧)
+  adequate-err-baby _ (η x) ()
+  adequate-err-baby _ ℧ _ = inl refl
+  adequate-err-baby IH (θ lx~) H-lx =
+    inr (cong θ (tick-extensionality Nat lx~ ℧
+      λ t → {!!}))
+
+
+  data GuardedNat : Type where
+    zro : GuardedNat
+    suc : ▹ Nat -> GuardedNat
+
+  _≤GN_ : GuardedNat -> Nat -> Type
+  n~ ≤GN m = {!!}
+
+{-
+  adequate-err :
+    ▹ ((m : Nat) ->
+    (lx : L℧ Nat) ->
+    (H-lx : lx ≾' (δ ^ m) ℧) ->
+    (Σ (▹ Nat) λ n -> (n ≤GN m) × (lx ≡ (δ ^ n) ℧))) ->
+    (m : Nat) ->
+    (lx : L℧ Nat) ->
+    (H-lx : lx ≾' (δ ^ m) ℧) ->
+    (Σ (▹ Nat) λ n -> (n ≤ m) × ((lx ≡ (δ ^ n) ℧)))
+  adequate-err _ zero (η x) ()
+  adequate-err _ (suc m') (η x) ()
+  adequate-err _ m ℧ H-lx = next (0 , {!!})
+  adequate-err _ zero (θ lx~) ()
+  adequate-err IH (suc m') (θ lx~) H-lx = {!!}
+-}
+
+  ≾'-δ : (lx ly : L℧ Nat) -> (lx ≾' ly) -> (lx ≾' (δ ly))
+  ≾'-δ = {!!}
+
+
+  adequate-err-2 : (m : Nat) -> Σ Nat λ n -> (n ≤ m) ×
+    (▹ ((lx : L℧ Nat) ->
+        (H-lx : lx ≾' (δ ^ m) ℧) ->
+        (lx ≡ (δ ^ n) ℧)) ->
+      (lx : L℧ Nat) ->
+      (H-lx : lx ≾' (δ ^ m) ℧) ->
+      ((lx ≡ (δ ^ n) ℧)))
+  adequate-err-2 zero = zero , ≤-refl , thm-zero
+    where
+      thm-zero : ▹ ((lx : L℧ Nat) → lx ≾' (δ ^ zero) ℧ → lx ≡ (δ ^ zero) ℧) →
+                    (lx : L℧ Nat) → lx ≾' (δ ^ zero) ℧ → lx ≡ (δ ^ zero) ℧
+      thm-zero IH ℧ H-lx = refl
+  adequate-err-2 (suc m') =
+    (suc (fst (adequate-err-2 m'))) , ({!!} , {!!})
+      where
+        thm-suc-m' : {!!}
+        thm-suc-m' IH ℧ H-lx = {!!}
+        thm-suc-m' IH (θ lx~) H-lx =
+          cong θ (tick-irrelevance Nat lx~ ((δ ^ fst (adequate-err-2 m')) ℧)
+          λ t → {!!})
+
+
+-- Given:  θ lx~ ≾' (δ ^ suc m') ℧
+-- i.e.    θ lx~ ≾' θ (next (δ ^ m') ℧)
+-- i.e.    ▸ (λ t -> (lx~ t) ≾ (δ ^ m') ℧)
+
+-- By IH, we have
+-- ▸ (λ t -> lx~ t ≡ (δ ^ n') ℧ for some n')
+
+-- By tick extensionality, we have
+-- lx~ ≡ next (δ ^ n') ℧, so
+-- θ lx~ ≡ θ (next (δ ^ n') ℧) ≡ (δ ^ (suc n')) ℧
+
+
+-- Adequacy of weak bisimilarity relation
+
+open Bisimilarity ℕ
+
+module AdequacyBisimilarity
+  (lx ly : L℧ Nat)
+  (lx≈ly : lx ≈ ly) where
+
+
+-- Combined result: Adequacy of extensional ordering
+
+open ExtRel ℕ
+
+module AdequacyExt
+  (lx ly : L℧ Nat)
+  (lx⊴ly : lx ⊴ ly) where
+
+  adequate-1 : (n : Nat) (x : Nat) ->
+    (lx ≡ (δ ^ n) (η x)) ->
+    Σ Nat λ m -> ly ≡ (δ ^ m) (η x)
+  adequate-1 n x H-lx = {!!}
+
+  adequate-2 : (m : Nat) ->
+    (ly ≡ (δ ^ m) ℧) ->
+    Σ Nat λ n -> lx ≡ (δ ^ n) ℧
+  adequate-2 m H-ly = {!!}
+
+
+
+  
+
+
+
+
+{-
 gradual_guarantee : (M : Tm · nat) (N : Tm · nat) ->
                     · |- M ⊑tm N # nat ->
                     ⟦ M ⟧ ≲ ⟦ N ⟧
+-}

formalizations/guarded-cubical/SyntacticTermPrecision.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 SyntacticTermPrecision (k : Clock) where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat
+open import Cubical.Relation.Nullary
+
+open import ErrorDomains k
+open import GradualSTLC
+
+---- Syntactic term precision relation ----
+
+-- Make this a sigma type
+data CtxTyPrec : Set where
+  · : CtxTyPrec
+  _::_ : {A B : Ty} -> CtxTyPrec -> A ⊑ B -> CtxTyPrec
+
+
+infixr 5 _::_
+
+Ctx-ref : Ctx -> CtxTyPrec
+Ctx-ref · = ·
+Ctx-ref (Γ :: x) = Ctx-ref Γ :: ⊑ref x
+
+
+lhs-ty : {A B : Ty} -> A ⊑ B -> Ty
+lhs-ty {A} d = A
+
+rhs-ty : {A B : Ty} -> A ⊑ B -> Ty
+rhs-ty {_} {B} d = B
+
+lhs : CtxTyPrec -> Ctx
+lhs · = ·
+lhs (ctx :: d) = (lhs ctx) :: lhs-ty d
+
+rhs : CtxTyPrec -> Ctx
+rhs · = ·
+rhs (ctx :: d) = (rhs ctx) :: rhs-ty d
+
+
+lem-lhs : (A : Ty) -> A ≡ lhs-ty (⊑ref A)
+lem-lhs A = refl
+
+lem-rhs : (A : Ty) -> A ≡ rhs-ty (⊑ref A)
+lem-rhs A = refl
+
+
+ctx-refl-lhs : (Γ : Ctx) -> Γ ≡ lhs (Ctx-ref Γ)
+ctx-refl-lhs · = refl
+ctx-refl-lhs (Γ :: x) = λ i -> ctx-refl-lhs Γ i :: lem-lhs x i
+
+ctx-refl-rhs : (Γ : Ctx) -> Γ ≡ rhs (Ctx-ref Γ)
+ctx-refl-rhs · = refl
+ctx-refl-rhs (Γ :: x) = λ i -> ctx-refl-rhs Γ i :: lem-rhs x i
+
+iso-L : {Γ : Ctx} {A : Ty} -> Tm Γ A -> Tm (lhs (Ctx-ref Γ)) A
+iso-L {Γ} {A} M = transport (λ i → Tm (ctx-refl-lhs Γ i) A) M
+
+iso-R : {Γ : Ctx} {A : Ty} -> Tm Γ A -> Tm (rhs (Ctx-ref Γ)) A
+iso-R {Γ} {A} M = transport (λ i -> Tm (ctx-refl-rhs Γ i) A) M
+
+
+TmL : {A B : Ty} -> CtxTyPrec -> A ⊑ B -> Set
+TmL ctx d = {!!}
+
+
+-- "Contains" relation stating that a context Γ contains a type T
+
+data _∋'_ : {A B : Ty} -> CtxTyPrec -> A ⊑ B -> Set where
+
+infix 4 _∋'_
+
+contains-lhs : {A B : Ty} ->
+  (Γ : CtxTyPrec) (d : A ⊑ B) -> (Γ ∋' d) -> (lhs Γ ∋ A)
+contains-lhs = {!!}
+
+contains-rhs : {A B : Ty} ->
+  (Γ : CtxTyPrec) (d : A ⊑ B) -> (Γ ∋' d) -> (rhs Γ ∋ B)
+contains-rhs = {!!}
+
+
+
+
+-- d is fixed here so it should be a parameter, not an index
+-- (hence why it doesn't appear after M and N)
+data ltdyn-tm :
+  {A B : Ty} ->
+  (Γ : CtxTyPrec) ->
+  (d : A ⊑ B) ->
+  (M : Tm (lhs Γ) A) ->
+  (N : Tm (rhs Γ) B) -> Set where
+
+  -- err
+  err : {A B : Ty} -> (Γ : CtxTyPrec) -> (d : A ⊑ B) -> (N : Tm (rhs Γ) B) -> ltdyn-tm Γ d err N
+
+  ---- *Congruence rules* ----
+
+  -- variables
+  -- var : {!{A B : Ty} -> (Γ : CtxTyPrec) -> (d : A ⊑ B) -> (Γ ∋' d) -> ?!}
+  var : (A B : Ty) ->
+        (Γ : CtxTyPrec) ->
+        (d : A ⊑ B) ->
+        (x : Γ ∋' d) ->
+        ltdyn-tm Γ d (var (contains-lhs Γ d x)) (var (contains-rhs Γ d x))
+
+  -- natural numbers
+  zro : (Γ : CtxTyPrec) -> ltdyn-tm Γ nat zro zro
+  suc : (Γ : CtxTyPrec) (M : Tm (lhs Γ) nat) (M' : Tm (rhs Γ) nat) ->
+        ltdyn-tm Γ nat M M' ->
+        ltdyn-tm Γ nat (suc M) (suc M')
+
+  -- lambdas
+  lda : (Γ : CtxTyPrec) (A A' B B' : Ty)
+        (c : A ⊑ A') (d : B ⊑ B')
+        (M1 : Tm ((lhs Γ) :: A) B) (M2 : Tm ((rhs Γ) :: A') B') ->
+        ltdyn-tm (Γ :: c) d M1 M2 ->
+        ltdyn-tm Γ (c => d) (lda M1) (lda M2)
+
+  -- application
+  app : (Γ : CtxTyPrec) (Ain Bin Aout Bout : Ty)
+        (din : Ain ⊑ Bin) (dout : Aout ⊑ Bout)
+        (M1 : Tm (lhs Γ) (Ain => Aout)) (N1 : Tm (lhs Γ) Ain)
+        (M2 : Tm (rhs Γ) (Bin => Bout)) (N2 : Tm (rhs Γ) Bin) ->
+        ltdyn-tm Γ (din => dout) M1 M2 ->
+        ltdyn-tm Γ din N1 N2 ->
+        ltdyn-tm Γ dout (app M1 N1) (app M2 N2)
+    
+
+  ---- *Cast rules* ----
+  
+  upR : (Γ : Ctx) (A B : Ty)
+        (c : A ⊑ B)
+        --(M : Tm (lhs Γ) A)
+        (N : Tm Γ A) ->
+     --   ltdyn-tm Γ (⊑ref A) N N ->
+     ltdyn-tm (Ctx-ref Γ) c (iso-L N) (up c (iso-R N))
+     --   ltdyn-tm (Ctx-ref Γ) c N (up c N)
+
+  upL : (Γ : CtxTyPrec) (A B : Ty)
+        (c : A ⊑ B)
+        (M : Tm (lhs Γ) A)
+        (N : Tm (rhs Γ) B) ->
+        ltdyn-tm Γ c M N ->
+        ltdyn-tm Γ (⊑ref B) (up c M) N
+  
+  dnL : (Γ : Ctx) (A B : Ty)
+        (c : A ⊑ B)
+        (M : Tm Γ B) ->
+       --  (N : Tm (rhs Γ) B) ->
+       --  ltdyn-tm Γ (⊑ref B) M N ->
+       ltdyn-tm (Ctx-ref Γ) c (dn c (iso-L M)) (iso-R M)
+        -- ltdyn-tm Γ c (dn c M) M
+
+  dnR : (Γ : CtxTyPrec) (A B : Ty)
+        (c : A ⊑ B)
+        (M : Tm (lhs Γ) A)
+        (N : Tm (rhs Γ) B) ->
+        ltdyn-tm Γ c M N ->
+        ltdyn-tm Γ (⊑ref A) M (dn c N)
+
+
+-- Notation that matches the written syntax, with d appearing at the end
+_|-_⊑tm_#_ : {A B : Ty} -> (Γ : CtxTyPrec) -> (Tm (lhs Γ) A) -> (Tm (rhs Γ) B) -> A ⊑ B -> Set
+Γ |- M ⊑tm N # d = ltdyn-tm Γ d M N