diff --git a/formalizations/guarded-cubical/Common/Common.agda b/formalizations/guarded-cubical/Common/Common.agda
new file mode 100644
index 0000000000000000000000000000000000000000..c9ca7e6d1c4b5dab629dcd0140fb8fcc14aeec0e
--- /dev/null
+++ b/formalizations/guarded-cubical/Common/Common.agda
@@ -0,0 +1,19 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+
+module Common.Common where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Data.Nat hiding (_^_) renaming (â„• to Nat)
+
+
+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)
diff --git a/formalizations/guarded-cubical/Later.agda b/formalizations/guarded-cubical/Common/Later.agda
similarity index 79%
rename from formalizations/guarded-cubical/Later.agda
rename to formalizations/guarded-cubical/Common/Later.agda
index e68d77e4fb5f6ae4809287efaf77b25d036d30b5..b5624a83a1090ff9d55673498389d3e47b172b74 100644
--- a/formalizations/guarded-cubical/Later.agda
+++ b/formalizations/guarded-cubical/Common/Later.agda
@@ -1,12 +1,12 @@
{-# OPTIONS --cubical --rewriting --guarded #-}
-module Later where
+module Common.Later where
-- | This file is adapted from the supplementary material for the
-- | paper https://doi.org/10.1145/3372885.3373814, originally written
-- | by Niccolò Veltri and Andrea Vezzosi see the LICENSE.txt for
-- | their license.
-open import Agda.Builtin.Equality renaming (_≡_ to _≣_)
+open import Agda.Builtin.Equality renaming (_≡_ to _≣_) hiding (refl)
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Sigma
@@ -130,18 +130,44 @@ next-Mt≡M' M t = next-Mt≡M M t
+
+
+-- Clock-related postulates.
+
+clock-ext : {ℓ : Level} {A : (k : Clock) -> Type ℓ} -> {M N : (k : Clock) -> A k} →
+ (∀ k → M k ≡ N k) → M ≡ N
+clock-ext eq i k = eq k i
+
+
-- "Dependent" forcing (where the type can mention the clock).
-- This seems to be the correct type of the force function.
postulate
force' : {A : Clock -> Type} -> (∀ k → (▹ k , A k)) → (∀ (k : Clock) → A k)
+ -- original (non-dependent) version:
+ -- force'-beta : ∀ {A : Type} (x : A) → force' (λ k -> next x) ≡ λ k → x
+ -- "Reduction" rules:
+ -- Builds in clock extensionality
+ force'-beta : ∀ {A : Clock -> Type} (f : ∀ k -> A k) →
+ force' (λ k -> next (f k)) ≡ f
+
+ -- Builds in clock extensionality
+ next-force' : ∀ {A : Clock -> Type} (f : ∀ k -> ▹ k , A k) ->
+ (λ k -> next (force' f k)) ≡ f
+
+ --next-force' : ∀ {A : Clock -> Type} (f : ∀ k -> ▹ k , A k) ->
+ -- (k : Clock) -> next (force' f k) ≡ f k
+
+
+force-iso : {A : Clock -> Type} -> Iso (∀ k -> (▹ k , A k)) (∀ k -> A k)
+force-iso = iso force' (λ f k → next (f k))
+ force'-beta
+ next-force'
+ -- (λ f → clock-ext (λ k → next-force' f k))
--- Clock-related postulates.
-postulate
- clock-iso : {A : Type} -> (∀ (k : Clock) -> A) ≡ A
postulate
k0 : Clock
@@ -152,7 +178,7 @@ postulate
-}
-- Definition of clock irrelevance, parameterized by a specific type
-clock-irrel : Type -> Type
+clock-irrel : {â„“ : Level} -> Type â„“ -> Type â„“
clock-irrel A =
(M : ∀ (k : Clock) -> A) ->
(k k' : Clock) ->
@@ -165,15 +191,20 @@ clock-irrel A =
-- If A is clock irrelevant, then the above map is inverse
-- to the map A -> ∀ k . A.
+Iso-∀kA-A : {A : Type} -> clock-irrel A -> Iso (∀ (k : Clock) -> A) A
+Iso-∀kA-A {A} H-irrel-A = iso
+ (∀kA->A A)
+ (λ a k -> a)
+ (λ a → refl)
+ (λ f → clock-ext (λ k → H-irrel-A f k0 k))
postulate
nat-clock-irrel : clock-irrel â„•
+ type-clock-irrel : clock-irrel Type
+
-clock-ext : {ℓ : Level} {A : (k : Clock) -> Type ℓ} -> {M N : (k : Clock) -> A k} →
- (∀ k → M k ≡ N k) → M ≡ N
-clock-ext eq i k = eq k i
diff --git a/formalizations/guarded-cubical/Lemmas.agda b/formalizations/guarded-cubical/Common/Lemmas.agda
similarity index 67%
rename from formalizations/guarded-cubical/Lemmas.agda
rename to formalizations/guarded-cubical/Common/Lemmas.agda
index 95c1d1a8535ee850ff9eac6e8ab48463de05293a..dd3acc69e7e4ec4e9597571031dd79261d51f428 100644
--- a/formalizations/guarded-cubical/Lemmas.agda
+++ b/formalizations/guarded-cubical/Common/Lemmas.agda
@@ -3,9 +3,9 @@
-- to allow opening this module in other files while there are still holes
{-# OPTIONS --allow-unsolved-metas #-}
-open import Later
+open import Common.Later
-module Lemmas (k : Clock) where
+module Common.Lemmas (k : Clock) where
open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat renaming (â„• to Nat) hiding (_^_)
@@ -21,9 +21,9 @@ open import Cubical.Data.Empty
open import Cubical.Foundations.Function
-open import StrongBisimulation k
-open import GradualSTLC
-open import SyntacticTermPrecision k
+open import Semantics.StrongBisimulation k
+open import Syntax.GradualSTLC
+open import Syntax.SyntacticTermPrecision k
private
variable
@@ -33,7 +33,7 @@ private
▹_ : Set l → Set l
â–¹_ A = â–¹_,_ k A
-open ð•ƒ
+open LiftPredomain
{-
test : (A B : Type) -> (eq : A ≡ B) -> (x : A) -> (T : (A : Type) -> A -> Type) ->
@@ -137,7 +137,72 @@ mTransportDomain {A} {B} {C} eq f = record {
-- ord' (next ord) (ext' f (next (ext f)) la) (ext' f (next (ext f)) la')
--- ext respects monotonicity
+-- ext respects monotonicity, in a general, heterogeneous sense
+ext-monotone-het : {A A' B B' : Predomain} ->
+ (rAA' : ⟨ A ⟩ -> ⟨ A' ⟩ -> Type) -> (rBB' : ⟨ B ⟩ -> ⟨ B' ⟩ -> Type) ->
+ (f : ⟨ A ⟩ -> ⟨ (𕃠B) ⟩) -> (f' : ⟨ A' ⟩ -> ⟨ (𕃠B') ⟩) ->
+ fun-order-het A A' (𕃠B) (𕃠B') rAA' (LiftRelation._≾_ B B' rBB') f f' ->
+ (la : ⟨ 𕃠A ⟩) -> (la' : ⟨ 𕃠A' ⟩) ->
+ (LiftRelation._≾_ A A' rAA' la la') ->
+ LiftRelation._≾_ B B' rBB' (ext f la) (ext f' la')
+ext-monotone-het {A} {A'} {B} {B'} rAA' rBB' f f' f≤f' la la' la≤la' =
+ let fixed = fix (monotone-ext') in
+ transport
+ (sym (λ i -> LiftBB'.unfold-≾ i (unfold-ext f i la) (unfold-ext f' i la')))
+ (fixed la la' (transport (λ i → LiftAA'.unfold-≾ i la la') la≤la'))
+ where
+
+ -- bring the homogeneous lifted relations into scope
+ _≾LA_ = LiftPredomain._≾_ A
+ _≾LA'_ = LiftPredomain._≾_ A'
+ _≾LB_ = LiftPredomain._≾_ B
+ _≾LB'_ = LiftPredomain._≾_ B'
+
+ -- Note that these next four have already been
+ -- passed (next _≾_) as a parameter (this happened in
+ -- the defintion of the module ð•ƒ, where we said
+ -- open Inductive (next _≾_) public)
+ _≾'LA_ = LiftPredomain._≾'_ A
+ _≾'LA'_ = LiftPredomain._≾'_ A'
+ _≾'LB_ = LiftPredomain._≾'_ B
+ _≾'LB'_ = LiftPredomain._≾'_ B'
+
+
+ module LiftAA' = LiftRelation A A' rAA'
+ module LiftBB' = LiftRelation B B' rBB'
+
+ -- The heterogeneous lifted relations
+ _≾'LALA'_ = LiftAA'.Inductive._≾'_ (next LiftAA'._≾_)
+ _≾'LBLB'_ = LiftBB'.Inductive._≾'_ (next LiftBB'._≾_)
+
+
+ monotone-ext' :
+ â–¹ (
+ (la : ⟨ 𕃠A ⟩) -> (la' : ⟨ 𕃠A' ⟩) ->
+ (la ≾'LALA' la') ->
+ (ext' f (next (ext f)) la) ≾'LBLB'
+ (ext' f' (next (ext f')) la')) ->
+ (la : ⟨ 𕃠A ⟩) -> (la' : ⟨ 𕃠A' ⟩) ->
+ (la ≾'LALA' la') ->
+ (ext' f (next (ext f)) la) ≾'LBLB'
+ (ext' f' (next (ext f')) la')
+ monotone-ext' IH (η x) (η y) x≤y =
+ transport
+ (λ i → LiftBB'.unfold-≾ i (f x) (f' y))
+ (f≤f' x y x≤y)
+ monotone-ext' IH ℧ la' la≤la' = tt
+ monotone-ext' IH (θ lx~) (θ ly~) la≤la' = λ t ->
+ transport
+ (λ i → (sym (LiftBB'.unfold-≾)) i
+ (sym (unfold-ext f) i (lx~ t))
+ (sym (unfold-ext f') i (ly~ t)))
+ (IH t (lx~ t) (ly~ t)
+ (transport (λ i -> LiftAA'.unfold-≾ i (lx~ t) (ly~ t)) (la≤la' t)))
+
+
+
+-- ext respects monotonicity (in the usual homogeneous sense)
+-- This can be rewritten to reuse the above result!
ext-monotone : {A B : Predomain} ->
(f f' : ⟨ A ⟩ -> ⟨ (𕃠B) ⟩) ->
fun-order A (𕃠B) f f' ->
@@ -147,35 +212,45 @@ ext-monotone : {A B : Predomain} ->
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'))
+ (sym (λ i -> unfold-≾ B i (unfold-ext f i la) (unfold-ext f' i la')))
+ (fixed la la' (transport (λ i → unfold-≾ A i la la') la≤la'))
where
+
+ -- bring the homogeneous lifted relations into scope
+ _≾LA_ = LiftPredomain._≾_ A
+ _≾LB_ = LiftPredomain._≾_ B
+
+ -- Note that these next two have already been
+ -- passed (next _≾_) as a parameter (this happened in
+ -- the defintion of the module ð•ƒ, where we said
+ -- open Inductive (next _≾_) public)
+ _≾'LA_ = LiftPredomain._≾'_ A
+ _≾'LB_ = LiftPredomain._≾'_ B
+
monotone-ext' :
(f f' : ⟨ A ⟩ -> ⟨ (𕃠B) ⟩) ->
(fun-order A (𕃠B) f f') ->
â–¹ (
(la la' : ⟨ 𕃠A ⟩) ->
- ord' A (next (ord A)) la la' ->
- ord' B (next (ord B))
- (ext' f (next (ext f)) la)
+ la ≾'LA la' ->
+ (ext' f (next (ext f)) la) ≾'LB
(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)
+ la ≾'LA la' ->
+ (ext' f (next (ext f)) la) ≾'LB
(ext' f' (next (ext f')) la')
monotone-ext' f f' f≤f' IH (η x) (η y) x≤y =
transport
- (λ i → unfold-ord B i (f x) (f' y))
+ (λ i → unfold-≾ B i (f x) (f' y))
(f≤f' x y x≤y)
monotone-ext' f f' f≤f' IH ℧ la' la≤la' = tt
monotone-ext' f f' f≤f' IH (θ lx~) (θ ly~) la≤la' = λ t ->
transport
- (λ i → (sym (unfold-ord B)) i
+ (λ i → (sym (unfold-≾ B)) i
(sym (unfold-ext f) i (lx~ t))
(sym (unfold-ext f') i (ly~ t)))
(IH t (lx~ t) (ly~ t)
- (transport (λ i -> unfold-ord A i (lx~ t) (ly~ t)) (la≤la' t)))
+ (transport (λ i -> unfold-≾ A i (lx~ t) (ly~ t)) (la≤la' t)))
@@ -223,6 +298,20 @@ bind-monotone {A} {B} {la} {la'} f f' la≤la' f≤f' =
ext-monotone f f' f≤f' la la' la≤la'
+mapL-monotone-het : {A A' B B' : Predomain} ->
+ (rAA' : ⟨ A ⟩ -> ⟨ A' ⟩ -> Type) -> (rBB' : ⟨ B ⟩ -> ⟨ B' ⟩ -> Type) ->
+ (f : ⟨ A ⟩ -> ⟨ B ⟩) -> (f' : ⟨ A' ⟩ -> ⟨ B' ⟩) ->
+ fun-order-het A A' B B' rAA' rBB' f f' ->
+ (la : ⟨ 𕃠A ⟩) -> (la' : ⟨ 𕃠A' ⟩) ->
+ (LiftRelation._≾_ A A' rAA' la la') ->
+ LiftRelation._≾_ B B' rBB' (mapL f la) (mapL f' la')
+mapL-monotone-het {A} {A'} {B} {B'} rAA' rBB' f f' f≤f' la la' la≤la' =
+ ext-monotone-het rAA' rBB' (ret ∘ f) (ret ∘ f')
+ (λ a a' a≤a' → LiftRelation.Properties.ord-η-monotone B B' rBB' (f≤f' a a' a≤a'))
+ la la' la≤la'
+
+
+-- This is a special case of the above
mapL-monotone : {A B : Predomain} ->
{la la' : ⟨ 𕃠A ⟩} ->
(f f' : ⟨ A ⟩ -> ⟨ B ⟩) ->
diff --git a/formalizations/guarded-cubical/MonFuns.agda b/formalizations/guarded-cubical/Common/MonFuns.agda
similarity index 79%
rename from formalizations/guarded-cubical/MonFuns.agda
rename to formalizations/guarded-cubical/Common/MonFuns.agda
index ff86d56ea24886841140e8ccf58155de74aba206..9ff06719bdae463d1f1586a1f6b9eff97093c9aa 100644
--- a/formalizations/guarded-cubical/MonFuns.agda
+++ b/formalizations/guarded-cubical/Common/MonFuns.agda
@@ -3,9 +3,9 @@
-- to allow opening this module in other files while there are still holes
{-# OPTIONS --allow-unsolved-metas #-}
-open import Later
+open import Common.Later
-module MonFuns (k : Clock) where
+module Common.MonFuns (k : Clock) where
open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat renaming (â„• to Nat)
@@ -22,10 +22,11 @@ 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 Common.Common
+open import Semantics.StrongBisimulation k
+open import Syntax.GradualSTLC
+open import Syntax.SyntacticTermPrecision k
+open import Common.Lemmas k
private
@@ -36,8 +37,9 @@ private
▹_ : Set l → Set l
â–¹_ A = â–¹_,_ k A
+open MonFun
-open ð•ƒ
+open LiftPredomain
-- abstract
@@ -106,8 +108,8 @@ mSuc = record {
U : {A B : Predomain} -> ⟨ A ==> B ⟩ -> ⟨ A ⟩ -> ⟨ B ⟩
U f = MonFun.f f
-_<$$>_ : {A B : Predomain} -> ⟨ A ==> B ⟩ -> ⟨ A ⟩ -> ⟨ B ⟩
-_<$$>_ = U
+_$_ : {A B : Predomain} -> ⟨ A ==> B ⟩ -> ⟨ A ⟩ -> ⟨ B ⟩
+_$_ = U
S : (Γ : Predomain) -> {A B : Predomain} ->
⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
@@ -140,12 +142,15 @@ Id = record { f = id ; isMon = λ x≤y → x≤y }
Curry : {Γ A B : Predomain} -> ⟨ (Γ ×d A) ==> B ⟩ -> ⟨ Γ ==> A ==> B ⟩
-Curry f = record {
+Curry {Γ} g = record {
f = λ γ →
record {
- f = λ a → MonFun.f f (γ , a) ;
- isMon = {!!} } ;
- isMon = {!!} }
+ f = λ a → MonFun.f g (γ , a) ;
+ -- For a fixed γ, f as defined directly above is monotone
+ isMon = λ {a} {a'} a≤a' → MonFun.isMon g (reflexive Γ _ , a≤a') } ;
+
+ -- The outer f is monotone in γ
+ isMon = λ {γ} {γ'} γ≤γ' → λ a a' a≤a' -> MonFun.isMon g (γ≤γ' , a≤a') }
Uncurry : {Γ A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ (Γ ×d A) ==> B ⟩
Uncurry f = record {
@@ -171,23 +176,10 @@ Swap Γ f = record {
λ γ1 γ2 γ1≤γ2 -> {!!} } -- γ1 γ2 γ1≤γ2 → {!!} }
- -- Convenience versions of comp, ext, and ret using combinators
-
-mComp' : (Γ : Predomain) -> {A B C : Predomain} ->
- ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
-mComp' Γ 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_
+SwapPair : {A B : Predomain} -> ⟨ (A ×d B) ==> (B ×d A) ⟩
+SwapPair = record {
+ f = λ { (a , b) -> b , a } ;
+ isMon = λ { {a1 , b1} {a2 , b2} (a1≤a2 , b1≤b2) → b1≤b2 , a1≤a2} }
-- Apply a monotone function to the first or second argument of a pair
@@ -210,17 +202,76 @@ Cong2nd = {!!}
-IntroArg : {Γ B B' : Predomain} ->
+IntroArg' : {Γ B B' : Predomain} ->
⟨ Γ ==> B ⟩ -> ⟨ B ==> B' ⟩ -> ⟨ Γ ==> B' ⟩
-IntroArg {Γ} {B} {B'} fΓB fBB' = S Γ (With2nd fBB') fΓB
+IntroArg' {Γ} {B} {B'} fΓB fBB' = S Γ (With2nd fBB') fΓB
-- S : ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+IntroArg : {Γ B B' : Predomain} ->
+ ⟨ B ==> B' ⟩ -> ⟨ (Γ ==> B) ==> (Γ ==> B') ⟩
+IntroArg f = Curry (mCompU f App)
+
+
+PairAssocLR : {A B C : Predomain} ->
+ ⟨ A ×d B ×d C ==> A ×d (B ×d C) ⟩
+PairAssocLR = record {
+ f = λ { ((a , b) , c) → a , (b , c) } ;
+ isMon = λ { {(a1 , b1) , c1} {(a2 , b2) , c2} ((a1≤a2 , b1≤b2) , c1≤c2) →
+ a1≤a2 , (b1≤b2 , c1≤c2)} }
+
+PairAssocRL : {A B C : Predomain} ->
+ ⟨ A ×d (B ×d C) ==> A ×d B ×d C ⟩
+PairAssocRL = record {
+ f = λ { (a , (b , c)) -> (a , b) , c } ;
+ isMon = λ { {a1 , (b1 , c1)} {a2 , (b2 , c2)} (a1≤a2 , (b1≤b2 , c1≤c2)) →
+ (a1≤a2 , b1≤b2) , c1≤c2} }
+
+PairCong : {Γ A A' : Predomain} ->
+ ⟨ A ==> A' ⟩ -> ⟨ (Γ ×d A) ==> (Γ ×d A') ⟩
+PairCong f = record {
+ f = λ { (γ , a) → γ , (f $ a)} ;
+ isMon = λ { {γ1 , a1} {γ2 , a2} (γ1≤γ2 , a1≤a2) → γ1≤γ2 , isMon f a1≤a2 }}
+
+{-
+PairCong : {Γ A A' : Predomain} ->
+ ⟨ A ==> A' ⟩ -> ⟨ (Γ ×d A) ==> (Γ ×d A') ⟩
+PairCong f = Uncurry (mCompU {!!} {!!})
+-- Goal:
+-- Γ ==> (A ==> Γ ×d A')
+-- Write it as : Γ ==> (A ==> (A' ==> Γ ×d A'))
+-- i.e. Γ ==> A' ==> Γ ×d A'
+-- Pair : ⟨ A ==> B ==> A ×d B ⟩
+-}
TransformDomain : {Γ A A' B : Predomain} ->
⟨ Γ ×d A ==> B ⟩ ->
⟨ ( A ==> B ) ==> ( A' ==> B ) ⟩ ->
⟨ Γ ×d A' ==> B ⟩
-TransformDomain f1 f2 = Uncurry (IntroArg (Curry f1) f2)
+TransformDomain fΓ×A->B f = Uncurry (IntroArg' (Curry fΓ×A->B) f)
+
+
+
+ -- Convenience versions of comp, ext, and ret using combinators
+
+mComp' : (Γ : Predomain) -> {A B C : Predomain} ->
+ ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+mComp' Γ {A} {B} {C} f g = S {!!} (mCompU f aux) g
+ where
+ aux : ⟨ Γ ×d A ×d B ==> Γ ×d B ⟩
+ aux = mCompU π1 (mCompU (mCompU PairAssocRL (PairCong SwapPair)) PairAssocLR)
+
+ aux2 : ⟨ Γ ×d B ==> C ⟩ -> ⟨ Γ ×d A ×d B ==> C ⟩
+ aux2 h = mCompU f aux
+
+
+_∘m_ : {Γ A B C : Predomain} ->
+ ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+_∘m_ {Γ} = mComp' Γ
+
+_$_∘m_ : (Γ : Predomain) -> {A B C : Predomain} ->
+ ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+Γ $ f ∘m g = mComp' Γ f g
+infixl 20 _∘m_
mExt' : (Γ : Predomain) -> {A B : Predomain} ->
@@ -250,7 +301,7 @@ mMap {A} {B} = Curry (mExt' (A ==> B) ((With2nd mRet) ∘m App))
mMap' : {Γ A B : Predomain} ->
⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d 𕃠A ==> 𕃠B) ⟩
-mMap' f = Uncurry {!!}
+mMap' f = {!!}
Map : {Γ A B : Predomain} ->
⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ==> 𕃠A) ⟩ -> ⟨ (Γ ==> 𕃠B) ⟩
@@ -321,6 +372,7 @@ mFunProj A A' B B' fAA' fB'LB = {!!}
-- ((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 ⟩) ->
@@ -358,3 +410,5 @@ bind-K = {!!}
{- Goal: rel (⟦ Γ ⟧ctx ==> 𕃠⟦ B ⟧ty) ⟦ err [ N ] ⟧tm
(Bind ⟦ Γ ⟧ctx ⟦ N ⟧tm (Curry ⟦ err ⟧tm))
-}
+
+-}
diff --git a/formalizations/guarded-cubical/Interpretation.agda b/formalizations/guarded-cubical/Interpretation.agda
deleted file mode 100644
index 513d6500811cb79bbeefc1cd0f7363bbfbc36e57..0000000000000000000000000000000000000000
--- a/formalizations/guarded-cubical/Interpretation.agda
+++ /dev/null
@@ -1,91 +0,0 @@
-{-# OPTIONS --cubical --rewriting --guarded #-}
-
--- Define the interpretation of the syntax
-
-open import Later
-
-module Interpretation (k : Clock) where
-
- open import Cubical.Foundations.Prelude
- open import Cubical.Foundations.Function
- open import Cubical.Foundations.Transport
- open import Cubical.Data.Unit
- open import Cubical.Data.Nat hiding (_^_)
- open import Cubical.Data.Prod
- open import Cubical.Data.Empty
- open import Cubical.Relation.Binary.Poset
-
- open import ErrorDomains k
- open import GradualSTLC
-
- private
- variable
- l : Level
- A B : Set l
- private
- ▹_ : Set l → Set l
- â–¹_ A = â–¹_,_ k A
-
- -- Denotational semantics
-
- ⟦_⟧ty : Ty -> Type
- ⟦ nat ⟧ty = ℕ
- ⟦ dyn ⟧ty = Dyn
- ⟦ A => B ⟧ty = ⟦ A ⟧ty -> L℧ ⟦ B ⟧ty
-
- ⟦_⟧ctx : Ctx -> Type
- ⟦ · ⟧ctx = Unit
- ⟦ Γ :: A ⟧ctx = ⟦ Γ ⟧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
-
-{-
- ⟦_⟧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
- ⟦ nat ⟧lt = EP-id ℕ
- ⟦ 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)
- ⟦ var x ⟧tm = λ ⟦Γ⟧ -> ret (look ⟦Γ⟧ _ x)
-
- ⟦ lda M ⟧tm = λ ⟦Γ⟧ -> ret ( λ N -> ⟦ M ⟧tm (⟦Γ⟧ , N) )
-
- ⟦ app M1 M2 ⟧tm =
- -- λ Γ -> bind (⟦ M1 ⟧tm Γ) λ f -> bind (⟦ M2 ⟧tm Γ) f
- λ Γ -> bind (⟦ M1 ⟧tm Γ) (bind (⟦ M2 ⟧tm Γ))
-
- ⟦ err ⟧tm ⟦Γ⟧ = ℧
-
- ⟦ up {Γ = Γ2} {A = A} {B = B} A⊑B M ⟧tm =
- λ ⟦Γ⟧ -> mapL (EP.emb ⟦ A⊑B ⟧lt) (⟦ M ⟧tm ⟦Γ⟧)
- -- Equivalently:
- -- EP.emb (EP-L ⟦ A⊑B ⟧lt) (⟦ M ⟧tm ⟦Γ⟧)
-
- ⟦ dn {A = A} {B = B} A⊑B M ⟧tm =
- λ ⟦Γ⟧ -> bind (⟦ M ⟧tm ⟦Γ⟧) (EP.proj ⟦ A⊑B ⟧lt)
-
-
- 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
-
-
- --------------------------------------------------------------------------------
-
-
-
-
diff --git a/formalizations/guarded-cubical/Results.agda b/formalizations/guarded-cubical/Results.agda
deleted file mode 100644
index 9e1a62e5f7f6cda9017c13057216e724d8b1a639..0000000000000000000000000000000000000000
--- a/formalizations/guarded-cubical/Results.agda
+++ /dev/null
@@ -1,251 +0,0 @@
-{-# 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.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
- l : Level
- A B : Set l
-private
- ▹_ : Set l → Set l
- â–¹_ 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 ⟧
--}
diff --git a/formalizations/guarded-cubical/Results/Coinductive.agda b/formalizations/guarded-cubical/Results/Coinductive.agda
new file mode 100644
index 0000000000000000000000000000000000000000..d5e19891ce52f8d7dd15891d337d462acd8988bc
--- /dev/null
+++ b/formalizations/guarded-cubical/Results/Coinductive.agda
@@ -0,0 +1,247 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+{-# OPTIONS --guardedness #-}
+
+
+open import Common.Later
+
+module Results.Coinductive where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Sum
+open import Cubical.Data.Unit renaming (Unit to ⊤)
+open import Cubical.Data.Sigma
+open import Cubical.Data.Nat renaming (ℕ to Nat) hiding (_·_ ; _^_)
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Structure
+open import Cubical.Data.Empty
+
+open import Results.IntensionalAdequacy
+open import Semantics.StrongBisimulation
+
+private
+ variable
+ l : Level
+ X : Type l
+
+
+{-
+-- If there was an answer produced at each step, we could parameterize by another type A,
+-- and make running have type A -> State Res
+mutual
+ data State (Res : Type) : Type where
+ done : Res -> State Res
+ running : Machine Res -> State Res
+
+ record Machine (B : Type) : Type where
+ coinductive
+ field
+ view : State B
+
+open Machine
+
+Ω : {B : Type} -> Machine B
+-- Ω .view = running (Ω .view)
+view Ω = running Ω
+
+
+isom : {X : Type} -> Iso (L℧F X) (Machine (X ⊎ ⊤))
+isom {X} = iso {!!} {!!} {!!} {!!}
+ where
+ f : (L℧F X) -> (Machine (X ⊎ ⊤))
+ view (f l) with (l k0)
+ ... | η x = done (inl x)
+ ... | ℧ = done (inr tt)
+ ... | θ lx~ = running (f l)
+
+ inv : Machine (X ⊎ ⊤) -> L℧F X
+ inv m with (view m)
+ ... | done (inl x) = ηF x
+ ... | done (inr tt) = ℧F
+ ... | running m' = λ k -> θ λ t → inv m'' {!!}
+ where
+ m'' : Machine (X ⊎ ⊤)
+ view m'' = {!!}
+-}
+
+
+{-
+ inv : Machine (X ⊎ ⊤) -> L℧F X
+ inv m with (view m)
+ ... | done (inl x) = λ k -> η x
+ ... | done (inr x) = λ k -> ℧
+ ... | running = λ k -> θ λ t → {!!}
+
+-}
+
+
+
+
+
+{-
+-- A until B == B + A × (A until B)
+record Machine (B : Type) : Type where
+ coinductive
+ field
+ -- view : State B
+ view : B ⊎ (Unit × Machine B)
+
+open Machine
+
+Ω : {B : Type} -> Machine B
+Ω .view = inr (tt , Ω)
+-- equivalently:
+--view Ω = inr (tt , Ω)
+-- But this doesn't work:
+-- Ω = record { view = inr (tt , Ω) } -- fails termination checking
+
+
+
+module _ {X : Type} (H-irrel : clock-irrel X) where
+
+ ∀-to-machine' : (L℧F X) -> Machine (X ⊎ ⊤)
+ view (∀-to-machine' l) with (Iso.fun (L℧F-iso H-irrel) l)
+ ... | inl (inl x) = inl (inl x)
+ ... | inl (inr _) = inl (inr tt)
+ ... | inr l' = inr (tt , (∀-to-machine' l'))
+
+
+-}
+
+record Machine (Res : Type) : Type
+
+data State (Res : Type) : Type where
+ result : Res -> State Res
+ error : State Res
+ running : Machine Res -> State Res
+
+record Machine Res where
+ coinductive
+ field view : State Res
+
+open Machine public
+
+
+module _ {X : Type} (H-irrel : clock-irrel X) where
+
+ ∀-to-machine : (L℧F X) -> Machine X
+ view (∀-to-machine l) with (Iso.fun (L℧F-iso H-irrel) l)
+ ... | inl (inl x) = result x
+ ... | inl (inr _) = error
+ ... | inr l' = running (∀-to-machine l')
+
+
+ -- We can't use normal recursion, because the argument is coinductive and so may be infinite.
+ {-
+ machine-to-∀ : Machine X -> L℧F X
+ machine-to-∀ m with (view m)
+ ... | result x = ηF x
+ ... | error = ℧F
+ ... | running m' = λ k -> θ λ t → machine-to-∀ m' k
+ -}
+
+
+ {-
+ machine-to-∀' : (k : Clock) -> (Machine X) -> L℧ k X
+ machine-to-∀' k m = fix f
+ where
+ f : ▹ k , L℧ k X -> L℧ k X
+ f lx~ with (view m)
+ ... | result x = η x
+ ... | error = ℧
+ ... | running m' = θ (λ t → lx~ t)
+ -}
+
+
+ machine-to-∀'' : (k : Clock) -> ▹ k , (Machine X -> L℧ k X) -> (Machine X -> L℧ k X)
+ machine-to-∀'' k rec m with (view m)
+ ... | result x = η x
+ ... | error = ℧
+ ... | running m' = θ (λ t → rec t m')
+
+ -- Instead, we can define it by a guarded fixpoint.
+ machine-to-∀' : (k : Clock) -> (Machine X) -> L℧ k X
+ machine-to-∀' k = fix (machine-to-∀'' k)
+
+ machine-to-∀ : Machine X -> L℧F X
+ machine-to-∀ m k = fix (machine-to-∀'' k) m
+
+ retr : retract ∀-to-machine machine-to-∀
+ retr l with (Iso.fun (L℧F-iso H-irrel) l)
+ ... | inl (inl x) = clock-ext (λ k → {!!})
+ ... | inl (inr _) = {!!}
+ ... | inr x = {!!}
+
+
+ -- Showing these are inverses requires a notion of equality for Machines,
+ -- which is the bisimilarity relation defined below.
+
+
+
+-- Bisimilarity relation on Machines.
+module Bisim (X : Predomain k0) (H-irrel : clock-irrel ⟨ X ⟩) where
+
+
+ -- Mutually define coinductive bisimilarity of machines
+ -- along with the relation on states of a machine.
+
+
+ record _≋_ (m m' : Machine ⟨ X ⟩) : Type
+
+ _≋''_ : State ⟨ X ⟩ -> State ⟨ X ⟩ -> Type
+ result x ≋'' result x' = rel k0 X x x'
+ error ≋'' error = ⊤
+ running m ≋'' running m' = m ≋ m' -- using the coinductive bisimilarity on machines
+ _ ≋'' _ = ⊥
+
+
+ data _≋'_ (s s' : State ⟨ X ⟩) : Type
+
+ record _≋_ m m' where
+ coinductive
+ field prove : view m ≋' view m'
+
+ data _≋'_ s s' where
+ con : s ≋'' s' -> s ≋' s'
+
+
+ open _≋_ public
+
+
+
+
+
+
+
+
+
+
+{-
+∀-to-machine : (L℧F X) -> (Machine (X ⊎ ⊤))
+view (∀-to-machine l) with (l k0)
+... | η x = inl (inl x) -- done (inl x) }
+... | ℧ = inl (inr tt) -- done (inr tt) }
+... | θ lx~ = inr (tt , (∀-to-machine l)) -- running }
+
+{-# TERMINATING #-}
+machine-to-∀ : Machine (X ⊎ ⊤) -> L℧F X
+machine-to-∀ m with (view m)
+... | inl (inl x) = λ k -> η x
+... | inl (inr tt) = λ k -> ℧
+... | inr (tt , m') = λ k -> θ λ t → machine-to-∀ m' k
+
+isom : {X : Type} -> Iso (L℧F X) (Machine (X ⊎ ⊤))
+isom {X} = iso ∀-to-machine machine-to-∀ sec retr
+ where
+ sec : section ∀-to-machine machine-to-∀
+ sec m with (view m)
+ ... | inl (inl x) = {!!}
+ ... | inl (inr tt) = {!!}
+ ... | inr (_ , m') = {!!}
+
+ retr : retract ∀-to-machine machine-to-∀
+ retr l with (l k0) in eq
+ ... | η x = clock-ext {!!}
+ ... | ℧ = clock-ext {!!}
+ ... | θ l~ = {!!}
+
+-}
diff --git a/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda b/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda
new file mode 100644
index 0000000000000000000000000000000000000000..7b4a0d6e408b40fb91ba78926347827a316ea1d3
--- /dev/null
+++ b/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda
@@ -0,0 +1,361 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+{-# OPTIONS --guardedness #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+
+open import Common.Later
+
+
+module Results.IntensionalAdequacy where
+
+open import Cubical.Foundations.Prelude
+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 Cubical.Data.Unit renaming (Unit to ⊤)
+
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+
+open import Cubical.Foundations.Function
+
+import Semantics.StrongBisimulation
+import Common.MonFuns
+import Syntax.GradualSTLC
+
+open import Common.Common
+
+-- TODO move definition of Predomain to a module that
+-- isn't parameterized by a clock!
+
+private
+ variable
+ l : Level
+ X : Type l
+
+-- Lift monad
+open Semantics.StrongBisimulation
+-- open StrongBisimulation.LiftPredomain
+
+
+-- "Global" definitions
+L℧F : (X : Type) -> Type
+L℧F X = ∀ (k : Clock) -> L℧ k X
+
+ηF : {X : Type} -> X -> L℧F X
+ηF {X} x = λ k → η x
+
+℧F : {X : Type} -> L℧F X
+℧F = λ k -> ℧
+
+θF : {X : Type} -> L℧F X -> L℧F X
+θF lx = λ k → θ (λ t → lx k)
+
+δ-gl : {X : Type} -> L℧F X -> L℧F X
+δ-gl lx = λ k → δ k (lx k)
+
+δ-gl^n : (lxF : L℧F Nat) -> (n : Nat) -> (k : Clock) ->
+ ((δ-gl) ^ n) lxF k ≡ ((δ k) ^ n) (lxF k)
+δ-gl^n lxF zero k = refl
+δ-gl^n lxF (suc n') k = cong (δ k) (δ-gl^n lxF n' k)
+
+
+{-
+ _Iso⟨_⟩_ : {ℓ ℓ' ℓ'' : Level} {B : Type ℓ'} {C : Type ℓ''}
+ (X : Type ℓ) →
+ Iso X B → Iso B C → Iso X C
+ _∎Iso : {ℓ : Level} (A : Type ℓ) → Iso A A
+
+
+ Σ-Π-Iso : {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : A → Type ℓ'}
+ {C : (a : A) → B a → Type ℓ''} →
+ Iso ((a : A) → Σ-syntax (B a) (C a))
+ (Σ-syntax ((a : A) → B a) (λ f → (a : A) → C a (f a)))
+
+ codomainIsoDep
+ : {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : A → Type ℓ'}
+ {C : A → Type ℓ''} →
+ ((a : A) → Iso (B a) (C a)) → Iso ((a : A) → B a) ((a : A) → C a)
+
+ ⊎Iso : {A.ℓa : Level} {A : Type A.ℓa} {C.ℓc : Level}
+ {C : Type C.â„“c} {B.â„“b : Level} {B : Type B.â„“b} {D.â„“d : Level}
+ {D : Type D.ℓd} →
+ Iso A C → Iso B D → Iso (A ⊎ B) (C ⊎ D)
+-}
+
+Unit-clock-irrel : clock-irrel Unit
+Unit-clock-irrel M k k' with M k | M k'
+... | tt | tt = refl
+
+∀kL℧-▹-Iso : {X : Type} -> Iso ((k : Clock) -> ▹_,_ k (L℧ k X)) ((k : Clock) -> L℧ k X)
+∀kL℧-▹-Iso = force-iso
+
+∀clock-Σ : {A : Type} -> {B : A -> Clock -> Type} ->
+ -- (∀ a k -> clock-irrel (B a k)) ->
+ clock-irrel A ->
+ (∀ (k : Clock) -> Σ A (λ a -> B a k)) ->
+ Σ A (λ a -> ∀ (k : Clock) -> B a k)
+∀clock-Σ {A} {B} H-clk-irrel H =
+ let a = fst (H k0) in
+ a , (λ k -> transport
+ (λ i → B (H-clk-irrel (fst ∘ H) k k0 i) k)
+ (snd (H k)))
+ -- NTS: B (fst (H k)) k ≡ B (fst (H k0)) k
+ -- i.e. essentially need to show that fst (H k) ≡ fst (H k0)
+ -- This follows from clock irrelevance for A, with M = fst ∘ H of type Clock -> A
+
+
+
+Iso-Π-⊎ : {A B : Clock -> Type} ->
+ Iso ((k : Clock) -> (A k ⊎ B k)) (((k : Clock) -> A k) ⊎ ((k : Clock) -> B k))
+Iso-Π-⊎ {A} {B} = iso to inv sec retr
+ where
+ to : ((k : Clock) → A k ⊎ B k) → ((k : Clock) → A k) ⊎ ((k : Clock) → B k)
+ to f with f k0
+ ... | inl a = inl (λ k → transport (type-clock-irrel A k0 k) a)
+ ... | inr b = inr (λ k → transport (type-clock-irrel B k0 k) b)
+
+ inv : ((k : Clock) → A k) ⊎ ((k : Clock) → B k) -> ((k : Clock) → A k ⊎ B k)
+ inv (inl f) k = inl (f k)
+ inv (inr f) k = inr (f k)
+
+ sec : section to inv
+ sec (inl f) = cong inl (clock-ext λ k -> {!!})
+ sec (inr f) = cong inr (clock-ext (λ k -> {!!}))
+
+ retr : retract to inv
+ retr f with (f k0)
+ ... | inl a = clock-ext (λ k → {!!})
+ ... | inr b = {!!}
+
+ {-
+ transport-filler
+ : {ℓ : Level} {A B : Type ℓ} (p : A ≡ B) (x : A) →
+ PathP (λ i → p i) x (transport p x)
+ -}
+
+L℧-iso : {k : Clock} -> {X : Type} -> Iso (L℧ k X) ((X ⊎ ⊤) ⊎ (▹_,_ k (L℧ k X)))
+L℧-iso {k} {X} = iso f g sec retr
+ where
+ f : L℧ k X → (X ⊎ ⊤) ⊎ (▹ k , L℧ k X)
+ f (η x) = inl (inl x)
+ f ℧ = inl (inr tt)
+ f (θ lx~) = inr lx~
+
+ g : (X ⊎ ⊤) ⊎ (▹ k , L℧ k X) -> L℧ k X
+ g (inl (inl x)) = η x
+ g (inl (inr tt)) = ℧
+ g (inr lx~) = θ lx~
+
+ sec : section f g
+ sec (inl (inl x)) = refl
+ sec (inl (inr tt)) = refl
+ sec (inr lx~) = refl
+
+ retr : retract f g
+ retr (η x) = refl
+ retr ℧ = refl
+ retr (θ x) = refl
+
+
+L℧F-iso : {X : Type} -> clock-irrel X -> Iso (L℧F X) ((X ⊎ ⊤) ⊎ (L℧F X))
+L℧F-iso {X} H-irrel-X =
+ (∀ k -> L℧ k X)
+
+ Iso⟨ codomainIsoDep (λ k -> L℧-iso) ⟩
+
+ (∀ k -> (X ⊎ ⊤) ⊎ (▹_,_ k (L℧ k X)))
+
+ Iso⟨ Iso-Π-⊎ ⟩
+
+ (∀ (k : Clock) -> (X ⊎ ⊤)) ⊎ (∀ k -> ▹_,_ k (L℧ k X))
+
+ Iso⟨ ⊎Iso Iso-Π-⊎ idIso ⟩
+
+ ((∀ (k : Clock) -> X) ⊎ (∀ (k : Clock) -> ⊤)) ⊎
+ (∀ k -> ▹_,_ k (L℧ k X))
+
+ Iso⟨ ⊎Iso (⊎Iso (Iso-∀kA-A H-irrel-X) (Iso-∀kA-A Unit-clock-irrel)) force-iso ⟩
+
+ (X ⊎ ⊤) ⊎ (L℧F X) ∎Iso
+
+
+unfold-L℧F : {X : Type} -> clock-irrel X -> (L℧F X) ≡ ((X ⊎ ⊤) ⊎ (L℧F X))
+unfold-L℧F H = ua (isoToEquiv (L℧F-iso H))
+
+
+
+-- Adequacy of lock-step relation
+module AdequacyLockstep
+
+ where
+
+ open Semantics.StrongBisimulation
+ open Semantics.StrongBisimulation.LiftPredomain
+
+ _≾-gl_ : {p : Predomain k0} -> (L℧F ⟨ p ⟩) -> (L℧F ⟨ p ⟩) -> Type
+ _≾-gl_ {p} lx ly = ∀ (k : Clock) -> _≾_ k p (lx k) (ly k)
+
+ -- _≾'_ : {k : Clock} -> L℧ k Nat → L℧ k Nat → Type
+ -- _≾'_ {k} = {!!}
+
+
+ -- These should probably be moved to the module where _≾'_ is defined.
+ ≾'-℧ : {k : Clock} -> (lx : L℧ k Nat) ->
+ _≾'_ k (ℕ k0) lx ℧ -> lx ≡ ℧
+ ≾'-℧ (η x) ()
+ ≾'-℧ ℧ _ = refl
+ ≾'-℧ (θ x) ()
+
+ ≾'-θ : {k : Clock} -> (lx : L℧ k Nat) -> (ly~ : ▹_,_ k (L℧ k Nat)) ->
+ _≾'_ k (ℕ k0) lx (θ ly~) ->
+ Σ (▹_,_ k (L℧ k Nat)) (λ lx~ -> lx ≡ θ lx~)
+ ≾'-θ (θ lz~) ly~ H = lz~ , refl
+ ≾'-θ ℧ ly~ x = {!!}
+
+
+ L℧F-▹alg : ((k : Clock) -> ▹_,_ k (L℧ k Nat)) -> L℧F Nat
+ L℧F-▹alg = λ lx~ → λ k → θ (lx~ k)
+
+ L℧F-▹alg' : ((k : Clock) -> ▹_,_ k (L℧ k Nat)) -> L℧F Nat
+ L℧F-▹alg' = λ lx~ → λ k → θ (λ t → lx~ k t)
+
+
+ helper : {X : Type} -> {k : Clock} -> (M~ : â–¹_,_ k X) ->
+ next (M~ ◇) ≡ M~
+ helper M~ = next-Mt≡M M~ ◇
+
+
+ adequate-err' :
+ (m : Nat) ->
+ (lxF : L℧F Nat) ->
+ (H-lx : _≾-gl_ {ℕ k0} lxF ((δ-gl ^ m) ℧F)) ->
+ (Σ (Nat) λ n -> (n ≤ m) × ((lxF ≡ (δ-gl ^ n) ℧F)))
+ adequate-err' zero lxF H-lx with (Iso.fun (L℧F-iso nat-clock-irrel) lxF)
+ ... | inl (inl x) = zero , {!!}
+ ... | _ = {!!}
+ adequate-err' (suc m) = {!!}
+
+ adequate-err :
+ (m : Nat) ->
+ (lxF : L℧F Nat) ->
+ (H-lx : _≾-gl_ {ℕ k0} lxF ((δ-gl ^ m) ℧F)) ->
+ (Σ (Nat) λ n -> (n ≤ m) × ((lxF ≡ (δ-gl ^ n) ℧F)))
+ adequate-err zero lxF H-lxF =
+ let H' = transport (λ i -> ∀ k -> unfold-≾ k (ℕ k0) i (lxF k) (℧F k)) H-lxF in
+ zero , ≤-refl , clock-ext λ k → ≾'-℧ (lxF k) (H' k)
+ -- H' says that for all k, (lxF k) ≾' (℧F k) i.e.
+ -- for all k, (lxF k) ≾' ℧, which means, by definition of ≾',
+ -- for all k, (lxF k) = ℧, which means, by clock extensionality,
+ -- that lxF = ℧F.
+ adequate-err (suc m') lxF H-lxF =
+ let IH = adequate-err m' (λ k → fst (fst (aux k)) ◇) (λ k → snd (aux k))
+ in {!!}
+ where
+ aux : (k : Clock) -> (Σ (▹ k , L℧ k Nat) (λ lx~ → lxF k ≡ θ lx~)) × _
+ aux k = let RHS = (((δ-gl ^ m') ℧F) k) in
+ let RHS' = (δ k RHS) in
+ let H1 = transport (λ i -> unfold-≾ k (ℕ k0) i (lxF k) RHS') (H-lxF k) in
+ let pair = ≾'-θ (lxF k) (next RHS) H1 in
+ let H2 = transport (λ i → _≾'_ k (ℕ k0) (snd pair i) RHS') H1 in
+ let H3 = transport ((λ i -> (t : Tick k) -> _≾_ k (ℕ k0) (tick-irrelevance (fst pair) t ◇ i) RHS)) H2 in
+ pair , (H3 â—‡)
+
+
+
+ {-
+ let H' = transport
+ (λ i -> ∀ k -> unfold-≾ k (ℕ k0) i (lxF k) ((δ-gl ((δ-gl ^ n) ℧F)) k)) H-lxF in
+ let H'' = transport (λ i -> ∀ k -> _≾'_ k (ℕ k0) (snd (≾'-θ (lxF k) (next ((δ-gl ^ n) ℧F k)) (H' k)) i) (δ k (((δ-gl ^ n) ℧F) k)) ) H' in
+
+ let IH = adequate-err n lxF {!!} in {!!}
+ -}
+ -- H-lxF says that lx ≾-gl (δ-gl ((δ-gl ^ n) ℧F))
+ -- H' says that for all k, (lxF k) ≾' (δ-gl ((δ-gl ^ n) ℧F)) k
+ -- i.e. for all k, (lxF k) ≾' δ k (((δ-gl ^ n) ℧F) k)
+ -- By inversion on ≾', this means that
+ -- for all k, there exists lx~ : ▹k (L℧ k Nat)
+ -- such that (lxF k) ≡ θ lx~, and
+ -- ▸k ( λ t -> lx~ t ≾ (next (((δ-gl ^ n) ℧F) k)) t )
+ -- ▸k ( λ t -> lx~ t ≾ (((δ-gl ^ n) ℧F) k) )
+
+
+
+
+
+
+module AdequacyBisim where
+
+ open Semantics.StrongBisimulation
+ open Semantics.StrongBisimulation.Bisimilarity
+ open Inductive
+ open Bisimilarity.Properties
+
+
+ -- Some properties of the global bisimilarity relation
+ module GlobalBisim (p : Predomain k0) where
+
+ _≈-gl_ : (L℧F ⟨ p ⟩) -> (L℧F ⟨ p ⟩) -> Type
+ _≈-gl_ lx ly = ∀ (k : Clock) -> _≈_ k p (lx k) (ly k)
+
+ ≈-gl-δ-elim : (lx ly : L℧F ⟨ p ⟩) ->
+ _≈-gl_ (δ-gl lx) (δ-gl ly) ->
+ _≈-gl_ lx ly
+ ≈-gl-δ-elim lx ly H = force' H'
+ where
+ H' : ∀ k -> ▹_,_ k (_≈_ k p (lx k) (ly k))
+ H' = transport (λ i → ∀ k -> unfold-≈ k p i (δ k (lx k)) (δ k (ly k))) H
+ -- H : (δ-gl lx) ≈-gl (δ-gl ly)
+ -- i.e. ∀ k . (δ k (lx k)) ≈ (δ k (ly k))
+ -- i.e. ∀ k . (δ k (lx k)) ≈' (δ k (ly k))
+ -- i.e. ∀ k . ▸ (λ t -> (next (lx k) t) ≈ (next (ly k) t))
+ -- i.e. ∀ k . ▸ (λ t -> (lx k) ≈ (ly k))
+ -- i.e. ∀ k . ▹ ((lx k) ≈ (ly k))
+ -- By force we then have: ∀ k . lx k ≈ ly k
+
+
+
+ ≈-gl-δ : (lx ly : L℧F ⟨ p ⟩) ->
+ _≈-gl_ (δ-gl lx) ly -> _≈-gl_ lx ly
+ ≈-gl-δ lx ly H = {!!}
+ where
+ H' : {!!}
+ H' = {!!}
+
+
+ open GlobalBisim (â„• k0)
+
+
+
+
+ adequate-err :
+ (m : Nat) ->
+ (lxF : L℧F Nat) ->
+ (H-lx : _≈-gl_ lxF ((δ-gl ^ m) ℧F)) ->
+ (Σ (Nat) λ n -> ((lxF ≡ (δ-gl ^ n) ℧F)))
+ adequate-err zero lxF H-lx = (fst H3) , clock-ext (snd H4)
+ where
+ H1 : (k : Clock) -> _≈'_ k (ℕ k0) (next (_≈_ k (ℕ k0))) (lxF k) (℧F k)
+ H1 = transport (λ i → ∀ k -> unfold-≈ k (ℕ k0) i (lxF k) (℧F k)) H-lx
+
+ H2 : (k : Clock) -> Σ Nat (λ n → lxF k ≡ (δ k ^ n) ℧)
+ H2 k = ≈-℧ k (ℕ k0) (lxF k) (H1 k)
+
+ H3 : Σ Nat (λ n -> ∀ (k : Clock) -> lxF k ≡ (δ k ^ n) ℧)
+ H3 = ∀clock-Σ nat-clock-irrel H2
+
+ --δ-gl^n : (lxF : L℧F Nat) -> (n : Nat) -> (k : Clock) ->
+ -- ((δ-gl) ^ n) lxF k ≡ ((δ k) ^ n) (lxF k)
+
+ H4 : Σ Nat (λ n -> ∀ (k : Clock) -> lxF k ≡ (δ-gl ^ n) ℧F k)
+ H4 = (fst H3) , (λ k → lxF k ≡⟨ snd H3 k ⟩ (sym (δ-gl^n ℧F (fst H3) k)))
+ -- NTS: lxF k ≡ (δ-gl ^ fst H3) ℧F k
+
+ adequate-err (suc m') lxF H-lx = {!!}
+
diff --git a/formalizations/guarded-cubical/Semantics.agda b/formalizations/guarded-cubical/Semantics/Semantics.agda
similarity index 69%
rename from formalizations/guarded-cubical/Semantics.agda
rename to formalizations/guarded-cubical/Semantics/Semantics.agda
index 02ba34f87b462a90fb6daad3aad50cc1a88f202a..f8b1242c005438640639a19b9b72f9886a9fed11 100644
--- a/formalizations/guarded-cubical/Semantics.agda
+++ b/formalizations/guarded-cubical/Semantics/Semantics.agda
@@ -2,10 +2,14 @@
-- to allow opening this module in other files while there are still holes
{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --lossy-unification #-} -- Makes type-checking *much* faster
+-- (Otherwise, finding the implicit arguments for the definitions in EP-arrow
+-- takes a long time)
+-- See https://agda.readthedocs.io/en/v2.6.3/language/lossy-unification.html
-open import Later
+open import Common.Later
-module Semantics (k : Clock) where
+module Semantics.Semantics (k : Clock) where
open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat renaming (â„• to Nat) hiding (_^_)
@@ -22,22 +26,26 @@ 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
+open import Common.Common
+
+open import Semantics.StrongBisimulation k
+open import Syntax.GradualSTLC
+-- open import SyntacticTermPrecision k
+open import Common.Lemmas k
+open import Common.MonFuns k
private
variable
l : Level
A B : Set l
+ â„“ â„“' : Level
private
▹_ : Set l → Set l
â–¹_ A = â–¹_,_ k A
-open ð•ƒ
+open LiftPredomain using (𕃠; ord-η-monotone ; ord-δ-monotone ; ord-bot )
+
-- Denotations of Types
@@ -114,40 +122,46 @@ DynP-rel : ∀ 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) ⟩) d1 i) -- can also just use (sym unfold-⟨DynP⟩) and remove the λ j
(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)
- )
+DynP'-rel : ∀ d1 d2 ->
+ rel DynP d1 d2 ->
+ rel (DynP' (next 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) -- can also just use unfold-⟨DynP⟩ and remove the λ j
+ (transport-filler (λ j -> ⟨ unfold-DynP j ⟩) d2 i))
d1≤d2
--}
-
-------------------------------------
-- *** Embedding-projection pairs ***
+-- open MonRel
+-- open MonFun
+-- open LiftRelation
-record EP (A B : Predomain) : Set where
+record EP (A B : Predomain) : Type (â„“-suc â„“-zero) where
+ open LiftPredomain using () renaming (_≾_ to _≾hom_)
+ open LiftRelation
+ open MonRel
+ open MonFun
field
emb : MonFun A B
proj : MonFun B (𕃠A)
wait-l-e : ⟨ A ==> A ⟩
- wait-l-p : ⟨ 𕃠A ==> 𕃠A ⟩
+ wait-l-p : ⟨ A ==> 𕃠A ⟩
wait-r-e : ⟨ B ==> B ⟩
- wait-r-p : ⟨ 𕃠B ==> 𕃠B ⟩
+ wait-r-p : ⟨ B ==> 𕃠B ⟩
+ R : MonRel A B
+
+ upR : fun-order-het A A A B (rel A) (MonRel.R R) (wait-l-e .f) (emb .f)
+ upL : fun-order-het A B B B (MonRel.R R) (rel B) (emb .f) (wait-r-e .f)
+
+ dnL : fun-order-het B B (𕃠A) (𕃠B) (rel B) (_≾_ A B (MonRel.R R)) (proj .f) (wait-r-p .f)
+ dnR : fun-order-het A B (𕃠A) (𕃠A) (MonRel.R R) (_≾hom_ A) (wait-l-p .f) (proj .f)
-- Identity E-P pair
@@ -155,11 +169,18 @@ record EP (A B : Predomain) : Set where
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 };
+ proj = mCompU Δ mRet ; -- record { f = ret ; isMon = ord-η-monotone A };
wait-l-e = Id;
- wait-l-p = Id;
+ wait-l-p = mCompU Δ mRet;
wait-r-e = Id;
- wait-r-p = Id}
+ wait-r-p = mCompU Δ mRet;
+ R = predomain-monrel A;
+
+ upR = λ a a' a≤a' → a≤a';
+ upL = λ a a' a≤a' → a≤a';
+
+ dnL = λ a a' a≤a' → ord-δ-monotone A (ord-η-monotone A a≤a') ; -- (ord-η-monotone A a≤a');
+ dnR = λ a a' a≤a' → ord-δ-monotone A (ord-η-monotone A a≤a') } -- ord-η-monotone A a≤a'}
@@ -192,101 +213,226 @@ p-nat = {!!} -- S DynP (K DynP p-nat') (mTransport unfold-DynP)
-- mTransportDomain (sym unfold-DynP) p-nat'
+-- TODO add in delays for the projection and wait-p functions
EP-nat : EP â„• DynP
EP-nat = record {
emb = e-nat;
proj = p-nat;
wait-l-e = Id;
- wait-l-p = Id;
+ wait-l-p = mRet;
wait-r-e = Id;
- wait-r-p = Id}
-
-
--- E-P Pair for monotone functions Dyn to L℧ Dyn
+ wait-r-p = mRet;
+ R = record {
+ R = λ n d -> R' n (DynP-to-DynP' d) ;
+ isAntitone = λ {n} {n'} {d} n≤d n'≤n → {!!} ;
+ isMonotone = λ {n} {d} {d'} n≤d d≤d' ->
+ isMonotone' n≤d (DynP'-rel d d' d≤d') } ;
-e-fun : MonFun (DynP ==> (𕃠DynP)) DynP
-e-fun = record { f = e-fun-f ; isMon = e-fun-mon }
- where
- e-fun-f : ⟨ DynP ==> (𕃠DynP) ⟩ -> ⟨ DynP ⟩
- e-fun-f f = DynP'-to-DynP (fun (next f))
+ upR = λ n n' n≤n' → {!!};
+ upL = λ n d n≤d → {!!};
- e-fun-mon :
- {f1 f2 : ⟨ DynP ==> (𕃠DynP) ⟩} ->
- rel (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 → {!!})
+ dnL = λ d d' d≤d' → {!!};
+ dnR = λ n d n≤d → {!!}
+ }
+ where
+ R' : ⟨ ℕ ⟩ -> ⟨ DynP' (next DynP) ⟩ -> Type
+ R' n (nat n') = n ≡ n'
+ R' n (fun _) = ⊥
-p-fun : MonFun DynP (𕃠(DynP ==> (𕃠DynP)))
-p-fun = record { f = p-fun-f ; isMon = {!!} }
- where
+ R : ⟨ ℕ ⟩ -> ⟨ DynP ⟩ -> Type
+ R n d = R' n (DynP-to-DynP' d)
- p-fun-f' : ⟨ DynP' (next DynP) ⟩ -> ⟨ 𕃠(DynP ==> (𕃠DynP)) ⟩
- p-fun-f' (nat n) = ℧
- p-fun-f' (fun f) = θ (λ t → η (f t))
- -- f : ▸ (λ t → MonFun (next DynP t) (𕃠(next DynP t)))
+ isMonotone' : {n : ⟨ ℕ ⟩} {d d' : ⟨ DynP' (next DynP) ⟩} →
+ R' n d →
+ rel (DynP' (next DynP)) d d' →
+ R' n d'
+ isMonotone' {n} {nat n1} {nat n2} n≡n1 n1≡n2 =
+ n ≡⟨ n≡n1 ⟩ n1 ≡⟨ n1≡n2 ⟩ n2 ∎
- p-fun-f : ⟨ DynP ⟩ -> ⟨ 𕃠(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
+-- E-P Pair for monotone functions Dyn to L℧ Dyn
+-- This is parameterized by the waiting information of the EP-pair below it,
+-- in order for the projection/wait left function to remain in sync with the
+-- child's wait-right function (required for composition to be defined)
+EP-fun : EP (DynP ==> (𕃠DynP)) DynP
EP-fun = record {
emb = e-fun;
proj = p-fun;
- wait-l-e = Id;
- wait-l-p = Δ;
+
+ -- This is equal to the identity!
+ wait-l-e = Curry (
+ (mMap' (With2nd (EP.wait-l-e (EP-id DynP)))) ∘m
+ (Uncurry mExt) ∘m
+ (With2nd (EP.wait-l-p (EP-id DynP))) ∘m
+ π2
+ );
+
+ wait-l-p = mRet' (DynP ==> 𕃠DynP) (Curry (
+ With2nd (U mExt (EP.wait-l-p (EP-id DynP))) ∘m
+ App ∘m
+ With2nd (EP.wait-l-e (EP-id DynP)))) ;
+
wait-r-e = Id;
- wait-r-p = Δ}
+
+ wait-r-p = record {
+ f = λ d → mapL DynP'-to-DynP (wait-r-p-fun (DynP-to-DynP' d)) ;
+ isMon = {!!} } ;
+
+ R = R ;
+
+ upR = λ n n' n≤n' → {!!};
+ upL = λ n d n≤d → {!!};
+
+ dnL = λ d d' d≤d' → {!!};
+ dnR = λ n d n≤d → {!!}
+
+
+ }
+ where
+ e-fun : MonFun (DynP ==> (𕃠DynP)) DynP
+ e-fun = record { f = e-fun-f ; isMon = e-fun-mon }
+ where
+ e-fun-f : ⟨ DynP ==> (𕃠DynP) ⟩ -> ⟨ DynP ⟩
+ e-fun-f f = DynP'-to-DynP (fun (next f))
+
+ e-fun-mon :
+ {f1 f2 : ⟨ DynP ==> (𕃠DynP) ⟩} ->
+ rel (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 (𕃠(DynP ==> (𕃠DynP)))
+ p-fun = record { f = p-fun-f ; isMon = {!!} }
+ where
+
+ p-fun-f' : ⟨ DynP' (next DynP) ⟩ -> ⟨ 𕃠(DynP ==> (𕃠DynP)) ⟩
+ p-fun-f' (nat n) = ℧
+ p-fun-f' (fun f) = θ (λ t → η (f t))
+
+ -- f : ▸ (λ t → MonFun (next DynP t) (𕃠(next DynP t)))
+
+ p-fun-f : ⟨ DynP ⟩ -> ⟨ 𕃠(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)
+
+ wait-l-p-fun : ⟨ ( (DynP' (next DynP)) ==> 𕃠(DynP' (next DynP)) ) ⟩ ->
+ ⟨ 𕃠( (DynP' (next DynP)) ==> 𕃠(DynP' (next DynP)) ) ⟩
+ wait-l-p-fun d = δ (η d) -- is this correct?
+
+ wait-r-p-fun : ⟨ DynP' (next DynP) ⟩ -> ⟨ 𕃠(DynP' (next DynP)) ⟩
+ wait-r-p-fun (nat n) = η (nat n)
+ wait-r-p-fun (fun f) = θ (next (η (fun f)))
+
+
+ {-
+ R' : ⟨ DynP ==> 𕃠DynP ⟩ -> ⟨ DynP' (next DynP) ⟩ -> Type
+ R' f (nat n) = ⊥
+ R' f (fun f') = ▸ λ t ->
+ fun-order-het DynP DynP (𕃠DynP) (𕃠DynP)
+ (rel DynP)
+ (LiftRelation._≾_ DynP DynP (rel DynP))
+ (MonFun.f f) (MonFun.f (f' t))
+ -}
+
+ R' : ⟨ DynP ==> 𕃠DynP ⟩ -> ⟨ DynP' (next DynP) ⟩ -> Type
+ R' f (nat n) = ⊥
+ R' f (fun f') = ▸ λ t ->
+ mon-fun-order DynP (𕃠DynP) f (f' t)
+
+ R : MonRel (DynP ==> 𕃠DynP) DynP
+ R = record {
+ R = λ f d → R' f (DynP-to-DynP' d) ;
+ isAntitone = λ {f} {f'} {d} f≤d f'≤f → {!!} ;
+ isMonotone = λ {f} {d} {d'} f≤d d≤d' -> monotone' f≤d (DynP'-rel d d' d≤d') }
+
+ where
+ monotone' : {f : ⟨ DynP ==> 𕃠DynP ⟩} {d d' : ⟨ DynP' (next DynP) ⟩} →
+ R' f d →
+ rel (DynP' (next DynP)) d d' ->
+ R' f d'
+ monotone' {f} {fun f~} {fun g~} f≤d d≤d' =
+ λ t → mon-fun-order-trans f (f~ t) (g~ t) (f≤d t) (d≤d' t)
-- Composing EP pairs
+-- We can compose EP pairs provided that the "middle" wait functions
+-- satisfy a "coherence" condition.
module EPComp
{A B C : Predomain}
- (epAB : EP A B)
- (epBC : EP B C) where
+ (d' : EP B C)
+ (d : EP A B)
+ (⊑-wait-rl-e : rel (B ==> B) (EP.wait-r-e d) (EP.wait-l-e d'))
+ (⊑-wait-rl-p : rel (B ==> 𕃠B) (EP.wait-r-p d) (EP.wait-l-p d'))
+ where
open EP
open MonFun
+ open MonRel
comp-emb : ⟨ A ==> C ⟩
- comp-emb = mCompU (emb epBC) (emb epAB)
- -- A ! K A (emb epBC) <*> (emb epAB) -- mComp (emb epBC) (emb epAB)
+ comp-emb = mCompU (emb d') (emb d)
comp-proj : ⟨ C ==> 𕃠A ⟩
- comp-proj = Bind C (proj epBC) (mCompU (proj epAB) π2)
- --C ! (mExt' C (K C (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))
+ comp-proj = Bind C (proj d') (mCompU (proj d) π2)
+
EP-comp : EP A C
EP-comp = record {
emb = comp-emb;
proj = comp-proj;
- wait-l-e = wait-l-e epAB;
- wait-l-p = wait-l-p epAB;
- wait-r-e = wait-r-e epBC;
- wait-r-p = wait-r-p epBC}
+
+ wait-l-e = mCompU (wait-l-e d) (wait-l-e d);
+ wait-l-p = mCompU (mExtU (wait-l-p d)) (wait-l-p d);
+ wait-r-e = mCompU (wait-r-e d') (wait-r-e d');
+ wait-r-p = mCompU (mExtU (wait-r-p d')) (wait-r-p d');
+
+ R = CompMonRel (R d') (R d);
+
+ upR = λ a a' a≤a' →
+ emb d $ (wait-l-e d $ a) ,
+ upR d (wait-l-e d $ a) (wait-l-e d $ a) (reflexive A _) ,
+ isAntitone (R d')
+ (upR d' (emb d $ a') (emb d $ a') (reflexive B _))
+ (transitive B
+ (emb d $ (wait-l-e d $ a))
+ (wait-r-e d $ (emb d $ a'))
+ (wait-l-e d' $ (emb d $ a'))
+ (upL d _ _ (upR d _ _ a≤a'))
+ (⊑-wait-rl-e _ _ (reflexive B _)));
+
+ upL = λ a c (b , a≤b , b≤c) → {!!};
+
+ dnL = λ c c' c≤c' → {!!};
+ dnR = λ a c a≤c → {!!} }
+
-- Lifting EP pairs to ð•ƒ
EP-lift : {A B : Predomain} -> EP A B -> EP (𕃠A) (𕃠B)
-EP-lift epAB =
+EP-lift {A} {B} d =
record {
- emb = U mMap (EP.emb epAB);
- proj = U mMap (EP.proj epAB);
- wait-l-e = U mMap (EP.wait-l-e epAB);
- wait-l-p = U mMap (EP.wait-l-p epAB);
- wait-r-e = U mMap (EP.wait-r-e epAB);
- wait-r-p = U mMap (EP.wait-r-p epAB) }
+ emb = U mMap (EP.emb d);
+ proj = U mMap (EP.proj d);
+ wait-l-e = U mMap (EP.wait-l-e d);
+ wait-l-p = U mMap (EP.wait-l-p d);
+ wait-r-e = U mMap (EP.wait-r-e d);
+ wait-r-p = U mMap (EP.wait-r-p d);
+ R = LiftRelMon.R A B (EP.R d);
+
+ upR = λ la la' la≤la' → mapL-monotone-het (rel A) (MonRel.R (EP.R d)) (MonFun.f (EP.wait-l-e d)) (MonFun.f (EP.emb d)) (EP.upR d) la la' la≤la' ;
+ upL = λ la lb la≤lb → mapL-monotone-het (MonRel.R (EP.R d)) (rel B) _ _ (EP.upL d) la lb la≤lb ;
+
+ dnL = {!!};
+ dnR = {!!}}
+ where open MonFun
+ open EP
-- Lifting EP pairs to functions
@@ -302,53 +448,52 @@ module EPArrow
p-arrow : ⟨ (A' ==> (𕃠B')) ==> (𕃠(A ==> (𕃠B))) ⟩
p-arrow = mFunProj A A' B B' (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 (A ==> (𕃠B)) (A' ==> (𕃠B'))
-EP-arrow epAA' epBB' = record {
+EP-arrow {A} {A'} {B} {B'} epAA' epBB' = record {
emb = e-arrow;
proj = p-arrow;
+
wait-l-e = Curry (
(mMap' (With2nd (EP.wait-l-e epBB'))) ∘m
(Uncurry mExt) ∘m
(With2nd (EP.wait-l-p epAA')) ∘m
- (mRet' _ π2)
+ π2
) ;
- wait-l-p = U mMap (Curry (
- With2nd (EP.wait-l-p epBB') ∘m
+ wait-l-p = mRet' (A ==> 𕃠B) (Curry (
+ With2nd (U mExt (EP.wait-l-p epBB')) ∘m
App ∘m
- With2nd (EP.wait-l-e epAA')
- )) ;
+ With2nd (EP.wait-l-e epAA'))) ;
wait-r-e = Curry (
mMap' (With2nd (EP.wait-r-e epBB')) ∘m
((Uncurry mExt) ∘m
(With2nd (EP.wait-r-p epAA') ∘m
- (mRet' _ π2)))) ;
- -- or : wait-r-e = Curry (mMap' (With2nd (EP.wait-r-e epBB')) ∘m ((Uncurry mExt) ∘m (With2nd (EP.wait-r-p epAA') ∘m (With2nd mRet)))) ;
-
+ π2))) ;
- wait-r-p = U mMap (Curry (
- With2nd (EP.wait-r-p epBB') ∘m
+ wait-r-p = mRet' (A' ==> 𕃠B') (Curry (
+ With2nd (U mExt (EP.wait-r-p epBB')) ∘m
App ∘m
- With2nd (EP.wait-r-e epAA')
- ))
+ With2nd (EP.wait-r-e epAA'))) ;
+
+ R = FunRel (EP.R epAA') {!!} ;
+
+ upR = λ p p' x p₠p'' x₠→ {!!} ;
+ upL = {!!} ;
+ dnL = {!!} ;
+ dnR = {!!}
}
where open EPArrow epAA' epBB'
+{-
-------------------------------------------
@@ -720,17 +865,6 @@ UpR {Ai => Ao} M1 M2 (inj-arrow (cin' => cout')) dyn M1⊑M2 = {!!}
-
-
-
-
-
-
-
-
-
-
-
@@ -822,6 +956,4 @@ eta = {!!}
-}
-{-
-
-}
diff --git a/formalizations/guarded-cubical/StrongBisimulation.agda b/formalizations/guarded-cubical/Semantics/StrongBisimulation.agda
similarity index 80%
rename from formalizations/guarded-cubical/StrongBisimulation.agda
rename to formalizations/guarded-cubical/Semantics/StrongBisimulation.agda
index 895c8cbe81358e7de26aa75b8b17a7fc640749f1..0e4b10b004a8c884374b373bbc4b6def7dd2e392 100644
--- a/formalizations/guarded-cubical/StrongBisimulation.agda
+++ b/formalizations/guarded-cubical/Semantics/StrongBisimulation.agda
@@ -3,9 +3,9 @@
-- to allow opening this module in other files while there are still holes
{-# OPTIONS --allow-unsolved-metas #-}
-open import Later
+open import Common.Later
-module StrongBisimulation(k : Clock) where
+module Semantics.StrongBisimulation(k : Clock) where
open import Cubical.Relation.Binary
open import Cubical.Relation.Binary.Poset
@@ -30,6 +30,8 @@ open import Cubical.Data.Unit.Properties
open import Agda.Primitive
+open import Common.Common
+
private
variable
l : Level
@@ -40,19 +42,44 @@ private
â–¹_ 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)
+
+Predomain' : {â„“ â„“' : Level} -> Type (â„“-max (â„“-suc â„“) (â„“-suc â„“'))
+Predomain' {â„“} {â„“'} = Poset â„“ â„“'
+
+-- The relation associated to a predomain d
+rel' : (d : Predomain') -> (⟨ d ⟩ -> ⟨ d ⟩ -> Type)
+rel' d = PosetStr._≤_ (d .snd)
+
+reflexive' : (d : Predomain') -> (x : ⟨ d ⟩) -> (rel' d x x)
+reflexive' d x = IsPoset.is-refl (PosetStr.isPoset (str d)) x
+
+transitive' : (d : Predomain') -> (x y z : ⟨ d ⟩) ->
+ rel' d x y -> rel' d y z -> rel' d x z
+transitive' d x y z x≤y y≤z =
+ IsPoset.is-trans (PosetStr.isPoset (str d)) x y z x≤y y≤z
+
+test : Predomain' -> Predomain' -> Predomain'
+test A B =
+ (Path Predomain' A B) ,
+ posetstr (λ p1 p2 → rel' A {!p1 i0!} {!!} × {!!})
+ (isposet {!!} {!!} (λ a → {!!}) {!!} {!!})
+
+
+
+
+
+
+
-- Define predomains as posets
+
Predomain : Setâ‚
Predomain = Poset â„“-zero â„“-zero
+
-- The relation associated to a predomain d
rel : (d : Predomain) -> (⟨ d ⟩ -> ⟨ d ⟩ -> Type)
rel d = PosetStr._≤_ (d .snd)
@@ -83,6 +110,7 @@ record MonFun (X Y : Predomain) : Set where
-- Specialize to the case of monotone functions and fill in the proof
-- later
+
-- Monotone relations between predomains X and Y
-- (antitone in X, monotone in Y).
record MonRel {â„“' : Level} (X Y : Predomain) : Type (â„“-suc â„“') where
@@ -102,6 +130,34 @@ predomain-monrel X = record {
isMonotone = λ {x} {y} {y'} x≤y y≤y' -> transitive X x y y' x≤y y≤y' }
+compRel : {X Y Z : Type} ->
+ (R1 : Y -> Z -> Type â„“) ->
+ (R2 : X -> Y -> Type â„“) ->
+ (X -> Z -> Type â„“)
+compRel {ℓ} {X} {Y} {Z} R1 R2 x z = Σ[ y ∈ Y ] R2 x y × R1 y z
+
+CompMonRel : {X Y Z : Predomain} ->
+ MonRel {â„“} Y Z ->
+ MonRel {â„“} X Y ->
+ MonRel {â„“} X Z
+CompMonRel {â„“} {X} {Y} {Z} R1 R2 = record {
+ R = compRel (MonRel.R R1) (MonRel.R R2) ;
+ isAntitone = antitone ;
+ isMonotone = {!!} }
+ where
+ antitone : {x x' : ⟨ X ⟩} {z : ⟨ Z ⟩} ->
+ compRel (MonRel.R R1) (MonRel.R R2) x z ->
+ rel X x' x ->
+ compRel (MonRel.R R1) (MonRel.R R2) x' z
+ antitone (y , xR2y , yR1z) x'≤x = y , (MonRel.isAntitone R2 xR2y x'≤x) , yR1z
+
+ monotone : {x : ⟨ X ⟩} {z z' : ⟨ Z ⟩} ->
+ compRel (MonRel.R R1) (MonRel.R R2) x z ->
+ rel Z z z' ->
+ compRel (MonRel.R R1) (MonRel.R R2) x z'
+ monotone (y , xR2y , yR1z) z≤z' = y , xR2y , (MonRel.isMonotone R1 yR1z z≤z')
+
+
{-
record IsMonFun {X Y : Predomain} (f : ⟨ X ⟩ → ⟨ Y ⟩) : Type (ℓ-max ℓ ℓ') where
no-eta-equality
@@ -408,6 +464,8 @@ UnitP = flat (Unit , isSetUnit)
-- Predomains from arrows (need to ensure monotonicity)
+
+
-- Ordering on functions between predomains. This does not require that the
-- functions are monotone.
fun-order-het : (P1 P1' P2 P2' : Predomain) ->
@@ -420,6 +478,8 @@ fun-order-het P1 P1' P2 P2' rel-P1P1' rel-P2P2' fP1P2 fP1'P2' =
rel-P2P2' (fP1P2 p) (fP1'P2' p')
+
+
-- TODO can define this in terms of fun-order-het
fun-order : (P1 P2 : Predomain) -> (⟨ P1 ⟩ -> ⟨ P2 ⟩) -> (⟨ P1 ⟩ -> ⟨ P2 ⟩) -> Type ℓ-zero
fun-order P1 P2 f1 f2 =
@@ -504,17 +564,6 @@ arr' P1 P2 =
_≤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
@@ -522,6 +571,26 @@ A ==> B = arr' A B
infixr 20 _==>_
+
+-- TODO show that this is a monotone relation
+
+-- TODO define version where the arguments are all monotone relations
+-- instead of arbitrary relations
+
+FunRel : {A A' B B' : Predomain} ->
+ MonRel {â„“-zero} A A' ->
+ MonRel {â„“-zero} B B' ->
+ MonRel {â„“-zero} (A ==> B) (A' ==> B')
+FunRel {A} {A'} {B} {B'} RAA' RBB' =
+ record {
+ R = λ f f' → fun-order-het A A' B B'
+ (MonRel.R RAA') (MonRel.R RBB')
+ (MonFun.f f) (MonFun.f f') ;
+ isAntitone = {!!} ;
+ isMonotone = λ {f} {f'} {g'} f≤f' f'≤g' a a' a≤a' →
+ MonRel.isMonotone RBB' (f≤f' a a' a≤a') {!!} } -- (f'≤g' a' a' (reflexive A' a')) }
+
+
arr : Predomain -> ErrorDomain -> ErrorDomain
arr dom cod =
record {
@@ -538,9 +607,14 @@ arr dom cod =
const-err-bot : (f : ⟨ arr' dom (𕌠cod) ⟩) -> rel (arr' dom (𕌠cod)) const-err f
const-err-bot f = λ x y x≤y → ErrorDomain.℧⊥ cod (MonFun.f f y)
-
+
+-- Delay function
+δ : {X : Type} -> L℧ X -> L℧ X
+δ = θ ∘ next
+ where open L℧
+
-- Lifting a heterogeneous relation between A and B to a
@@ -549,99 +623,57 @@ arr dom cod =
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
-
-
-module LiftRelMonotone
- (A B C : Predomain)
- (ordAB : ⟨ A ⟩ -> ⟨ B ⟩ -> Type)
- (ordBC : ⟨ B ⟩ -> ⟨ C ⟩ -> Type)
+ (RAB : ⟨ A ⟩ -> ⟨ B ⟩ -> 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)
+ module Inductive
+ (rec : ▹ ( L℧ ⟨ A ⟩ → L℧ ⟨ B ⟩ → Type)) where
- ordAC : ⟨ A ⟩ -> ⟨ C ⟩ -> Type
- ordAC a c = Σ ⟨ B ⟩ λ b → ordAB a b × ordBC b c
+ _≾'_ : L℧ ⟨ A ⟩ → L℧ ⟨ B ⟩ → Type
+ (η a) ≾' (η b) = RAB a b
+ ℧ ≾' lb = Unit
+ (θ la~) ≾' (θ lb~) = ▸ (λ t → rec t (la~ t) (lb~ t))
+ _ ≾' _ = ⊥
- open LiftRelation A C ordAC renaming (ord to ordLALC; unfold-ord to unfold-ordLALC)
+ _≾_ : L℧ ⟨ A ⟩ -> L℧ ⟨ B ⟩ -> Type
+ _≾_ = fix _≾'_
+ where open Inductive
+ unfold-≾ : _≾_ ≡ Inductive._≾'_ (next _≾_)
+ unfold-≾ = fix-eq Inductive._≾'_
- {-
- 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
- -}
+ module Properties where
+ open Inductive (next _≾_)
+ ≾->≾' : {la : L℧ ⟨ A ⟩} {lb : L℧ ⟨ B ⟩} ->
+ la ≾ lb -> la ≾' lb
+ ≾->≾' {la} {lb} la≾lb = transport (λ i → unfold-≾ i la lb) la≾lb
- 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 = {!!}
-
+ ≾'->≾ : {la : L℧ ⟨ A ⟩} {lb : L℧ ⟨ B ⟩} ->
+ la ≾' lb -> la ≾ lb
+ ≾'->≾ {la} {lb} la≾'lb = transport (sym (λ i → unfold-≾ i la lb)) la≾'lb
- {- 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)
- -}
-
+ ord-η-monotone : {a : ⟨ A ⟩} -> {b : ⟨ B ⟩} -> RAB a b -> (η a) ≾ (η b)
+ ord-η-monotone {a} {b} a≤b = transport (sym (λ i → unfold-≾ i (η a) (η b))) a≤b
--- Delay function
-δ : {X : Type} -> L℧ X -> L℧ X
-δ = θ ∘ next
- where open L℧
+ ord-bot : (lb : L℧ ⟨ B ⟩) -> ℧ ≾ lb
+ ord-bot lb = transport (sym (λ i → unfold-≾ i ℧ lb)) tt
-- Predomain to lift predomain
-module 𕃠(p : Predomain) where
+module LiftPredomain (p : Predomain) where
module X = PosetStr (p .snd)
open X using (_≤_)
-- _≤_ = X._≤_
-
+ {-
ord' : ▹ ( L℧ ⟨ p ⟩ → L℧ ⟨ p ⟩ → Type) ->
L℧ ⟨ p ⟩ → L℧ ⟨ p ⟩ → Type
ord' _ ℧ _ = Unit
@@ -653,54 +685,86 @@ module 𕃠(p : Predomain) where
ord : L℧ ⟨ p ⟩ → L℧ ⟨ p ⟩ → Type
ord = fix ord'
+ -}
+
+ -- _≾_ : L℧ ⟨ p ⟩ -> L℧ ⟨ p ⟩ -> Type
+ -- _≾_ = LiftRelation._≾_ p p (_≤_)
- _≾_ : L℧ ⟨ p ⟩ -> L℧ ⟨ p ⟩ -> Type
- _≾_ = ord
+ -- unfold-ord : ord ≡ ord' (next ord)
+ -- unfold-ord = fix-eq ord'
- unfold-ord : ord ≡ ord' (next ord)
- unfold-ord = fix-eq ord'
+ {-
+ ≈->≈' : {lx ly : L℧ ⟨ d ⟩} ->
+ lx ≈ ly -> lx ≈' ly
+ ≈->≈' {lx} {ly} lx≈ly = transport (λ i → unfold-≈ i lx ly) lx≈ly
+
+ ≈'->≈ : {lx ly : L℧ ⟨ d ⟩} ->
+ lx ≈' ly -> lx ≈ ly
+ ≈'->≈ {lx} {ly} lx≈'ly = transport (sym (λ i → unfold-≈ i lx ly)) lx≈'ly
+ -}
- 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-δ-monotone : {lx ly : L℧ ⟨ p ⟩} -> ord lx ly -> ord (δ lx) (δ ly)
- ord-δ-monotone = {!!}
+ -- Open the more general definitions from the heterogeneous
+ -- lifting module, specializing the types for the current
+ -- (homogeneous) situation, and re-export the definitions for
+ -- clients of this module to use at these specialized types.
+ open LiftRelation p p _≤_ public
+
+ -- could also say: open LiftRelation.Inductive p p _≤_ (next _≾_)
+ open Inductive (next _≾_) public
+ open Properties public
+
+ {-
+ ord-η-monotone : {x y : ⟨ p ⟩} -> x ≤ y -> (η x) ≾ (η y)
+ ord-η-monotone {x} {y} x≤y = transport (sym λ i → unfold-≾ i (η x) (η y)) x≤y
+ -}
+
+ -- TODO move to heterogeneous lifting module
+ ord-δ-monotone : {lx ly : L℧ ⟨ p ⟩} -> lx ≾ ly -> (δ lx) ≾ (δ ly)
+ ord-δ-monotone {lx} {ly} lx≤ly =
+ transport (sym (λ i → unfold-≾ i (δ lx) (δ ly))) (ord-δ-monotone' lx≤ly)
+ where
+ ord-δ-monotone' : {lx ly : L℧ ⟨ p ⟩} ->
+ lx ≾ ly ->
+ Inductive._≾'_ (next _≾_) (δ lx) (δ ly)
+ ord-δ-monotone' {lx} {ly} lx≤ly = λ t → lx≤ly
- ord-bot : (lx : L℧ ⟨ p ⟩) -> ord ℧ lx
- ord-bot lx = transport (sym λ i → unfold-ord i ℧ lx) tt
+ {-
+ ord-bot : (lx : L℧ ⟨ p ⟩) -> ℧ ≾ lx
+ ord-bot lx = transport (sym λ i → unfold-≾ i ℧ lx) tt
+ -}
-- lift-ord : (A -> A -> Type) -> (L℧ A -> L℧ A -> Type)
- ord-refl-ind : ▹ ((a : L℧ ⟨ p ⟩) -> ord a a) ->
- (a : L℧ ⟨ p ⟩) -> ord a a
+ ord-refl-ind : ▹ ((a : L℧ ⟨ p ⟩) -> a ≾ a) ->
+ (a : L℧ ⟨ p ⟩) -> a ≾ a
ord-refl-ind IH (η x) =
- transport (sym (λ i -> fix-eq ord' i (η x) (η x))) (IsPoset.is-refl X.isPoset x)
+ transport (sym (λ i -> unfold-≾ i (η x) (η x))) (IsPoset.is-refl X.isPoset x)
ord-refl-ind IH ℧ =
- transport (sym (λ i -> fix-eq ord' i ℧ ℧)) tt
+ transport (sym (λ i -> unfold-≾ i ℧ ℧)) tt
ord-refl-ind IH (θ x) =
- transport (sym (λ i -> fix-eq ord' i (θ x) (θ x))) λ t → IH t (x t)
+ transport (sym (λ i -> unfold-≾ i (θ x) (θ x))) λ t → IH t (x t)
- ord-refl : (a : L℧ ⟨ p ⟩) -> ord a a
+ ord-refl : (a : L℧ ⟨ p ⟩) -> a ≾ a
ord-refl = fix ord-refl-ind
-
𕃠: Predomain
𕃠=
(L℧ ⟨ p ⟩) ,
- (posetstr ord (isposet {!!} {!!} ord-refl ord-trans {!!}))
+ (posetstr _≾_ (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 ->
+ b ≾' c ->
+ a ≾' c) ->
(a b c : L℧ ⟨ p ⟩) ->
- ord' (next ord) a b ->
- ord' (next ord) b c ->
- ord' (next ord) a c
+ a ≾' b ->
+ b ≾' c ->
+ 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 ∎
@@ -711,17 +775,67 @@ module 𕃠(p : Predomain) where
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))
+ λ t -> transport (sym λ i → unfold-≾ 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)))
+ (transport (λ i -> unfold-≾ i (lx~ t) (ly~ t)) (ord-ab t))
+ (transport (λ i -> unfold-≾ 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 : (a b c : L℧ ⟨ p ⟩) -> a ≾ b -> b ≾ c -> 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) →
+ unfold-≾ i a b → unfold-≾ i b c → unfold-≾ 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)
+ unfold-≾ i a b → unfold-≾ i b c → unfold-≾ i a c))) ord-trans-ind)
+
+
+
+
+module LiftRelMon
+ (A B : Predomain)
+ (RAB : MonRel A B) where
+
+ -- Bring the heterogeneous relation between 𕃠A and 𕃠B into scope
+ open LiftRelation A B (MonRel.R RAB)
+ using (_≾_ ; module Inductive ; module Properties) -- brings _≾_ into scope
+ open Inductive (next _≾_) -- brings _≾'_ into scope
+ open Properties -- brings conversion between _≾_ and _≾'_ into scope
+
+ -- Bring the homogeneous lifted relations on A and B into scope
+ -- open LiftPredomain renaming (_≾_ to _≾h_ ; _≾'_ to _≾h'_)
+ open LiftPredomain using (ð•ƒ)
+
+ _≾LA_ = LiftPredomain._≾_ A
+ _≾LB_ = LiftPredomain._≾_ B
+ -- Could also say:
+ -- open LiftPredomain A using () renaming (_≾_ to _≾LA_)
+
+ _≾'LA_ = LiftPredomain._≾'_ A
+ _≾'LB_ = LiftPredomain._≾'_ B
+
+
+ R : MonRel (𕃠A) (𕃠B)
+ R = record {
+ R = _≾_ ;
+ isAntitone = {!!} ;
+ isMonotone = {!!} }
+
+ antitone' :
+ ▹ ({la la' : L℧ ⟨ A ⟩} -> {lb : L℧ ⟨ B ⟩} ->
+ la ≾' lb -> la' ≾'LA la -> la' ≾' lb) ->
+ {la la' : L℧ ⟨ A ⟩} -> {lb : L℧ ⟨ B ⟩} ->
+ la ≾' lb -> la' ≾'LA la -> la' ≾' lb
+ antitone' IH {η a2} {η a1} {η a3} la≤lb la'≤la =
+ MonRel.isAntitone RAB la≤lb la'≤la
+ antitone' IH {la} {℧} {lb} la≤lb la'≤la = tt
+ antitone' IH {θ la2~} {θ la1~} {θ lb~} la≤lb la'≤la =
+ λ t → ≾'->≾ (IH t (≾->≾' (la≤lb t)) ({!!} ))
+
+ monotone : {!!}
+ monotone = {!!}
+
+ -- isAntitone : ∀ {x x' y} -> R x y -> x' ≤X x -> R x' y
+ -- isMonotone : ∀ {x y y'} -> R x y -> y ≤Y y' -> R x y'
+
-- Predomain to lift Error Domain
@@ -733,7 +847,10 @@ module 𕃠(p : Predomain) where
where
-- module X = PosetStr (X .snd)
-- open Relation X
- open ð•ƒ
+ open LiftPredomain
+
+
+
@@ -944,7 +1061,18 @@ module Bisimilarity (d : Predomain) where
lx ≈' ly -> lx ≈ ly
≈'->≈ {lx} {ly} lx≈'ly = transport (sym (λ i → unfold-≈ i lx ly)) lx≈'ly
-
+ {-
+ ≈-℧ : (lx : L℧ ⟨ d ⟩) ->
+ lx ≈' ℧ -> (lx ≡ ℧) ⊎ (Σ Nat λ n -> lx ≡ (δ ^ n) ℧)
+ ≈-℧ ℧ H = inl refl
+ ≈-℧ (θ x) H = inr H
+ -}
+
+ -- Simpler version of the above:
+ ≈-℧ : (lx : L℧ ⟨ d ⟩) ->
+ lx ≈' ℧ -> (Σ Nat λ n -> lx ≡ (δ ^ n) ℧)
+ ≈-℧ ℧ H = zero , refl
+ ≈-℧ (θ x) H = H
{-
bisim-θ : (lx~ ly~ : L℧ ⟨ d ⟩) ->
@@ -1027,7 +1155,9 @@ module Bisimilarity (d : Predomain) where
-- which holds by IH.
x≈δx : (lx : L℧ ⟨ d ⟩) -> lx ≈ (δ lx)
- x≈δx = {!!}
+ x≈δx = transport
+ (sym (λ i → (lx : L℧ ⟨ d ⟩) -> unfold-≈ i lx (δ lx)))
+ (fix x≈'δx)
-- ¬_ : Set → Set
@@ -1072,6 +1202,10 @@ module Bisimilarity (d : Predomain) where
+
+
+
+
{-
lem1 :
▹ ((lx : L℧ ⟨ d ⟩) -> lx ≾' θ (next lx)) ->
@@ -1138,6 +1272,7 @@ module Bisimilarity (d : Predomain) where
+{-
-- Extensional relation (two terms are error-related "up to thetas")
module ExtRel (d : Predomain) where
@@ -1148,7 +1283,7 @@ module ExtRel (d : Predomain) where
x ⊴ y = Σ (L℧ ⟨ d ⟩) λ p -> Σ (L℧ ⟨ d ⟩) λ q ->
(x ≈ p) × (p ≾ q) × (q ≈ y)
-
+-}
diff --git a/formalizations/guarded-cubical/SyntacticTermPrecision.agda b/formalizations/guarded-cubical/SyntacticTermPrecision.agda
deleted file mode 100644
index ee17a0c1e55226cffb8fcdfbeea4ae08709556ff..0000000000000000000000000000000000000000
--- a/formalizations/guarded-cubical/SyntacticTermPrecision.agda
+++ /dev/null
@@ -1,170 +0,0 @@
-{-# 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
diff --git a/formalizations/guarded-cubical/GradualSTLC.agda b/formalizations/guarded-cubical/Syntax/DeBruijnCommon.agda
similarity index 57%
rename from formalizations/guarded-cubical/GradualSTLC.agda
rename to formalizations/guarded-cubical/Syntax/DeBruijnCommon.agda
index 1c83416b29c765bf916392438729d7ac889ac1ff..21950d7fd4a80bd9afa39fdd656330ee7938364b 100644
--- a/formalizations/guarded-cubical/GradualSTLC.agda
+++ b/formalizations/guarded-cubical/Syntax/DeBruijnCommon.agda
@@ -1,14 +1,29 @@
{-# OPTIONS --cubical --rewriting --guarded #-}
-module GradualSTLC where
-
open import Cubical.Foundations.Prelude
+
+
+module Syntax.DeBruijnCommon
+ (Ty : Type)
+ (Ctx : Type)
+ ( · : Ctx)
+ (_::_ : Ctx -> Ty -> Ctx)
+ (let infixr 5 _::_ ; _::_ = _::_)
+ (_∋_ : Ctx -> Ty -> Type)
+ (let infixr 4 _∋_ ; _∋_ = _∋_)
+ (vz : ∀ {Γ S} -> Γ :: S ∋ S)
+ (vs : ∀ {Γ S T} (x : Γ ∋ T) -> (Γ :: S ∋ T))
+ (Tm : Ctx -> Ty -> Type)
+ where
+
+
+
open import Cubical.Data.Nat
open import Cubical.Relation.Nullary
-- Types --
-
+{-
data Ty : Set where
nat : Ty
dyn : Ty
@@ -48,63 +63,6 @@ data _⊑_ : Ty -> Ty -> Set where
⊑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
- _=>_ : {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
@@ -147,11 +105,12 @@ data Ctx : Set where
infixr 5 _::_
+
-- "Contains" relation stating that a context Γ contains a type T
data _∋_ : Ctx -> Ty -> Set where
vz : ∀ {Γ S} -> Γ :: S ∋ S
- vs : ∀ {Γ S T} (x : Γ ∋ T) -> (Γ :: S ∋ T)
+ vs : ∀ {Γ S T} (x : Γ ∋ T) -> (Γ :: S ∋ T)
infix 4 _∋_
@@ -170,15 +129,19 @@ data Tm : Ctx -> Ty -> Set where
-- infix 4 _â–¸_
+-}
+
-- ================================================================= --
--- Type of "proofs" --
+-- Type of "proofs", i.e., relations between contexts and types --
ProofT = Ctx -> Ty -> Set
+-- Kits --
+
VarToProof : ProofT -> Set
VarToProof _◆_ = ∀ {Γ T} -> (Γ ∋ T) -> (Γ ◆ T)
-- The diamond is a function, and the underscores around it allow us to use it in infix
@@ -189,10 +152,6 @@ ProofToTm _◆_ = ∀ {Γ T} -> (Γ ◆ T) -> (Tm Γ T)
WeakeningMap : ProofT -> Set
WeakeningMap _◆_ = ∀ {Γ S T} -> (Γ ◆ T) -> ((Γ :: S) ◆ T)
-
-
--- Kits --
-
data Kit (â—† : ProofT) : Set where
kit : ∀ (vr : VarToProof ◆) (tm : ProofToTm ◆) (wk : WeakeningMap ◆) -> Kit ◆
@@ -203,16 +162,27 @@ Subst : Ctx -> Ctx -> ProofT -> Set
Subst Δ Γ _◈_ = ∀ {T} -> (Γ ∋ T) -> (Δ ◈ T)
--- Lift function --
+module DeBruijn
+ (trav : {Δ Γ : Ctx} {T : Ty} {_◈_ : ProofT} (K : Kit _◈_)
+ (τ : Subst Δ Γ _◈_) (t : Tm Γ T) -> Tm Δ T)
+ (var : ∀ {Γ T} -> Γ ∋ T -> Tm Γ T)
+ where
+
+
+ -- Lift function --
+
+{-
lft : {Δ Γ : Ctx} {S : Ty} {_◈_ : ProofT}
- (K : Kit _◈_) (τ : Subst Δ Γ _◈_) {T : Ty} (h : (Γ :: S) ∋ T) -> (Δ :: S) ◈ T
+ (K : Kit _◈_) (τ : Subst Δ Γ _◈_) {T : Ty} (h : (Γ :: S) ∋ T) -> (Δ :: S) ◈ T
lft (kit vr tm wk) Ï„ vz = vr vz
lft (kit vr tm wk) Ï„ (vs x) = wk (Ï„ x)
+-}
-- Note that the type of lft can also be written as (Subst Δ Γ _◈_) -> (Subst (Δ ∷ S) (Γ ∷ S) _◈_)
+{-
-- Traversal function --
trav : {Δ Γ : Ctx} {T : Ty} {_◈_ : ProofT} (K : Kit _◈_)
@@ -225,74 +195,34 @@ 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 --
-
-idContains : {Γ : Ctx} {T : Ty} (t : Γ ∋ T) -> Γ ∋ T
-idContains t = t
-
-varKit : Kit _∋_
-varKit = kit idContains var vs
-
-rename : {Γ Δ : Ctx} {T : Ty} (Ï : Subst Δ Γ _∋_) (t : Tm Γ T) -> Tm Δ T
-rename Ï t = trav varKit Ï t
+ -- Renaming --
--- Substitution --
+ idContains : {Γ : Ctx} {T : Ty} (t : Γ ∋ T) -> Γ ∋ T
+ idContains t = t
-idTerm : {Γ : Ctx} {T : Ty} (t : Tm Γ T) -> Tm Γ T
-idTerm t = t
+ varKit : Kit _∋_
+ varKit = kit idContains var vs
-weakenTerm : WeakeningMap Tm
-weakenTerm = rename vs
+ rename : {Γ Δ : Ctx} {T : Ty} (Ï : Subst Δ Γ _∋_) (t : Tm Γ T) -> Tm Δ T
+ rename Ï t = trav varKit Ï t
-termKit : Kit Tm
-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]
+ -- Substitution --
-_[_] : ∀ {Γ 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)
-
--- Upcasts are values, downcasts are evaluation contexts
+ idTerm : {Γ : Ctx} {T : Ty} (t : Tm Γ T) -> Tm Γ T
+ idTerm t = t
-{-
-data Value : Type where
- Zero : {Γ} -> Value
- Suc : Value -> Value
--}
+ weakenTerm : WeakeningMap Tm
+ weakenTerm = rename vs
+ termKit : Kit Tm
+ termKit = kit var idTerm weakenTerm
+ sub : (Δ Γ : Ctx) (σ : Subst Δ Γ Tm) (T : Ty) (t : Tm Γ T) -> Tm Δ T
+ sub Δ Γ σ T t = trav termKit σ t
diff --git a/formalizations/guarded-cubical/Syntax/GSTLC.agda b/formalizations/guarded-cubical/Syntax/GSTLC.agda
new file mode 100644
index 0000000000000000000000000000000000000000..0d9ca07250b1708a1178d9a59de476e37e60eb54
--- /dev/null
+++ b/formalizations/guarded-cubical/Syntax/GSTLC.agda
@@ -0,0 +1,278 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+
+open import Common.Later
+
+module Syntax.GSTLC (k : Clock) where
+
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat hiding (_·_)
+open import Cubical.Relation.Nullary
+open import Cubical.Foundations.Function
+open import Cubical.Data.Prod
+open import Cubical.Foundations.Isomorphism
+
+import Syntax.DeBruijnCommon
+
+
+private
+ variable
+ â„“ : Level
+
+private
+ ▹_ : Set ℓ → Set ℓ
+ â–¹_ A = â–¹_,_ k A
+
+-- Types --
+
+data Interval : Type where
+ l r : Interval
+
+data iCtx : Type where
+ Empty : iCtx
+ Full : iCtx
+
+
+data Ty : iCtx -> Type where
+ nat : ∀ {Ξ} -> Ty Ξ
+ dyn : ∀ {Ξ} -> Ty Ξ
+ _=>_ : ∀ {Ξ} -> Ty Ξ -> Ty Ξ -> Ty Ξ
+ inj-nat : Ty Full
+ inj-arrow : Ty Full -> Ty Full
+
+
+-- From a "full" type, i.e. a type precision derivation, we can completely recover its left and
+-- right "endpoints"
+{-
+lft : Ty Full -> Ty Empty
+lft nat = nat
+lft dyn = dyn
+lft (cin => cout) = lft cin => lft cout
+lft inj-nat = nat
+lft (inj-arrow c) = lft c -- here, c : A ⊑ (dyn => dyn), and inj-arrow c : A ⊑ dyn
+
+rgt : Ty Full -> Ty Empty
+rgt nat = nat
+rgt dyn = dyn
+rgt (cin => cout) = rgt cin => rgt cout
+rgt inj-nat = dyn
+rgt (inj-arrow c) = dyn
+-}
+
+endpoint : Interval -> Ty Full -> Ty Empty
+endpoint p nat = nat
+endpoint p dyn = dyn
+endpoint p (cin => cout) = endpoint p cin => endpoint p cout
+endpoint l inj-nat = nat
+endpoint r inj-nat = dyn
+endpoint l (inj-arrow c) = endpoint l c -- here, c : A ⊑ (dyn => dyn), and inj-arrow c : A ⊑ dyn
+endpoint r (inj-arrow c) = dyn
+
+_[_/i] : Ty Full -> Interval -> Ty Empty
+c [ p /i] = endpoint p c
+
+left : Ty Full -> Ty Empty
+left = endpoint l
+
+right : Ty Full -> Ty Empty
+right = endpoint r
+
+
+_⊑_ : Ty Empty -> Ty Empty -> Type
+A ⊑ B = Σ[ c ∈ Ty Full ] ((left c ≡ A) × (right c ≡ B))
+
+
+infixr 5 _=>_
+
+⊑-ref : (A : Ty Empty) -> A ⊑ A
+⊑-ref nat = nat , (refl , refl)
+⊑-ref dyn = dyn , (refl , refl)
+⊑-ref (Ai => Ao) with ⊑-ref Ai | ⊑-ref Ao
+... | ci , (eq-left-i , eq-right-i) | co , (eq-left-o , eq-right-o) =
+ (ci => co) ,
+ ((congâ‚‚ _=>_ eq-left-i eq-left-o) ,
+ (congâ‚‚ _=>_ eq-right-i eq-right-o))
+
+{-
+
+{-
+data _⊑_ : Ty Empty -> Ty Empty -> Set where
+ dyn : dyn ⊑ dyn
+ _=>_ : {A A' B B' : Ty Empty} ->
+ A ⊑ A' -> B ⊑ B' -> (A => B) ⊑ (A' => B')
+ nat : nat ⊑ nat
+ inj-nat : nat ⊑ dyn
+ inj-arrow : {A : Ty Empty} ->
+ A ⊑ (dyn => dyn) -> A ⊑ dyn
+ -- inj-arrow : {A A' : Ty} ->
+ -- (A => A') ⊑ (dyn => dyn) -> (A => A') ⊑ dyn
+-}
+
+
+⊑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
+
+
+
+module ⊑-properties where
+ -- experiment with modules
+ ⊑-prop : ∀ A B → isProp (A ⊑ B)
+ ⊑-prop .dyn .dyn dyn dyn = refl
+ ⊑-prop .(_ => _) .(_ => _) (p1 => p3) (p2 => p4) = λ i → (⊑-prop _ _ p1 p2 i) => (⊑-prop _ _ p3 p4 i)
+ ⊑-prop .nat .nat nat nat = refl
+ ⊑-prop .nat .dyn inj-nat inj-nat = refl
+ ⊑-prop A .dyn (inj-arrow p1) (inj-arrow p2) = λ i → inj-arrow (⊑-prop _ _ p1 p2 i)
+
+ dyn-⊤ : ∀ A → A ⊑ dyn
+ dyn-⊤ nat = inj-nat
+ dyn-⊤ dyn = dyn
+ dyn-⊤ (A => B) = inj-arrow (dyn-⊤ A => dyn-⊤ B)
+
+ ⊑-dec : ∀ A B → Dec (A ⊑ B)
+ ⊑-dec A dyn = yes (dyn-⊤ A)
+ ⊑-dec nat nat = yes nat
+ ⊑-dec nat (B => Bâ‚) = no (λ ())
+ ⊑-dec dyn nat = no (λ ())
+ ⊑-dec dyn (B => Bâ‚) = no (λ ())
+ ⊑-dec (A => Aâ‚) nat = no ((λ ()))
+ ⊑-dec (A => B) (A' => B') with (⊑-dec A A') | (⊑-dec B B')
+ ... | yes p | yes q = yes (p => q)
+ ... | yes p | no ¬p = no (refute ¬p)
+ where refute : ∀ {A A' B B'} → (¬ (B ⊑ B')) → ¬ ((A => B) ⊑ (A' => B'))
+ refute ¬p (_ => p) = ¬p p
+ ... | no ¬p | _ = no (refute ¬p)
+ where refute : ∀ {A A' B B'} → (¬ (A ⊑ A')) → ¬ ((A => B) ⊑ (A' => B'))
+ refute ¬p (p => _) = ¬p p
+
+-}
+
+
+-- Contexts --
+
+data Ctx : iCtx -> Type where
+ · : ∀ {Ξ} -> Ctx Ξ
+ _::_ : ∀ {Ξ} -> Ctx Ξ -> Ty Ξ -> Ctx Ξ
+
+infixr 5 _::_
+
+-- Given a "normal" type A, view it as its reflexivity precision derivation c : A ⊑ A.
+ty-refl : Ty Empty -> Ty Full
+ty-refl nat = nat
+ty-refl dyn = dyn
+ty-refl (Ai => Ao) = ty-refl Ai => ty-refl Ao
+
+-- View a "normal" typing context Γ as a type precision context where the derivation
+-- corresponding to each type A in Γ is just the reflexivity precision derivation A ⊑ A.
+ctx-refl : Ctx Empty -> Ctx Full
+ctx-refl · = ·
+ctx-refl (Γ :: A) = ctx-refl Γ :: ty-refl A
+
+-- Flag determining whether the syntax is intensional (i.e., with θ) or extensional
+data IntExt : Type where
+ Int Ext : IntExt
+
+-- "Contains" relation stating that a context Γ contains a type T
+data _∋_ : ∀ {Ξ} -> Ctx Ξ -> Ty Ξ -> Set where
+ vz : ∀ {Ξ Γ S} -> _∋_ {Ξ} (Γ :: S) S
+ vs : ∀ {Ξ Γ S T} (x : _∋_ {Ξ} Γ T) -> (Γ :: S ∋ T)
+
+infix 4 _∋_
+
+
+-- All constructors below except for those for upcast and downcast are simultaneously
+-- the term constructors, as well as the constructors for the corresponding term
+-- precision congruence rule.
+-- This explains why Ξ is generic in all but the up and dn constructors,
+-- where it is Empty to indicate that we do not obtain term precision congruence rules.
+
+-- All constructors below except for θ simultaneously belong to the extensional
+-- and intensional languages. θ only exists in the intensional language.
+data Tm : (α : IntExt) {Ξ : iCtx} -> (Γ : Ctx Ξ) -> Ty Ξ -> Set where
+ var : ∀ {α Ξ Γ T} -> Γ ∋ T -> Tm α {Ξ} Γ T
+ lda : ∀ {α Ξ Γ S T} -> (Tm α {Ξ} (Γ :: S) T) -> Tm α Γ (S => T)
+ app : ∀ {α Ξ Γ S T} -> (Tm α {Ξ} Γ (S => T)) -> (Tm α Γ S) -> (Tm α Γ T)
+ err : ∀ {α Ξ Γ A} -> Tm α {Ξ} Γ A
+ up : ∀ {α Γ} (c : Ty Full) -> Tm α {Empty} Γ (left c) -> Tm α {Empty} Γ (right c)
+ dn : ∀ {α Γ} (c : Ty Full) -> Tm α {Empty} Γ (right c) -> Tm α {Empty} Γ (left c)
+ zro : ∀ {α Ξ Γ} -> Tm α {Ξ} Γ nat
+ suc : ∀ {α Ξ Γ} -> Tm α {Ξ} Γ nat -> Tm α Γ nat
+ θ : ∀ {Ξ Γ A} -> ▹ Tm Int {Ξ} Γ A -> Tm Int {Ξ} Γ A
+
+
+
+
+ -- Equational theory
+
+ -- Other term precision rules
+ err-bot : ∀ {α Γ} (c : Ty Full) (M : Tm α {Empty} Γ (right c)) -> Tm α {Full} (ctx-refl Γ) c
+
+
+-- TODO need to quotient by the equational theory!
+
+-- TODO non-congruence term precision rules
+
+
+
+-- Substitution and Renaming using De Bruijn framework
+module DB_Base = Syntax.DeBruijnCommon (Ty Empty) (Ctx Empty) · (_::_) _∋_ vz vs (Tm Ext {Empty})
+open DB_Base
+ -- Brings in definitions of ProofT, Kit, Subst
+
+
+ -- Lift function --
+
+lft : {Δ Γ : Ctx Empty} {S : Ty Empty} {_◈_ : ProofT}
+ (K : Kit _◈_) (τ : Subst Δ Γ _◈_) {T : Ty Empty} (h : (Γ :: S) ∋ T) -> (Δ :: S) ◈ T
+lft (kit vr tm wk) Ï„ vz = vr vz
+lft (kit vr tm wk) Ï„ (vs x) = wk (Ï„ x)
+ -- Note that the type of lft can also be written as (Subst Δ Γ _◈_) -> (Subst (Δ ∷ S) (Γ ∷ S) _◈_)
+
+ -- Traversal function --
+
+
+trav : {Δ Γ : Ctx Empty} {T : Ty Empty} {_◈_ : ProofT} (K : Kit _◈_)
+ (τ : Subst Δ Γ _◈_) (t : Tm Ext Γ T) -> Tm Ext Δ T
+trav (kit vr tm wk) Ï„ (var x) = tm (Ï„ x)
+trav K Ï„ (lda t') = (lda (trav K (lft K Ï„) t'))
+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'))
+
+
+open DB_Base.DeBruijn trav var
+-- Gives us renaming and substitution
+
+-- Single substitution
+-- N[M/x]
+
+
+_[_] : ∀ {Γ A B}
+ → Tm Ext (Γ :: B) A
+ → Tm Ext Γ B
+ → Tm Ext Γ A
+_[_] {Γ} {A} {B} N M = {!!} -- sub Γ (Γ :: B) σ A N
+ where
+ σ : Subst Γ (Γ :: B) (Tm Ext) -- i.e., {T : Ty} → Γ :: B ∋ T → Tm Γ T
+ σ vz = M
+ σ (vs x) = var x
+
+
+
+
+
diff --git a/formalizations/guarded-cubical/Syntax/GSTLCCollapse.agda b/formalizations/guarded-cubical/Syntax/GSTLCCollapse.agda
new file mode 100644
index 0000000000000000000000000000000000000000..d566b9140fc4659911f237ccbd5597706a365969
--- /dev/null
+++ b/formalizations/guarded-cubical/Syntax/GSTLCCollapse.agda
@@ -0,0 +1,66 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+open import Common.Later
+
+module Syntax.GSTLCCollapse (k : Clock) where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat hiding (_·_)
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Sum
+open import Cubical.Foundations.Isomorphism
+
+import Syntax.DeBruijnCommon
+open import Syntax.GSTLC k
+
+
+private
+ variable
+ â„“ : Level
+
+private
+ ▹_ : Set ℓ → Set ℓ
+ â–¹_ A = â–¹_,_ k A
+
+
+IntTm = Tm Int
+ExtTm = Tm Ext
+
+
+⌊_⌋ : ∀ {Γ} {A} -> IntTm {Empty} Γ A -> ExtTm {Empty} Γ A
+⌊ var x ⌋ = var x
+⌊ lda M ⌋ = lda ⌊ M ⌋
+⌊ app M N ⌋ = app ⌊ M ⌋ ⌊ N ⌋
+⌊ err ⌋ = err
+⌊ up c M ⌋ = up c ⌊ M ⌋
+⌊ dn c M ⌋ = dn c ⌊ M ⌋
+⌊ zro ⌋ = zro
+⌊ suc M ⌋ = suc ⌊ M ⌋
+⌊ θ M~ ⌋ = ⌊ M~ ◇ ⌋
+
+
+embed : ∀ {Γ} {A} -> ExtTm {Empty} Γ A -> IntTm {Empty} Γ A
+embed (var x) = var x
+embed (lda M) = lda (embed M)
+embed (app M N) = app (embed M) (embed N)
+embed err = err
+embed (up c M) = up c (embed M)
+embed (dn c M) = dn c (embed M)
+embed zro = zro
+embed (suc M) = suc (embed M)
+
+
+
+-- Every extensional term has an intensional program computing it
+collapse-embed : ∀ {Γ} {A} -> retract embed (⌊_⌋ {Γ} {A})
+collapse-embed (var x) = refl
+collapse-embed (lda M) = cong lda (collapse-embed M)
+collapse-embed (app M N) = congâ‚‚ app (collapse-embed M) (collapse-embed N)
+collapse-embed err = refl
+collapse-embed (up c M) = cong (up c) (collapse-embed M)
+collapse-embed (dn c M) = cong (dn c) (collapse-embed M)
+collapse-embed zro = refl
+collapse-embed (suc M) = cong suc (collapse-embed M)
+
+
+