From 17874a9eba71af0396f8de1e2f3cd48e3e1e9b9b Mon Sep 17 00:00:00 2001 From: vikraman Date: Sun, 13 Oct 2024 19:50:06 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20vikraman?= =?UTF-8?q?/agda-coexp@1b2bb0c78797166404d49bd70d673853a8dd7556=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Coexp.Kappa.Syntax.html | 16 +- Coexp.KappaStar.Syntax.html | 16 +- Coexp.LamLamBar.Interp.html | 1028 ++++++++++++++++++----------------- Coexp.LamLamBar.Syntax.html | 428 +++++++-------- Coexp.Meta.Prelude.html | 68 +-- Coexp.Zeta.Syntax.html | 16 +- Coexp.ZetaStar.Syntax.html | 16 +- 7 files changed, 796 insertions(+), 792 deletions(-) diff --git a/Coexp.Kappa.Syntax.html b/Coexp.Kappa.Syntax.html index 20a26e7..4398366 100644 --- a/Coexp.Kappa.Syntax.html +++ b/Coexp.Kappa.Syntax.html @@ -50,18 +50,18 @@ wk-arr π (lift e) = lift (wk-arr π e) wk-arr π (κ e) = κ (wk-arr (wk-cong π) e) -open WkArr Arr wk-arr -open Sub `1 var +open WkArr Arr wk-arr +open Sub `1 var -sub-arr : Sub Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B -sub-arr θ (var i) = sub-mem θ i +sub-arr : Sub Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B +sub-arr θ (var i) = sub-mem θ i sub-arr θ id = id sub-arr θ bang = bang sub-arr θ (e1 ∘ e2) = sub-arr θ e1 ∘ sub-arr θ e2 sub-arr θ (lift e) = lift (sub-arr θ e) -sub-arr θ (κ e) = κ (sub-arr (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e) +sub-arr θ (κ e) = κ (sub-arr (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e) -open SubArr sub-arr +open SubArr sub-arr syntax Eq Γ A B e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A ->> B @@ -85,9 +85,9 @@ κ-beta : (f : (Γ ∙ C) ⊢ A ->> B) (c : Γ ⊢ `1 ->> C) ------------------------------------------------ - -> Γ ⊢ κ {C = C} f ∘ lift {A = A} c ≈ sub c f ∶ A ->> B + -> Γ ⊢ κ {C = C} f ∘ lift {A = A} c ≈ sub c f ∶ A ->> B κ-eta : (f : Γ ⊢ C `× A ->> B) --------------------------------------------------- - -> Γ ⊢ κ {C = C} (wk f ∘ lift {A = A} (var h)) ≈ f ∶ C `× A ->> B + -> Γ ⊢ κ {C = C} (wk f ∘ lift {A = A} (var h)) ≈ f ∶ C `× A ->> B \ No newline at end of file diff --git a/Coexp.KappaStar.Syntax.html b/Coexp.KappaStar.Syntax.html index d35dbb6..c3d25bd 100644 --- a/Coexp.KappaStar.Syntax.html +++ b/Coexp.KappaStar.Syntax.html @@ -52,18 +52,18 @@ wk-arr π (lift* e) = lift* (wk-arr π e) wk-arr π (κ* e) = κ* (wk-arr (wk-cong π) e) -open WkArr Arr wk-arr -open Sub `1 var +open WkArr Arr wk-arr +open Sub `1 var -sub-arr : Sub Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B -sub-arr θ (var i) = sub-mem θ i +sub-arr : Sub Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B +sub-arr θ (var i) = sub-mem θ i sub-arr θ id = id sub-arr θ bang = bang sub-arr θ (e1 ∘ e2) = sub-arr θ e1 ∘ sub-arr θ e2 sub-arr θ (lift* e) = lift* (sub-arr θ e) -sub-arr θ (κ* e) = κ* (sub-arr (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e) +sub-arr θ (κ* e) = κ* (sub-arr (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e) -open SubArr sub-arr +open SubArr sub-arr syntax Eq Γ A B e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A ->> B @@ -87,9 +87,9 @@ κ*-beta : (f : (Γ ∙ C *) ⊢ A ->> B) (c : Γ ⊢ `1 ->> C *) ------------------------------------------------ - -> Γ ⊢ κ* {C = C} f ∘ lift* {A = A} c ≈ sub c f ∶ A ->> B + -> Γ ⊢ κ* {C = C} f ∘ lift* {A = A} c ≈ sub c f ∶ A ->> B κ*-eta : (f : Γ ⊢ (A `- C) ->> B) --------------------------------------------------- - -> Γ ⊢ κ* {C = C} (wk f ∘ lift* {A = A} (var h)) ≈ f ∶ (A `- C) ->> B + -> Γ ⊢ κ* {C = C} (wk f ∘ lift* {A = A} (var h)) ≈ f ∶ (A `- C) ->> B \ No newline at end of file diff --git a/Coexp.LamLamBar.Interp.html b/Coexp.LamLamBar.Interp.html index 2e7da7d..034e4f4 100644 --- a/Coexp.LamLamBar.Interp.html +++ b/Coexp.LamLamBar.Interp.html @@ -19,516 +19,520 @@ -- interpretation of types -- functions are kleisli arrows interpTy : Ty -> Set -interpTy `Nat = ℕ -interpTy `Unit = ⊤ -interpTy (A *) = interpTy A -> R -interpTy (A `× B) = interpTy A × interpTy B -interpTy (A `⇒ B) = interpTy A -> T (interpTy B) -interpTy (A `+ B) = interpTy A ⊎ interpTy B - --- interpretation of contexts -interpCtx : Ctx -> Set -interpCtx ε = ⊤ -interpCtx (Γ ∙ A) = interpCtx Γ × interpTy A - --- interpretation of membership -interpIn : A ∈ Γ -> interpCtx Γ -> interpTy A -interpIn h = proj₂ -interpIn (t i) = proj₁ ； interpIn i - --- interpretation of terms -interpTm : Γ ⊢ A -> interpCtx Γ -> T (interpTy A) -interpTm (nat n) = - const n ； T.eta -interpTm (zero? e) = - interpTm e ； T.map is-zero -interpTm (var i) = - interpIn i ； T.eta -interpTm (lam e) = - curry (interpTm e) ； T.eta -interpTm (app e1 e2) = - let f = interpTm e1 ; x = interpTm e2 - in < f , x > ； T.beta ； T.map eval ； T.mu -interpTm (pair e1 e2) = - let f = interpTm e1 ; g = interpTm e2 - in < f , g > ； T.beta -interpTm (fst e) = - interpTm e ； T.map proj₁ -interpTm (snd e) = - interpTm e ； T.map proj₂ -interpTm unit = - const tt ； T.eta -interpTm (inl e) = - interpTm e ； T.map inj₁ -interpTm (inr e) = - interpTm e ； T.map inj₂ -interpTm (case e1 e2 e3) = - let f = interpTm e1 ; g1 = interpTm e2 ; g2 = interpTm e3 - in < id , f > ； T.tau ； T.map distl ； T.map S.[ g1 , g2 ] ； T.mu -interpTm (colam e) = - councurry (interpTm e) -interpTm (coapp e1 e2) = - let f = interpTm e1 ; g = interpTm e2 - in < f , g > ； T.tau ； T.map couneval ； T.mu - --- interpretation of weakening -interpWk : Wk Γ Δ -> interpCtx Γ -> interpCtx Δ -interpWk wk-ε = const tt -interpWk (wk-cong π) = pmap (interpWk π) id -interpWk (wk-wk π) = proj₁ ； interpWk π - -interpWk-id-coh : interpWk (wk-id {Γ}) ≡ id -interpWk-id-coh {Γ = ε} = refl -interpWk-id-coh {Γ = Γ ∙ A} rewrite interpWk-id-coh {Γ = Γ} = refl -{-# REWRITE interpWk-id-coh #-} - -interpWk-mem-coh : (π : Wk Γ Δ) (i : A ∈ Δ) -> interpIn (wk-mem π i) ≡ interpWk π ； interpIn i -interpWk-mem-coh (wk-cong π) h = refl -interpWk-mem-coh (wk-cong π) (t i) rewrite interpWk-mem-coh π i = refl -interpWk-mem-coh (wk-wk π) h rewrite interpWk-mem-coh π h = refl -interpWk-mem-coh (wk-wk π) (t i) rewrite interpWk-mem-coh π (t i) = refl - -interpWk-tm-coh : (π : Wk Γ Δ) (e : Δ ⊢ A) -> interpTm (wk-tm π e) ≡ interpWk π ； interpTm e -interpWk-tm-coh π (nat n) = refl -interpWk-tm-coh π (zero? e) rewrite interpWk-tm-coh π e = refl -interpWk-tm-coh π (var i) rewrite interpWk-mem-coh π i = refl -interpWk-tm-coh π (lam e) rewrite (interpWk-tm-coh (wk-cong π) e) = refl -interpWk-tm-coh π (app e1 e2) rewrite interpWk-tm-coh π e1 | interpWk-tm-coh π e2 = refl -interpWk-tm-coh π (pair e1 e2) rewrite interpWk-tm-coh π e1 | interpWk-tm-coh π e2 = refl -interpWk-tm-coh π (fst e) rewrite interpWk-tm-coh π e = refl -interpWk-tm-coh π (snd e) rewrite interpWk-tm-coh π e = refl -interpWk-tm-coh π unit = refl -interpWk-tm-coh π (inl e) rewrite interpWk-tm-coh π e = refl -interpWk-tm-coh π (inr e) rewrite interpWk-tm-coh π e = refl -interpWk-tm-coh π (case e1 e2 e3) rewrite interpWk-tm-coh π e1 | interpWk-tm-coh (wk-cong π) e2 | interpWk-tm-coh (wk-cong π) e3 = - funext \γ -> funext \k -> cong (interpTm e1 (interpWk π γ)) (funext \{ (inj₁ a) -> refl ; (inj₂ b) -> refl }) -interpWk-tm-coh π (colam e) rewrite interpWk-tm-coh (wk-cong π) e = refl -interpWk-tm-coh π (coapp e1 e2) rewrite interpWk-tm-coh π e1 | interpWk-tm-coh π e2 = refl -{-# REWRITE interpWk-tm-coh #-} - --- interpretation of values -interpVal : (e : Γ ⊢ A) -> isVal e -> interpCtx Γ -> interpTy A -interpVal (nat n) nat = const n -interpVal (zero? e) (zero? {{ϕ}}) = interpVal e ϕ ； is-zero -interpVal (var i) var = interpIn i -interpVal (lam e) lam = curry (interpTm e) -interpVal (fst e) (fst {{ϕ}}) = interpVal e ϕ ； proj₁ -interpVal (snd e) (snd {{ϕ}}) = interpVal e ϕ ； proj₂ -interpVal (pair e1 e2) (pair {{ϕ1}} {{ϕ2}}) = < interpVal e1 ϕ1 , interpVal e2 ϕ2 > -interpVal unit unit = const tt -interpVal (inl e) (inl {{ϕ}}) = interpVal e ϕ ； inj₁ -interpVal (inr e) (inr {{ϕ}}) = interpVal e ϕ ； inj₂ - --- value interpretation coherence lemma -interpVal-tm-coh : (e : Γ ⊢ A) (ϕ : isVal e) -> interpTm e ≡ interpVal e ϕ ； T.eta -interpVal-tm-coh (nat n) nat = refl -interpVal-tm-coh (zero? e) (zero? {{ϕ}}) - rewrite interpVal-tm-coh e ϕ = refl -interpVal-tm-coh (var i) var = refl -interpVal-tm-coh (lam e) lam = refl -interpVal-tm-coh (fst e) (fst {{ϕ}}) - rewrite interpVal-tm-coh e ϕ = refl -interpVal-tm-coh (snd e) (snd {{ϕ}}) - rewrite interpVal-tm-coh e ϕ = refl -interpVal-tm-coh (pair e1 e2) (pair {{ϕ1}} {{ϕ2}}) - rewrite interpVal-tm-coh e1 ϕ1 | interpVal-tm-coh e2 ϕ2 = refl -interpVal-tm-coh unit unit = refl -interpVal-tm-coh (inl e) (inl {{ϕ}}) - rewrite interpVal-tm-coh e ϕ = refl -interpVal-tm-coh (inr e) (inr {{ϕ}}) - rewrite interpVal-tm-coh e ϕ = refl - -interpVal-wk-coh : (π : Wk Γ Δ) (v : Δ ⊢ A) (ϕ : isVal v) -> interpVal (wk-tm π v) (wk-tm-val π v ϕ) ≡ interpWk π ； interpVal v ϕ -interpVal-wk-coh π (nat n) nat = refl -interpVal-wk-coh π (zero? v) (zero? {{ϕ}}) rewrite interpVal-wk-coh π v ϕ = refl -interpVal-wk-coh π (var i) var = interpWk-mem-coh π i -interpVal-wk-coh π (lam e) lam rewrite interpWk-tm-coh (wk-cong π) e = refl -interpVal-wk-coh π (fst v) (fst {{ϕ}}) rewrite interpVal-wk-coh π v ϕ = refl -interpVal-wk-coh π (snd v) (snd {{ϕ}}) rewrite interpVal-wk-coh π v ϕ = refl -interpVal-wk-coh π (pair v1 v2) (pair {{ϕ1}} {{ϕ2}}) rewrite interpVal-wk-coh π v1 ϕ1 | interpVal-wk-coh π v2 ϕ2 = refl -interpVal-wk-coh π unit unit = refl -interpVal-wk-coh π (inl v) (inl {{ϕ}}) rewrite interpVal-wk-coh π v ϕ = refl -interpVal-wk-coh π (inr v) (inr {{ϕ}}) rewrite interpVal-wk-coh π v ϕ = refl -{-# REWRITE interpVal-wk-coh #-} - -open Val isVal - --- interpretation of substitutions -interpSub : (θ : Sub Γ Δ) (ϕ : isSub θ) -> interpCtx Γ -> interpCtx Δ -interpSub sub-ε sub-ε = const tt -interpSub (sub-ex θ v) (sub-ex ϕ ψ) = < interpSub θ ϕ , interpVal v ψ > - -interpSub-wk-coh : (π : Wk Γ Δ) -> (θ : Sub Δ Ψ) (ϕ : isSub θ) -> interpSub (sub-wk π θ) (sub-wk-sub π θ ϕ) ≡ interpWk π ； interpSub θ ϕ -interpSub-wk-coh π sub-ε sub-ε = refl -interpSub-wk-coh π (sub-ex θ v) (sub-ex ϕ ψ) rewrite interpSub-wk-coh π θ ϕ | interpVal-wk-coh π v ψ = refl -{-# REWRITE interpSub-wk-coh #-} - -interpSub-id-coh : {Γ : Ctx} -> interpSub (sub-id {Γ}) (sub-id-sub {Γ}) ≡ id -interpSub-id-coh {ε} = refl -interpSub-id-coh {Γ ∙ A} = - < interpSub (sub-wk (wk-wk wk-id) sub-id) (sub-wk-sub (wk-wk wk-id) sub-id sub-id-sub) , proj₂ > ≡⟨ cong (\f -> < f , proj₂ >) (interpSub-wk-coh (wk-wk wk-id) (sub-id {Γ}) sub-id-sub) ⟩ - < proj₁ ； interpWk wk-id ； interpSub sub-id sub-id-sub , proj₂ > ≡⟨ cong (\f -> < proj₁ ； interpWk wk-id ； f , proj₂ >) (interpSub-id-coh {Γ}) ⟩ - < proj₁ ； interpWk wk-id , proj₂ > ≡⟨ cong (\f -> < proj₁ ； f , proj₂ >) interpWk-id-coh ⟩ - id ∎ - where open ≡-Reasoning -{-# REWRITE interpSub-id-coh #-} - -interpSub-mem-val-coh : (θ : Sub Γ Δ) (ϕ : isSub θ) (i : A ∈ Δ) -> interpVal (sub-mem θ i) (sub-mem-val θ ϕ i) ≡ interpSub θ ϕ ； interpIn i -interpSub-mem-val-coh (sub-ex θ e) (sub-ex ϕ ψ) h = refl -interpSub-mem-val-coh (sub-ex θ e) (sub-ex ϕ ψ) (t i) rewrite interpSub-mem-val-coh θ ϕ i = refl - -interpSub-mem-tm-coh : (θ : Sub Γ Δ) (ϕ : isSub θ) (i : A ∈ Δ) -> interpTm (sub-mem θ i) ≡ interpSub θ ϕ ； interpIn i ； T.eta -interpSub-mem-tm-coh θ ϕ i rewrite interpVal-tm-coh (sub-mem θ i) (sub-mem-val θ ϕ i) | interpSub-mem-val-coh θ ϕ i = refl - -interpSub-tm-coh : (θ : Sub Γ Δ) (ϕ : isSub θ) -> (e : Δ ⊢ A) -> interpTm (sub-tm θ e) ≡ interpSub θ ϕ ； interpTm e -interpSub-tm-coh θ ϕ (nat n) = refl -interpSub-tm-coh θ ϕ (zero? e) rewrite interpSub-tm-coh θ ϕ e = refl -interpSub-tm-coh θ ϕ (var i) rewrite interpSub-mem-tm-coh θ ϕ i = refl -interpSub-tm-coh θ ϕ (lam e) = - curry (interpTm (sub-tm δ2 e)) ； T.eta ≡⟨ cong (\h -> curry h ； T.eta) (interpSub-tm-coh δ2 ψ2 e) ⟩ - curry (interpSub δ2 ψ2 ； interpTm e) ； T.eta ≡⟨ refl ⟩ - curry (< interpSub δ1 ψ1 , proj₂ > ； interpTm e) ； T.eta ≡⟨ cong (\h -> curry (< h , proj₂ > ； interpTm e) ； T.eta) (interpSub-wk-coh π1 θ ϕ) ⟩ - curry (< interpWk π1 ； interpSub θ ϕ , proj₂ > ； interpTm e) ； T.eta ≡⟨ cong (\h -> curry (< proj₁ ； h ； interpSub θ ϕ , proj₂ > ； interpTm e) ； T.eta) interpWk-id-coh ⟩ - curry (< proj₁ ； interpSub θ ϕ , proj₂ > ； interpTm e) ； T.eta ≡⟨ refl ⟩ - interpSub θ ϕ ； interpTm (lam e) ∎ - where open ≡-Reasoning - π1 = wk-wk wk-id - δ1 = sub-wk π1 θ ; ψ1 = sub-wk-sub π1 θ ϕ - δ2 = sub-ex δ1 (var h) ; ψ2 = sub-ex ψ1 var -interpSub-tm-coh θ ϕ (app e1 e2) rewrite interpSub-tm-coh θ ϕ e1 | interpSub-tm-coh θ ϕ e2 = refl -interpSub-tm-coh θ ϕ (pair e1 e2) rewrite interpSub-tm-coh θ ϕ e1 | interpSub-tm-coh θ ϕ e2 = refl -interpSub-tm-coh θ ϕ (fst e) rewrite interpSub-tm-coh θ ϕ e = refl -interpSub-tm-coh θ ϕ (snd e) rewrite interpSub-tm-coh θ ϕ e = refl -interpSub-tm-coh θ ϕ unit = refl -interpSub-tm-coh θ ϕ (inl e) rewrite interpSub-tm-coh θ ϕ e = refl -interpSub-tm-coh θ ϕ (inr e) rewrite interpSub-tm-coh θ ϕ e = refl -interpSub-tm-coh {Γ = Γ} θ ϕ (case {A = A} {B} e1 e2 e3) rewrite - interpSub-tm-coh θ ϕ e1 - | interpSub-tm-coh (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) (sub-ex (sub-wk-sub (wk-wk wk-id) θ ϕ) var) e2 - | interpSub-tm-coh (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) (sub-ex (sub-wk-sub (wk-wk wk-id) θ ϕ) var) e3 - | interpSub-wk-coh (wk-wk {A = A} wk-id) θ ϕ | interpSub-wk-coh (wk-wk {A = B} wk-id) θ ϕ - | interpWk-id-coh {Γ = Γ} = - funext \γ -> funext \k -> cong (interpTm e1 (interpSub θ ϕ γ)) (funext \{ (inj₁ a) -> refl ; (inj₂ b) -> refl }) -interpSub-tm-coh θ ϕ (colam e) = - councurry (interpTm (sub-tm δ2 e)) ≡⟨ cong councurry (interpSub-tm-coh δ2 ψ2 e) ⟩ - councurry (interpSub δ2 ψ2 ； interpTm e) ≡⟨ refl ⟩ - councurry (< interpSub δ1 ψ1 , proj₂ > ； interpTm e) ≡⟨ cong (\h -> councurry (< h , proj₂ > ； interpTm e)) (interpSub-wk-coh π1 θ ϕ) ⟩ - councurry (< interpWk π1 ； interpSub θ ϕ , proj₂ > ； interpTm e) ≡⟨ cong (\h -> councurry (< proj₁ ； h ； interpSub θ ϕ , proj₂ > ； interpTm e)) interpWk-id-coh ⟩ - councurry (< proj₁ ； interpSub θ ϕ , proj₂ > ； interpTm e) ≡⟨ refl ⟩ - interpSub θ ϕ ； interpTm (colam e) ∎ - where open ≡-Reasoning - π1 = wk-wk wk-id - δ1 = sub-wk π1 θ ; ψ1 = sub-wk-sub π1 θ ϕ - δ2 = sub-ex δ1 (var h) ; ψ2 = sub-ex ψ1 var -interpSub-tm-coh θ ϕ (coapp e1 e2) rewrite interpSub-tm-coh θ ϕ e1 | interpSub-tm-coh θ ϕ e2 = refl - --- continuation semantics -lookup : A ∈ Γ -> interpCtx Γ -> interpTy A -lookup = interpIn - -evalTm : Γ ⊢ A -> interpCtx Γ -> (interpTy A -> R) -> R -evalTm (nat n) γ k = - k n -evalTm (zero? e) γ k = - evalTm e γ \n -> - k (is-zero n) -evalTm (var i) γ k = - k (lookup i γ) -evalTm (lam e) γ k = - k \a kb -> evalTm e (γ , a) kb -evalTm (app e1 e2) γ k = - evalTm e2 γ \a -> - evalTm e1 γ \f -> - f a k -evalTm (pair e1 e2) γ k = - evalTm e2 γ \b -> - evalTm e1 γ \a -> - k (a , b) -evalTm (fst e) γ k = - evalTm e γ \p -> - k (proj₁ p) -evalTm (snd e) γ k = - evalTm e γ \p -> - k (proj₂ p) -evalTm unit γ k = - k tt -evalTm (inl e) γ k = - evalTm e γ \a -> - k (inj₁ a) -evalTm (inr e) γ k = - evalTm e γ \b -> - k (inj₂ b) -evalTm (case e1 e2 e3) γ k = - evalTm e1 γ - \{ (inj₁ a) -> evalTm e2 (γ , a) k - ; (inj₂ b) -> evalTm e3 (γ , b) k } -evalTm (colam e) γ k = - let ka = \a -> k (inj₁ a) - kb = \b -> k (inj₂ b) - in evalTm e (γ , ka) kb -evalTm (coapp e1 e2) γ k = - evalTm e2 γ \ka -> - evalTm e1 γ - \{ (inj₁ a) -> ka a - ; (inj₂ b) -> k b } - -_ : evalTm {Γ = ε} (colam (zero? (coapp (inl (nat 1)) (var h)))) tt ≡ \k -> k (inj₁ 1) -_ = refl - -_ : ∀ A -> evalTm {Γ = ε} (colam {A = A} (var h)) tt ≡ \k -> k (inj₂ (\a -> k (inj₁ a))) -_ = \A -> refl - --- both semantics agree --- -adequacy : (e : Γ ⊢ A) -> interpTm e ≡ evalTm e -adequacy (nat n) = refl -adequacy (zero? e) rewrite adequacy e = refl -adequacy (var x) = refl -adequacy (lam e) rewrite adequacy e = refl -adequacy (app e1 e2) rewrite adequacy e1 | adequacy e2 = refl -adequacy (pair e1 e2) rewrite adequacy e1 | adequacy e2 = refl -adequacy (fst e) rewrite adequacy e = refl -adequacy (snd e) rewrite adequacy e = refl -adequacy unit = refl -adequacy (inl e) rewrite adequacy e = refl -adequacy (inr e) rewrite adequacy e = refl -adequacy (case e1 e2 e3) rewrite adequacy e1 | adequacy e2 | adequacy e3 = - funext \γ -> funext \k -> - cong (evalTm e1 γ) (funext \{ (inj₁ a) -> refl ; (inj₂ b) -> refl }) -adequacy (colam e) rewrite adequacy e = refl -adequacy (coapp e1 e2) rewrite adequacy e1 | adequacy e2 = - funext \γ -> funext \k -> - cong (evalTm e2 γ) (funext \k1 -> cong (evalTm e1 γ) (funext \{ (inj₁ a) -> refl ; (inj₂ b) -> refl })) - --- soundness of equational theory - -interpWk-ev-coh : (π : Wk Γ Δ) (E : Δ ⊢ A ⇛ B) (e : Δ ⊢ A) -> interpTm (wk-ev π E [[ wk-tm π e ]]) ≡ interpWk π ； interpTm (E [[ e ]]) -interpWk-ev-coh π ø e = interpWk-tm-coh π e -interpWk-ev-coh π (app-r e1 E) e rewrite interpWk-tm-coh π e1 | interpWk-ev-coh π E e = refl -interpWk-ev-coh π (app-l E v) e rewrite interpWk-tm-coh π v | interpWk-ev-coh π E e = refl -{-# REWRITE interpWk-ev-coh #-} - -interpEv : Γ ⊢ C ⇛ A -> (f : interpCtx Γ -> T (interpTy C)) -> interpCtx Γ -> T (interpTy A) -interpEv ø = id -interpEv (app-r e E) f = - let x = interpEv E f ; g = interpTm e - in < g , x > ； T.beta ； T.map eval ； T.mu -interpEv (app-l E v {{ϕ}}) f = - let x = interpVal v ϕ ; g = interpEv E f - in < g , x > ； T.sigma ； T.map eval ； T.mu - -interpEv-Tm-coh : (E : Γ ⊢ A ⇛ B) (e : Γ ⊢ A) -> interpTm (E [[ e ]]) ≡ interpEv E (interpTm e) -interpEv-Tm-coh ø e = refl -interpEv-Tm-coh (app-r e1 E) e rewrite interpEv-Tm-coh E e = refl -interpEv-Tm-coh (app-l E v {{ϕ}}) e rewrite interpEv-Tm-coh E e | interpVal-tm-coh v ϕ = refl -{-# REWRITE interpEv-Tm-coh #-} - -interpWk-ev-coh' : (π : Wk Γ Δ) (E : Δ ⊢ A ⇛ B) (e : Γ ⊢ A) -> interpTm (wk-ev π E [[ e ]]) ≡ interpEv (wk-ev π E) (interpTm e) -interpWk-ev-coh' π ø e = refl -interpWk-ev-coh' π (app-r e1 E) e - rewrite interpWk-ev-coh' π E e = refl -interpWk-ev-coh' π (app-l E v {{ϕ}}) e = - interpTm (wk-ev π (app-l E v) [[ e ]]) ≡⟨ refl ⟩ - interpTm (app-l (wk-ev π E) (wk-tm π v) {{wk-tm-val π v ϕ}} [[ e ]]) ≡⟨ refl ⟩ - interpTm (app (wk-ev π E [[ e ]]) (wk-tm π v)) ≡⟨ refl ⟩ - < interpTm (wk-ev π E [[ e ]]) , interpTm (wk-tm π v) > ； T.beta ； T.map eval ； T.mu ≡⟨ cong (\z -> < interpTm (wk-ev π E [[ e ]]) , z > ； T.beta ； T.map eval ； T.mu) (interpVal-tm-coh (wk-tm π v) (wk-tm-val π v ϕ)) ⟩ - < interpTm (wk-ev π E [[ e ]]) , interpVal (wk-tm π v) (wk-tm-val π v ϕ) ； T.eta > ； T.beta ； T.map eval ； T.mu ≡⟨ refl ⟩ - < interpTm (wk-ev π E [[ e ]]) , interpVal (wk-tm π v) (wk-tm-val π v ϕ) > ； T.sigma ； T.map eval ； T.mu ≡⟨ refl ⟩ - < interpEv (wk-ev π E) (interpTm e) , interpVal (wk-tm π v) (wk-tm-val π v ϕ) > ； T.sigma ； T.map eval ； T.mu ≡⟨ refl ⟩ - interpEv (app-l (wk-ev π E) (wk-tm π v) {{wk-tm-val π v ϕ}}) (interpTm e) ≡⟨ refl ⟩ - interpEv (wk-ev π (app-l E v)) (interpTm e) ∎ - where open ≡-Reasoning - -interpEv-wk-coh : (π : Wk Γ Δ) (E : Δ ⊢ A ⇛ B) (f : interpCtx Δ -> T (interpTy A)) -> interpEv (wk-ev π E) (interpWk π ； f) ≡ interpWk π ； interpEv E f -interpEv-wk-coh π ø f = refl -interpEv-wk-coh π (app-r e E) f rewrite interpEv-wk-coh π E f = refl -interpEv-wk-coh π (app-l E v {{ϕ}}) f rewrite interpEv-wk-coh π E f | interpVal-wk-coh π v ϕ = refl - -interpEv-wk-coh' : {e : Γ ⊢ A} (E : Γ ⊢ B ⇛ C) - -> interpEv (wk-ev (wk-wk {A = A *} (wk-id {Γ = Γ})) E) (< proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) - ≡ < proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval -interpEv-wk-coh' ø = refl -interpEv-wk-coh' {e = e1} (app-r e E) = - interpEv (wk-ev π1 (app-r e E)) (< proj₁ ； interpTm e1 ； T.map inj₁ , proj₂ > ； couneval) ≡⟨ refl ⟩ - interpEv (app-r (wk-tm π1 e) (wk-ev π1 E)) (< proj₁ ； interpTm e1 ； T.map inj₁ , proj₂ > ； couneval) ≡⟨ refl ⟩ - < interpTm (wk-tm π1 e) , interpEv (wk-ev π1 E) (< proj₁ ； interpTm e1 ； T.map inj₁ , proj₂ > ； couneval) > ； T.beta ； T.map eval ； T.mu ≡⟨ cong (\f -> < interpTm (wk-tm π1 e) , f > ； T.beta ； T.map eval ； T.mu) (interpEv-wk-coh' {e = e1} E) ⟩ - < proj₁ ； interpTm e1 ； T.map inj₁ , proj₂ > ； couneval ∎ - where open ≡-Reasoning - π1 = wk-wk wk-id -interpEv-wk-coh' {e = e} (app-l E v {{ϕ}}) = - interpEv (wk-ev π1 (app-l E v)) (< proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) ≡⟨ refl ⟩ - interpEv (app-l (wk-ev π1 E) (wk-tm π1 v) {{wk-tm-val π1 v ϕ}}) (< proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) ≡⟨ refl ⟩ - < interpEv (wk-ev π1 E) (< proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) , interpVal (wk-tm π1 v) (wk-tm-val π1 v ϕ) > ； T.sigma ； T.map eval ； T.mu ≡⟨ cong (\f -> < interpEv (wk-ev π1 E) (< proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) , f > ； T.sigma ； T.map eval ； T.mu) (interpVal-wk-coh π1 v ϕ) ⟩ - < interpEv (wk-ev π1 E) (< proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) , proj₁ ； interpVal v ϕ > ； T.sigma ； T.map eval ； T.mu ≡⟨ cong (\f -> < f , proj₁ ； interpVal v ϕ > ； T.sigma ； T.map eval ； T.mu) (interpEv-wk-coh' {e = e} E) ⟩ - < < proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval , proj₁ ； interpVal v ϕ > ； T.sigma ； T.map eval ； T.mu ≡⟨ refl ⟩ - < proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval ∎ - where open ≡-Reasoning - π1 = wk-wk wk-id - -interpEv-wk-coh'' : (e : Γ ⊢ A `+ B) (e1 : (Γ ∙ A) ⊢ C) (e2 : (Γ ∙ B) ⊢ C) (E : Γ ⊢ C ⇛ D) - -> interpEv E (< id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) - ≡ < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev (wk-wk wk-id) E) (interpTm e1) , interpEv (wk-ev (wk-wk wk-id) E) (interpTm e2) ] ； T.mu -interpEv-wk-coh'' e e1 e2 ø = refl -interpEv-wk-coh'' e e1 e2 (app-r e3 E) = - interpEv (app-r e3 E) (< id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) ≡⟨ refl ⟩ - < interpTm e3 , interpEv E (< id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) > ； T.beta ； T.map eval ； T.mu ≡⟨ cong (\f -> < interpTm e3 , f > ； T.beta ； T.map eval ； T.mu) (interpEv-wk-coh'' e e1 e2 E) ⟩ - < interpTm e3 , < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev π1 E) (interpTm e1) , interpEv (wk-ev π2 E) (interpTm e2) ] ； T.mu > ； T.beta ； T.map eval ； T.mu ≡⟨ refl ⟩ - < interpTm e3 , < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev π1 E) (interpTm e1) , interpEv (wk-ev π2 E) (interpTm e2) ] ； T.mu > ； T.beta ； T.map eval ； T.mu ≡⟨ (funext \γ -> funext \k -> cong (interpTm e γ) (funext \{ (inj₁ x) -> refl ; (inj₂ y) -> refl } )) ⟩ - < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ < proj₁ ； interpTm e3 , interpEv (wk-ev π1 E) (interpTm e1) > ； T.beta ； T.map eval ； T.mu , < proj₁ ； interpTm e3 , interpEv (wk-ev π2 E) (interpTm e2) > ； T.beta ； T.map eval ； T.mu ] ； T.mu ≡⟨ refl ⟩ - < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ < interpTm (wk-tm π1 e3) , interpEv (wk-ev π1 E) (interpTm e1) > ； T.beta ； T.map eval ； T.mu , < interpTm (wk-tm π2 e3) , interpEv (wk-ev π2 E) (interpTm e2) > ； T.beta ； T.map eval ； T.mu ] ； T.mu ≡⟨ refl ⟩ - < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (app-r (wk-tm π1 e3) (wk-ev π1 E)) (interpTm e1) , interpEv (app-r (wk-tm π2 e3) (wk-ev π2 E)) (interpTm e2) ] ； T.mu ≡⟨ refl ⟩ - < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev π1 (app-r e3 E)) (interpTm e1) , interpEv (wk-ev π2 (app-r e3 E)) (interpTm e2) ] ； T.mu ∎ - where open ≡-Reasoning - π1 = wk-wk wk-id - π2 = wk-wk wk-id -interpEv-wk-coh'' e e1 e2 (app-l E v {{ϕ}}) = - interpEv (app-l E v) (< id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) ≡⟨ refl ⟩ - < interpEv E (< id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) , interpVal v ϕ > ； T.sigma ； T.map eval ； T.mu ≡⟨ cong (\f -> < f , interpVal v ϕ > ； T.sigma ； T.map eval ； T.mu) (interpEv-wk-coh'' e e1 e2 E) ⟩ - < < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev (wk-wk wk-id) E) (interpTm e1) , interpEv (wk-ev (wk-wk wk-id) E) (interpTm e2) ] ； T.mu , interpVal v ϕ > ； T.sigma ； T.map eval ； T.mu ≡⟨ (funext \γ -> funext \k -> cong (interpTm e γ) (funext \{ (inj₁ x) -> refl ; (inj₂ y) -> refl })) ⟩ - < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ < interpEv (wk-ev π1 E) (interpTm e1) , interpVal (wk-tm π1 v) (wk-tm-val π1 v ϕ) > ； T.sigma ； T.map eval ； T.mu , < interpEv (wk-ev π2 E) (interpTm e2) , interpVal (wk-tm π2 v) (wk-tm-val π2 v ϕ) > ； T.sigma ； T.map eval ； T.mu ] ； T.mu ≡⟨ refl ⟩ - < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (app-l (wk-ev π1 E) (wk-tm π1 v) {{wk-tm-val π1 v ϕ}}) (interpTm e1) , interpEv (app-l (wk-ev π2 E) (wk-tm π2 v) {{wk-tm-val π2 v ϕ}}) (interpTm e2) ] ； T.mu ≡⟨ refl ⟩ - < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev π1 (app-l E v)) (interpTm e1) , interpEv (wk-ev π2 (app-l E v)) (interpTm e2) ] ； T.mu ∎ - where open ≡-Reasoning - π1 = wk-wk wk-id - π2 = wk-wk wk-id - -interpEq : Γ ⊢ e1 ≈ e2 ∶ A -> interpTm e1 ≡ interpTm e2 -interpEq ≈-refl = refl -interpEq (≈-sym eq) = sym (interpEq eq) -interpEq (≈-trans eq1 eq2) = trans (interpEq eq1) (interpEq eq2) -interpEq (fst-cong eq) = cong (_； T.map proj₁) (interpEq eq) -interpEq (snd-cong eq) = cong (_； T.map proj₂) (interpEq eq) -interpEq (pair-cong eq1 eq2) = cong₂ (\f g -> < f , g > ； T.beta) (interpEq eq1) (interpEq eq2) -interpEq (fst-beta v1 {{ϕ1}} v2 {{ϕ2}}) = - interpTm (pair v1 v2) ； T.map proj₁ ≡⟨ cong (_； T.map proj₁) (interpVal-tm-coh (pair v1 v2) (pair {{ϕ1}} {{ϕ2}})) ⟩ - interpVal (pair v1 v2) (pair {{ϕ1}} {{ϕ2}}) ； T.eta ； T.map proj₁ ≡⟨ refl ⟩ - interpVal (pair v1 v2) (pair {{ϕ1}} {{ϕ2}}) ； proj₁ ； T.eta ≡⟨ refl ⟩ - interpVal v1 ϕ1 ； T.eta ≡⟨ sym (interpVal-tm-coh v1 ϕ1) ⟩ - interpTm v1 ∎ - where open ≡-Reasoning -interpEq (snd-beta v1 {{ϕ1}} v2 {{ϕ2}}) = - interpTm (pair v1 v2) ； T.map proj₂ ≡⟨ cong (_； T.map proj₂) (interpVal-tm-coh (pair v1 v2) (pair {{ϕ1}} {{ϕ2}})) ⟩ - interpVal (pair v1 v2) (pair {{ϕ1}} {{ϕ2}}) ； T.eta ； T.map proj₂ ≡⟨ refl ⟩ - interpVal (pair v1 v2) (pair {{ϕ1}} {{ϕ2}}) ； proj₂ ； T.eta ≡⟨ refl ⟩ - interpVal v2 ϕ2 ； T.eta ≡⟨ sym (interpVal-tm-coh v2 ϕ2) ⟩ - interpTm v2 ∎ - where open ≡-Reasoning -interpEq (pair-eta v {{ϕ}}) = - < interpTm v ； T.map proj₁ , interpTm v ； T.map proj₂ > ； T.beta ≡⟨ cong (\f -> < f ； T.map proj₁ , f ； T.map proj₂ > ； T.beta) (interpVal-tm-coh v ϕ) ⟩ - < interpVal v ϕ ； T.eta ； T.map proj₁ , interpVal v ϕ ； T.eta ； T.map proj₂ > ； T.beta ≡⟨ refl ⟩ - < interpVal v ϕ ； proj₁ ； T.eta , interpVal v ϕ ； proj₂ ； T.eta > ； T.beta ≡⟨ refl ⟩ - interpVal v ϕ ； T.eta ≡⟨ sym (interpVal-tm-coh v ϕ) ⟩ - interpTm v ∎ - where open ≡-Reasoning -interpEq (unit-eta v {{ϕ}}) = - interpTm v ≡⟨ interpVal-tm-coh v ϕ ⟩ - interpVal v ϕ ； T.eta ≡⟨ cong (_； T.eta) refl ⟩ - interpVal unit unit ； T.eta ≡⟨ sym (interpVal-tm-coh unit unit) ⟩ - interpTm unit ∎ - where open ≡-Reasoning -interpEq (lam-beta e v {{ϕ}}) = - < curry (interpTm e) ； T.eta , interpTm v > ； T.beta ； T.map eval ； T.mu ≡⟨ cong (\f -> < curry (interpTm e) ； T.eta , f > ； T.beta ； T.map eval ； T.mu) (interpVal-tm-coh v ϕ) ⟩ - < curry (interpTm e) ； T.eta , interpVal v ϕ ； T.eta > ； T.beta ； T.map eval ； T.mu ≡⟨ refl ⟩ - < curry (interpTm e), interpVal v ϕ > ； pmap T.eta T.eta ； T.beta ； T.map eval ； T.mu ≡⟨ refl ⟩ - < curry (interpTm e), interpVal v ϕ > ； T.eta ； T.map eval ； T.mu ≡⟨ refl ⟩ - < curry (interpTm e), interpVal v ϕ > ； eval ； T.eta ； T.mu ≡⟨ refl ⟩ - < curry (interpTm e), interpVal v ϕ > ； eval ≡⟨ refl ⟩ - < id , interpVal v ϕ > ； interpTm e ≡⟨ cong (\f -> < f , interpVal v ϕ > ； interpTm e) (sym interpSub-id-coh) ⟩ - < interpSub sub-id sub-id-sub , interpVal v ϕ > ； interpTm e ≡⟨ refl ⟩ - interpSub (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) ； interpTm e ≡⟨ sym (interpSub-tm-coh (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) e) ⟩ - interpTm (sub-tm (sub-ex sub-id v) e) ∎ - where open ≡-Reasoning -interpEq (lam-eta v {{ϕ}}) = - curry (< interpTm (wk-tm (wk-wk wk-id) v) , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta ≡⟨ cong (\f -> curry (< f , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta) (interpWk-tm-coh (wk-wk wk-id) v) ⟩ - curry (< interpWk (wk-wk wk-id) ； interpTm v , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta ≡⟨ cong (\f -> curry (< proj₁ ； f ； interpTm v , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta) interpWk-id-coh ⟩ - curry (< proj₁ ； interpTm v , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta ≡⟨ cong (\f -> curry (< proj₁ ； f , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta) (interpVal-tm-coh v ϕ) ⟩ - curry (< proj₁ ； interpVal v ϕ ； T.eta , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta ≡⟨ refl ⟩ - interpVal v ϕ ； T.eta ≡⟨ sym (interpVal-tm-coh v ϕ) ⟩ - interpTm v ∎ - where open ≡-Reasoning -interpEq (case-inl-beta v {{ϕ}} e2 e3) = - < id , interpTm v ； T.map inj₁ > ； T.tau ； T.map distl ； T.map S.[ interpTm e2 , interpTm e3 ] ； T.mu ≡⟨ cong (\f -> < id , f ； T.map inj₁ > ； T.tau ； T.map distl ； T.map S.[ interpTm e2 , interpTm e3 ] ； T.mu) (interpVal-tm-coh v ϕ) ⟩ - < id , interpVal v ϕ ； T.eta ； T.map inj₁ > ； T.tau ； T.map distl ； T.map S.[ interpTm e2 , interpTm e3 ] ； T.mu ≡⟨ refl ⟩ - < id , interpVal v ϕ > ； interpTm e2 ≡⟨ cong (\f -> < f , interpVal v ϕ > ； interpTm e2) (sym interpSub-id-coh) ⟩ - < interpSub sub-id sub-id-sub , interpVal v ϕ > ； interpTm e2 ≡⟨ refl ⟩ - interpSub (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) ； interpTm e2 ≡⟨ sym (interpSub-tm-coh (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) e2) ⟩ - interpTm (sub-tm (sub-ex sub-id v) e2) ∎ - where open ≡-Reasoning -interpEq (case-inr-beta v {{ϕ}} e2 e3) = - < id , interpTm v ； T.map inj₂ > ； T.tau ； T.map distl ； T.map S.[ interpTm e2 , interpTm e3 ] ； T.mu ≡⟨ cong (\f -> < id , f ； T.map inj₂ > ； T.tau ； T.map distl ； T.map S.[ interpTm e2 , interpTm e3 ] ； T.mu) (interpVal-tm-coh v ϕ) ⟩ - < id , interpVal v ϕ ； T.eta ； T.map inj₂ > ； T.tau ； T.map distl ； T.map S.[ interpTm e2 , interpTm e3 ] ； T.mu ≡⟨ refl ⟩ - < id , interpVal v ϕ > ； interpTm e3 ≡⟨ cong (\f -> < f , interpVal v ϕ > ； interpTm e3) (sym interpSub-id-coh) ⟩ - < interpSub sub-id sub-id-sub , interpVal v ϕ > ； interpTm e3 ≡⟨ refl ⟩ - interpSub (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) ； interpTm e3 ≡⟨ sym (interpSub-tm-coh (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) e3) ⟩ - interpTm (sub-tm (sub-ex sub-id v) e3) ∎ - where open ≡-Reasoning -interpEq (colam-beta e v {{ϕ}}) = - < councurry (interpTm e) , interpTm v > ； T.tau ； T.map couneval ； T.mu ≡⟨ cong (\f -> < councurry (interpTm e) , f > ； T.tau ； T.map couneval ； T.mu) (interpVal-tm-coh v ϕ) ⟩ - < councurry (interpTm e) , interpVal v ϕ ； T.eta > ； T.tau ； T.map couneval ； T.mu ≡⟨ refl ⟩ - < councurry (interpTm e) , interpVal v ϕ > ； couneval ≡⟨ refl ⟩ - < id , interpVal v ϕ > ； interpTm e ≡⟨ cong (\f -> < f , interpVal v ϕ > ； interpTm e) (sym interpSub-id-coh) ⟩ - < interpSub sub-id sub-id-sub , interpVal v ϕ > ； interpTm e ≡⟨ refl ⟩ - interpSub (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) ； interpTm e ≡⟨ sym (interpSub-tm-coh (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) e) ⟩ - interpTm (sub-tm (sub-ex sub-id v) e) ∎ - where open ≡-Reasoning -interpEq (colam-eta {A = A} e) = - councurry (< interpTm (wk-tm π1 e) , interpTm {A = A *} (var h) > ； T.tau ； T.map couneval ； T.mu) ≡⟨ cong (\f -> councurry (< f , interpTm {A = A *} (var h) > ； T.tau ； T.map couneval ； T.mu)) (interpWk-tm-coh π1 e) ⟩ - councurry (< interpWk π1 ； interpTm e , interpTm {A = A *} (var h) > ； T.tau ； T.map couneval ； T.mu) ≡⟨ cong (\f -> councurry (< f ； interpTm e , interpTm {A = A *} (var h) > ； T.tau ； T.map couneval ； T.mu)) (cong (proj₁ ；_) interpWk-id-coh) ⟩ - councurry (< proj₁ ； interpTm e , interpTm {A = A *} (var h) > ； T.tau ； T.map (cocurry id) ； T.mu) ≡⟨ refl ⟩ - councurry (cocurry (interpTm e)) ≡⟨ councurry-cocurry (interpTm e) ⟩ - interpTm e ∎ - where open ≡-Reasoning - π1 = wk-wk {A = A *} wk-id - -interpEq (colam-const {A = A} e) = - councurry (interpTm (wk-tm π1 e)) ≡⟨ cong councurry (interpWk-tm-coh π1 e) ⟩ - councurry (interpWk π1 ； interpTm e) ≡⟨ cong councurry (cong (\f -> proj₁ ； f ； interpTm e) interpWk-id-coh) ⟩ - councurry (proj₁ ； interpTm e) ≡⟨ refl ⟩ - interpTm e ； T.map inj₂ ∎ - where open ≡-Reasoning - π1 = wk-wk {A = A *} wk-id - -interpEq (colam-inr-pass e E) = - interpTm (colam (wk-ev π1 E [[ coapp (inr (wk e)) (var h) ]])) ≡⟨ refl ⟩ - councurry (interpTm (wk-ev π1 E [[ coapp (inr (wk e)) (var h) ]])) ≡⟨ cong councurry (interpWk-ev-coh' π1 E (coapp (inr (wk e)) (var h))) ⟩ - councurry (interpEv (wk-ev π1 E) (< interpWk π1 ； interpTm e ； T.map inj₂ , proj₂ > ； couneval)) ≡⟨ refl ⟩ - councurry (interpEv (wk-ev π1 E) (interpWk π1 ； interpTm e)) ≡⟨ cong councurry (interpEv-wk-coh π1 E (interpTm e)) ⟩ - councurry (interpWk π1 ； interpEv E (interpTm e)) ≡⟨ refl ⟩ - interpEv E (interpTm e) ； T.map inj₂ ≡⟨ refl ⟩ - interpTm (E [[ e ]]) ； T.map inj₂ ≡⟨ refl ⟩ - interpTm (inr (E [[ e ]])) ∎ - where open ≡-Reasoning - π1 = wk-wk wk-id - -interpEq (colam-inl-jump e E) = - interpTm (colam (wk-ev π1 E [[ coapp (inl (wk e)) (var h) ]])) ≡⟨ refl ⟩ - councurry (interpTm (wk-ev π1 E [[ coapp (inl (wk e)) (var h) ]])) ≡⟨ cong councurry (interpWk-ev-coh' π1 E (coapp (inl (wk e)) (var h))) ⟩ - councurry (interpEv (wk-ev π1 E) (< interpWk π1 ； interpTm e ； T.map inj₁ , proj₂ ； T.eta > ； T.tau ； T.map couneval ； T.mu)) ≡⟨ refl ⟩ - councurry (interpEv (wk-ev π1 E) (< interpWk π1 ； interpTm e ； T.map inj₁ , proj₂ > ； couneval)) ≡⟨ cong councurry (interpEv-wk-coh' {e = e} E) ⟩ - councurry (< interpWk π1 ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) ≡⟨ councurry-cocurry (interpTm e ； T.map inj₁) ⟩ - interpTm e ； T.map inj₁ ≡⟨ refl ⟩ - interpTm (inl e) ∎ - where open ≡-Reasoning - π1 = wk-wk wk-id - -interpEq (case-colam-beta v {{ϕ}} e1 e2) = - interpTm (case (colam v) e1 e2) ≡⟨ refl ⟩ - < id , councurry (interpTm v) > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu ≡⟨ cong (\f -> < id , councurry f > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) (interpVal-tm-coh v ϕ) ⟩ - < id , councurry (interpVal v ϕ ； T.eta) > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu ≡⟨ refl ⟩ - < id , councurry (interpSub θ1 ϕ1 ； interpTm e2) > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm (var h) ] ； T.mu ≡⟨ cong (\f -> < id , councurry f > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm (var h) ] ； T.mu) (sym (interpSub-tm-coh θ1 ϕ1 e2)) ⟩ - < id , councurry (interpTm (sub-tm θ1 e2)) > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm (var h) ] ； T.mu ≡⟨ refl ⟩ - interpTm (case (colam (sub-tm θ1 e2)) e1 (var h)) ∎ - where open ≡-Reasoning - θ1 = sub-ex (sub-wk (wk-wk wk-id) sub-id) v - ϕ1 = sub-ex (sub-wk-sub (wk-wk wk-id) sub-id sub-id-sub) ϕ - -interpEq (case-zeta e e1 e2 E) = - interpTm (E [[ case e e1 e2 ]]) ≡⟨ refl ⟩ - interpEv E (< id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) ≡⟨ interpEv-wk-coh'' e e1 e2 E ⟩ - < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev π1 E) (interpTm e1) , interpEv (wk-ev π2 E) (interpTm e2) ] ； T.mu ≡⟨ refl ⟩ - < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm (wk-ev π1 E [[ e1 ]]) , interpTm (wk-ev π2 E [[ e2 ]]) ] ； T.mu ≡⟨ refl ⟩ - interpTm (case e (wk-ev π1 E [[ e1 ]]) (wk-ev π2 E [[ e2 ]])) ∎ - where open ≡-Reasoning - π1 = wk-wk wk-id - π2 = wk-wk wk-id +interpTy `Nat = ℕ +interpTy `Unit = ⊤ +interpTy (A *) = interpTy A -> R +interpTy (A `× B) = interpTy A × interpTy B +interpTy (A `⇒ B) = interpTy A -> T (interpTy B) +interpTy (A `+ B) = interpTy A ⊎ interpTy B + +-- interpretation of contexts +interpCtx : Ctx -> Set +interpCtx ε = ⊤ +interpCtx (Γ ∙ A) = interpCtx Γ × interpTy A + +-- interpretation of membership +interpIn : A ∈ Γ -> interpCtx Γ -> interpTy A +interpIn h = proj₂ +interpIn (t i) = proj₁ ； interpIn i + +-- interpretation of terms +interpTm : Γ ⊢ A -> interpCtx Γ -> T (interpTy A) +interpTm (nat n) = + const n ； T.eta +interpTm (zero? e) = + interpTm e ； T.map is-zero +interpTm (var i) = + interpIn i ； T.eta +interpTm (lam e) = + curry (interpTm e) ； T.eta +interpTm (app e1 e2) = + let f = interpTm e1 ; x = interpTm e2 + in < f , x > ； T.beta ； T.map eval ； T.mu +interpTm (pair e1 e2) = + let f = interpTm e1 ; g = interpTm e2 + in < f , g > ； T.beta +interpTm (fst e) = + interpTm e ； T.map proj₁ +interpTm (snd e) = + interpTm e ； T.map proj₂ +interpTm unit = + const tt ； T.eta +interpTm (inl e) = + interpTm e ； T.map inj₁ +interpTm (inr e) = + interpTm e ； T.map inj₂ +interpTm (case e e1 e2) = + let f = interpTm e ; g1 = interpTm e1 ; g2 = interpTm e2 + in < id , f > ； T.tau ； T.map distl ； T.map S.[ g1 , g2 ] ； T.mu +interpTm (colam e) = + councurry (interpTm e) +interpTm (coapp e1 e2) = + let f = interpTm e1 ; g = interpTm e2 + in < f , g > ； T.tau ； T.map couneval ； T.mu + +-- interpretation of weakening +interpWk : Wk Γ Δ -> interpCtx Γ -> interpCtx Δ +interpWk wk-ε = const tt +interpWk (wk-cong π) = pmap (interpWk π) id +interpWk (wk-wk π) = proj₁ ； interpWk π + +interpWk-id-coh : interpWk (wk-id {Γ}) ≡ id +interpWk-id-coh {Γ = ε} = refl +interpWk-id-coh {Γ = Γ ∙ A} rewrite interpWk-id-coh {Γ = Γ} = refl +{-# REWRITE interpWk-id-coh #-} + +interpWk-mem-coh : (π : Wk Γ Δ) (i : A ∈ Δ) -> interpIn (wk-mem π i) ≡ interpWk π ； interpIn i +interpWk-mem-coh (wk-cong π) h = refl +interpWk-mem-coh (wk-cong π) (t i) rewrite interpWk-mem-coh π i = refl +interpWk-mem-coh (wk-wk π) h rewrite interpWk-mem-coh π h = refl +interpWk-mem-coh (wk-wk π) (t i) rewrite interpWk-mem-coh π (t i) = refl + +interpWk-tm-coh : (π : Wk Γ Δ) (e : Δ ⊢ A) -> interpTm (wk-tm π e) ≡ interpWk π ； interpTm e +interpWk-tm-coh π (nat n) = refl +interpWk-tm-coh π (zero? e) rewrite interpWk-tm-coh π e = refl +interpWk-tm-coh π (var i) rewrite interpWk-mem-coh π i = refl +interpWk-tm-coh π (lam e) rewrite (interpWk-tm-coh (wk-cong π) e) = refl +interpWk-tm-coh π (app e1 e2) rewrite interpWk-tm-coh π e1 | interpWk-tm-coh π e2 = refl +interpWk-tm-coh π (pair e1 e2) rewrite interpWk-tm-coh π e1 | interpWk-tm-coh π e2 = refl +interpWk-tm-coh π (fst e) rewrite interpWk-tm-coh π e = refl +interpWk-tm-coh π (snd e) rewrite interpWk-tm-coh π e = refl +interpWk-tm-coh π unit = refl +interpWk-tm-coh π (inl e) rewrite interpWk-tm-coh π e = refl +interpWk-tm-coh π (inr e) rewrite interpWk-tm-coh π e = refl +interpWk-tm-coh π (case e1 e2 e3) rewrite interpWk-tm-coh π e1 | interpWk-tm-coh (wk-cong π) e2 | interpWk-tm-coh (wk-cong π) e3 = + funext \γ -> funext \k -> cong (interpTm e1 (interpWk π γ)) (funext \{ (inj₁ a) -> refl ; (inj₂ b) -> refl }) +interpWk-tm-coh π (colam e) rewrite interpWk-tm-coh (wk-cong π) e = refl +interpWk-tm-coh π (coapp e1 e2) rewrite interpWk-tm-coh π e1 | interpWk-tm-coh π e2 = refl +{-# REWRITE interpWk-tm-coh #-} + +-- interpretation of values +interpVal : (e : Γ ⊢ A) -> {{ϕ : isVal e}} -> interpCtx Γ -> interpTy A +interpVal (nat n) {{nat}} = const n +interpVal (zero? e) {{zero?}} = interpVal e ； is-zero +interpVal (var i) {{var}} = interpIn i +interpVal (lam e) {{lam}} = curry (interpTm e) +interpVal (fst e) {{fst}} = interpVal e ； proj₁ +interpVal (snd e) {{snd}} = interpVal e ； proj₂ +interpVal (pair e1 e2) {{pair}} = < interpVal e1 , interpVal e2 > +interpVal unit {{unit}} = const tt +interpVal (inl e) {{inl}} = interpVal e ； inj₁ +interpVal (inr e) {{inr}} = interpVal e ； inj₂ + +-- value interpretation coherence lemma +interpVal-tm-coh : (e : Γ ⊢ A) {{ϕ : isVal e}} -> interpTm e ≡ interpVal e ； T.eta +interpVal-tm-coh (nat n) {{nat}} = refl +interpVal-tm-coh (zero? e) {{zero? {{ϕ}}}} + rewrite interpVal-tm-coh e {{ϕ}} = refl +interpVal-tm-coh (var i) {{var}} = refl +interpVal-tm-coh (lam e) {{lam}} = refl +interpVal-tm-coh (fst e) {{fst {{ϕ}}}} + rewrite interpVal-tm-coh e {{ϕ}} = refl +interpVal-tm-coh (snd e) {{snd {{ϕ}}}} + rewrite interpVal-tm-coh e {{ϕ}} = refl +interpVal-tm-coh (pair e1 e2) {{pair {{ϕ1}} {{ϕ2}}}} + rewrite interpVal-tm-coh e1 {{ϕ1}} | interpVal-tm-coh e2 {{ϕ2}} = refl +interpVal-tm-coh unit {{unit}} = refl +interpVal-tm-coh (inl e) {{inl {{ϕ}}}} + rewrite interpVal-tm-coh e {{ϕ}} = refl +interpVal-tm-coh (inr e) {{inr {{ϕ}}}} + rewrite interpVal-tm-coh e {{ϕ}} = refl + +interpVal-wk-coh : (π : Wk Γ Δ) (v : Δ ⊢ A) {{ϕ : isVal v}} -> interpVal (wk-tm π v) {{wk-tm-val π v}} ≡ interpWk π ； interpVal v +interpVal-wk-coh π (nat n) {{nat}} = refl +interpVal-wk-coh π (zero? v) {{zero? {{ϕ}}}} rewrite interpVal-wk-coh π v {{ϕ}} = refl +interpVal-wk-coh π (var i) {{var}} = interpWk-mem-coh π i +interpVal-wk-coh π (lam e) {{lam}} rewrite interpWk-tm-coh (wk-cong π) e = refl +interpVal-wk-coh π (fst v) {{fst {{ϕ}}}} rewrite interpVal-wk-coh π v {{ϕ}} = refl +interpVal-wk-coh π (snd v) {{snd {{ϕ}}}} rewrite interpVal-wk-coh π v {{ϕ}} = refl +interpVal-wk-coh π (pair v1 v2) {{pair {{ϕ1}} {{ϕ2}}}} rewrite interpVal-wk-coh π v1 {{ϕ1}} | interpVal-wk-coh π v2 {{ϕ2}} = refl +interpVal-wk-coh π unit {{unit}} = refl +interpVal-wk-coh π (inl v) {{inl {{ϕ}}}} rewrite interpVal-wk-coh π v {{ϕ}} = refl +interpVal-wk-coh π (inr v) {{inr {{ϕ}}}} rewrite interpVal-wk-coh π v {{ϕ}} = refl +{-# REWRITE interpVal-wk-coh #-} + +open Val isVal + +-- interpretation of substitutions +interpSub : (θ : Sub Γ Δ) (ϕ : isSub θ) -> interpCtx Γ -> interpCtx Δ +interpSub sub-ε sub-ε = const tt +interpSub (sub-ex θ v) (sub-ex ϕ ψ) = < interpSub θ ϕ , interpVal v {{ψ}} > + +interpSub-wk-coh : (π : Wk Γ Δ) -> (θ : Sub Δ Ψ) (ϕ : isSub θ) -> interpSub (sub-wk π θ) (sub-wk-sub π θ ϕ) ≡ interpWk π ； interpSub θ ϕ +interpSub-wk-coh π sub-ε sub-ε = refl +interpSub-wk-coh π (sub-ex θ v) (sub-ex ϕ ψ) rewrite interpSub-wk-coh π θ ϕ | interpVal-wk-coh π v {{ψ}} = refl +{-# REWRITE interpSub-wk-coh #-} + +interpSub-id-coh : {Γ : Ctx} -> interpSub (sub-id {Γ}) (sub-id-sub {Γ}) ≡ id +interpSub-id-coh {ε} = refl +interpSub-id-coh {Γ ∙ A} = + < interpSub (sub-wk (wk-wk wk-id) sub-id) (sub-wk-sub (wk-wk wk-id) sub-id sub-id-sub) , proj₂ > ≡⟨ cong (\f -> < f , proj₂ >) (interpSub-wk-coh (wk-wk wk-id) (sub-id {Γ}) sub-id-sub) ⟩ + < proj₁ ； interpWk wk-id ； interpSub sub-id sub-id-sub , proj₂ > ≡⟨ cong (\f -> < proj₁ ； interpWk wk-id ； f , proj₂ >) (interpSub-id-coh {Γ}) ⟩ + < proj₁ ； interpWk wk-id , proj₂ > ≡⟨ cong (\f -> < proj₁ ； f , proj₂ >) interpWk-id-coh ⟩ + id ∎ + where open ≡-Reasoning +{-# REWRITE interpSub-id-coh #-} + +interpSub-mem-val-coh : (θ : Sub Γ Δ) (ϕ : isSub θ) (i : A ∈ Δ) -> interpVal (sub-mem θ i) {{sub-mem-val θ ϕ i}} ≡ interpSub θ ϕ ； interpIn i +interpSub-mem-val-coh (sub-ex θ e) (sub-ex ϕ ψ) h = refl +interpSub-mem-val-coh (sub-ex θ e) (sub-ex ϕ ψ) (t i) rewrite interpSub-mem-val-coh θ ϕ i = refl + +interpSub-mem-tm-coh : (θ : Sub Γ Δ) (ϕ : isSub θ) (i : A ∈ Δ) -> interpTm (sub-mem θ i) ≡ interpSub θ ϕ ； interpIn i ； T.eta +interpSub-mem-tm-coh θ ϕ i rewrite interpVal-tm-coh (sub-mem θ i) {{sub-mem-val θ ϕ i}} | interpSub-mem-val-coh θ ϕ i = refl + +interpSub-tm-coh : (θ : Sub Γ Δ) (ϕ : isSub θ) -> (e : Δ ⊢ A) -> interpTm (sub-tm θ e) ≡ interpSub θ ϕ ； interpTm e +interpSub-tm-coh θ ϕ (nat n) = refl +interpSub-tm-coh θ ϕ (zero? e) rewrite interpSub-tm-coh θ ϕ e = refl +interpSub-tm-coh θ ϕ (var i) rewrite interpSub-mem-tm-coh θ ϕ i = refl +interpSub-tm-coh θ ϕ (lam e) = + curry (interpTm (sub-tm δ2 e)) ； T.eta ≡⟨ cong (\h -> curry h ； T.eta) (interpSub-tm-coh δ2 ψ2 e) ⟩ + curry (interpSub δ2 ψ2 ； interpTm e) ； T.eta ≡⟨ refl ⟩ + curry (< interpSub δ1 ψ1 , proj₂ > ； interpTm e) ； T.eta ≡⟨ cong (\h -> curry (< h , proj₂ > ； interpTm e) ； T.eta) (interpSub-wk-coh π1 θ ϕ) ⟩ + curry (< interpWk π1 ； interpSub θ ϕ , proj₂ > ； interpTm e) ； T.eta ≡⟨ cong (\h -> curry (< proj₁ ； h ； interpSub θ ϕ , proj₂ > ； interpTm e) ； T.eta) interpWk-id-coh ⟩ + curry (< proj₁ ； interpSub θ ϕ , proj₂ > ； interpTm e) ； T.eta ≡⟨ refl ⟩ + interpSub θ ϕ ； interpTm (lam e) ∎ + where open ≡-Reasoning + π1 = wk-wk wk-id + δ1 = sub-wk π1 θ ; ψ1 = sub-wk-sub π1 θ ϕ + δ2 = sub-ex δ1 (var h) ; ψ2 = sub-ex ψ1 var +interpSub-tm-coh θ ϕ (app e1 e2) rewrite interpSub-tm-coh θ ϕ e1 | interpSub-tm-coh θ ϕ e2 = refl +interpSub-tm-coh θ ϕ (pair e1 e2) rewrite interpSub-tm-coh θ ϕ e1 | interpSub-tm-coh θ ϕ e2 = refl +interpSub-tm-coh θ ϕ (fst e) rewrite interpSub-tm-coh θ ϕ e = refl +interpSub-tm-coh θ ϕ (snd e) rewrite interpSub-tm-coh θ ϕ e = refl +interpSub-tm-coh θ ϕ unit = refl +interpSub-tm-coh θ ϕ (inl e) rewrite interpSub-tm-coh θ ϕ e = refl +interpSub-tm-coh θ ϕ (inr e) rewrite interpSub-tm-coh θ ϕ e = refl +interpSub-tm-coh {Γ = Γ} θ ϕ (case {A = A} {B} e1 e2 e3) rewrite + interpSub-tm-coh θ ϕ e1 + | interpSub-tm-coh (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) (sub-ex (sub-wk-sub (wk-wk wk-id) θ ϕ) var) e2 + | interpSub-tm-coh (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) (sub-ex (sub-wk-sub (wk-wk wk-id) θ ϕ) var) e3 + | interpSub-wk-coh (wk-wk {A = A} wk-id) θ ϕ | interpSub-wk-coh (wk-wk {A = B} wk-id) θ ϕ + | interpWk-id-coh {Γ = Γ} = + funext \γ -> funext \k -> cong (interpTm e1 (interpSub θ ϕ γ)) (funext \{ (inj₁ a) -> refl ; (inj₂ b) -> refl }) +interpSub-tm-coh θ ϕ (colam e) = + councurry (interpTm (sub-tm δ2 e)) ≡⟨ cong councurry (interpSub-tm-coh δ2 ψ2 e) ⟩ + councurry (interpSub δ2 ψ2 ； interpTm e) ≡⟨ refl ⟩ + councurry (< interpSub δ1 ψ1 , proj₂ > ； interpTm e) ≡⟨ cong (\h -> councurry (< h , proj₂ > ； interpTm e)) (interpSub-wk-coh π1 θ ϕ) ⟩ + councurry (< interpWk π1 ； interpSub θ ϕ , proj₂ > ； interpTm e) ≡⟨ cong (\h -> councurry (< proj₁ ； h ； interpSub θ ϕ , proj₂ > ； interpTm e)) interpWk-id-coh ⟩ + councurry (< proj₁ ； interpSub θ ϕ , proj₂ > ； interpTm e) ≡⟨ refl ⟩ + interpSub θ ϕ ； interpTm (colam e) ∎ + where open ≡-Reasoning + π1 = wk-wk wk-id + δ1 = sub-wk π1 θ ; ψ1 = sub-wk-sub π1 θ ϕ + δ2 = sub-ex δ1 (var h) ; ψ2 = sub-ex ψ1 var +interpSub-tm-coh θ ϕ (coapp e1 e2) rewrite interpSub-tm-coh θ ϕ e1 | interpSub-tm-coh θ ϕ e2 = refl + +-- continuation semantics +lookup : A ∈ Γ -> interpCtx Γ -> interpTy A +lookup = interpIn + +evalTm : Γ ⊢ A -> interpCtx Γ -> (interpTy A -> R) -> R +evalTm (nat n) γ k = + k n +evalTm (zero? e) γ k = + evalTm e γ \n -> + k (is-zero n) +evalTm (var i) γ k = + k (lookup i γ) +evalTm (lam e) γ k = + k \a kb -> evalTm e (γ , a) kb +evalTm (app e1 e2) γ k = + evalTm e2 γ \a -> + evalTm e1 γ \f -> + f a k +evalTm (pair e1 e2) γ k = + evalTm e2 γ \b -> + evalTm e1 γ \a -> + k (a , b) +evalTm (fst e) γ k = + evalTm e γ \p -> + k (proj₁ p) +evalTm (snd e) γ k = + evalTm e γ \p -> + k (proj₂ p) +evalTm unit γ k = + k tt +evalTm (inl e) γ k = + evalTm e γ \a -> + k (inj₁ a) +evalTm (inr e) γ k = + evalTm e γ \b -> + k (inj₂ b) +evalTm (case e1 e2 e3) γ k = + evalTm e1 γ + \{ (inj₁ a) -> evalTm e2 (γ , a) k + ; (inj₂ b) -> evalTm e3 (γ , b) k } +evalTm (colam e) γ k = + let ka = \a -> k (inj₁ a) + kb = \b -> k (inj₂ b) + in evalTm e (γ , ka) kb +evalTm (coapp e1 e2) γ k = + evalTm e2 γ \ka -> + evalTm e1 γ + \{ (inj₁ a) -> ka a + ; (inj₂ b) -> k b } + +_ : evalTm {Γ = ε} (colam (zero? (coapp (inl (nat 1)) (var h)))) tt ≡ \k -> k (inj₁ 1) +_ = refl + +_ : ∀ A -> evalTm {Γ = ε} (colam {A = A} (var h)) tt ≡ \k -> k (inj₂ (\a -> k (inj₁ a))) +_ = \A -> refl + +-- both semantics agree +-- +adequacy : (e : Γ ⊢ A) -> interpTm e ≡ evalTm e +adequacy (nat n) = refl +adequacy (zero? e) rewrite adequacy e = refl +adequacy (var x) = refl +adequacy (lam e) rewrite adequacy e = refl +adequacy (app e1 e2) rewrite adequacy e1 | adequacy e2 = refl +adequacy (pair e1 e2) rewrite adequacy e1 | adequacy e2 = refl +adequacy (fst e) rewrite adequacy e = refl +adequacy (snd e) rewrite adequacy e = refl +adequacy unit = refl +adequacy (inl e) rewrite adequacy e = refl +adequacy (inr e) rewrite adequacy e = refl +adequacy (case e1 e2 e3) rewrite adequacy e1 | adequacy e2 | adequacy e3 = + funext \γ -> funext \k -> + cong (evalTm e1 γ) (funext \{ (inj₁ a) -> refl ; (inj₂ b) -> refl }) +adequacy (colam e) rewrite adequacy e = refl +adequacy (coapp e1 e2) rewrite adequacy e1 | adequacy e2 = + funext \γ -> funext \k -> + cong (evalTm e2 γ) (funext \k1 -> cong (evalTm e1 γ) (funext \{ (inj₁ a) -> refl ; (inj₂ b) -> refl })) + +-- soundness of equational theory + +interpWk-ev-coh : (π : Wk Γ Δ) (E : Δ ⊢ A ⇛ B) (e : Δ ⊢ A) -> interpTm (wk-ev π E [[ wk-tm π e ]]) ≡ interpWk π ； interpTm (E [[ e ]]) +interpWk-ev-coh π ø e = interpWk-tm-coh π e +interpWk-ev-coh π (app-r e1 E) e rewrite interpWk-tm-coh π e1 | interpWk-ev-coh π E e = refl +interpWk-ev-coh π (app-l E v) e rewrite interpWk-tm-coh π v | interpWk-ev-coh π E e = refl +{-# REWRITE interpWk-ev-coh #-} + +interpEv : Γ ⊢ C ⇛ A -> (f : interpCtx Γ -> T (interpTy C)) -> interpCtx Γ -> T (interpTy A) +interpEv ø = id +interpEv (app-r e E) f = + let x = interpEv E f ; g = interpTm e + in < g , x > ； T.beta ； T.map eval ； T.mu +interpEv (app-l E v) f = + let x = interpVal v ; g = interpEv E f + in < g , x > ； T.sigma ； T.map eval ； T.mu + +interpEv-Tm-coh : (E : Γ ⊢ A ⇛ B) (e : Γ ⊢ A) -> interpTm (E [[ e ]]) ≡ interpEv E (interpTm e) +interpEv-Tm-coh ø e = refl +interpEv-Tm-coh (app-r e1 E) e rewrite interpEv-Tm-coh E e = refl +interpEv-Tm-coh (app-l E v {{ϕ}}) e rewrite interpEv-Tm-coh E e | interpVal-tm-coh v {{ϕ}} = refl +{-# REWRITE interpEv-Tm-coh #-} + +interpWk-ev-coh' : (π : Wk Γ Δ) (E : Δ ⊢ A ⇛ B) (e : Γ ⊢ A) -> interpTm (wk-ev π E [[ e ]]) ≡ interpEv (wk-ev π E) (interpTm e) +interpWk-ev-coh' π ø e = refl +interpWk-ev-coh' π (app-r e1 E) e + rewrite interpWk-ev-coh' π E e = refl +interpWk-ev-coh' π (app-l E v {{ϕ}}) e = + interpTm (wk-ev π (app-l E v) [[ e ]]) ≡⟨ refl ⟩ + interpTm (app-l (wk-ev π E) (wk-tm π v) [[ e ]]) ≡⟨ refl ⟩ + interpTm (app (wk-ev π E [[ e ]]) (wk-tm π v)) ≡⟨ refl ⟩ + < interpTm (wk-ev π E [[ e ]]) , interpTm (wk-tm π v) > ； T.beta ； T.map eval ； T.mu ≡⟨ cong (\f -> < interpTm (wk-ev π E [[ e ]]) , f > ； T.beta ； T.map eval ； T.mu) (interpVal-tm-coh (wk-tm π v)) ⟩ + < interpTm (wk-ev π E [[ e ]]) , interpVal (wk-tm π v) ； T.eta > ； T.beta ； T.map eval ； T.mu ≡⟨ refl ⟩ + < interpTm (wk-ev π E [[ e ]]) , interpVal (wk-tm π v) > ； T.sigma ； T.map eval ； T.mu ≡⟨ refl ⟩ + < interpEv (wk-ev π E) (interpTm e) , interpVal (wk-tm π v) > ； T.sigma ； T.map eval ； T.mu ≡⟨ refl ⟩ + interpEv (app-l (wk-ev π E) (wk-tm π v)) (interpTm e) ≡⟨ refl ⟩ + interpEv (wk-ev π (app-l E v)) (interpTm e) ∎ + where open ≡-Reasoning + instance _ = wk-tm-val π v {{ϕ}} + +interpEv-wk-coh : (π : Wk Γ Δ) (E : Δ ⊢ A ⇛ B) (f : interpCtx Δ -> T (interpTy A)) -> interpEv (wk-ev π E) (interpWk π ； f) ≡ interpWk π ； interpEv E f +interpEv-wk-coh π ø f = refl +interpEv-wk-coh π (app-r e E) f rewrite interpEv-wk-coh π E f = refl +interpEv-wk-coh π (app-l E v {{ϕ}}) f rewrite interpEv-wk-coh π E f | interpVal-wk-coh π v {{ϕ}} = refl + +interpEv-wk-coh' : {e : Γ ⊢ A} (E : Γ ⊢ B ⇛ C) + -> interpEv (wk-ev (wk-wk {A = A *} (wk-id {Γ = Γ})) E) (< proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) + ≡ < proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval +interpEv-wk-coh' ø = refl +interpEv-wk-coh' {e = e1} (app-r e E) = + interpEv (wk-ev π1 (app-r e E)) (< proj₁ ； interpTm e1 ； T.map inj₁ , proj₂ > ； couneval) ≡⟨ refl ⟩ + interpEv (app-r (wk-tm π1 e) (wk-ev π1 E)) (< proj₁ ； interpTm e1 ； T.map inj₁ , proj₂ > ； couneval) ≡⟨ refl ⟩ + < interpTm (wk-tm π1 e) , interpEv (wk-ev π1 E) (< proj₁ ； interpTm e1 ； T.map inj₁ , proj₂ > ； couneval) > ； T.beta ； T.map eval ； T.mu ≡⟨ cong (\f -> < interpTm (wk-tm π1 e) , f > ； T.beta ； T.map eval ； T.mu) (interpEv-wk-coh' {e = e1} E) ⟩ + < proj₁ ； interpTm e1 ； T.map inj₁ , proj₂ > ； couneval ∎ + where open ≡-Reasoning + π1 = wk-wk wk-id +interpEv-wk-coh' {e = e} (app-l E v {{ϕ}}) = + interpEv (wk-ev π1 (app-l E v)) (< proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) ≡⟨ refl ⟩ + interpEv (app-l (wk-ev π1 E) (wk-tm π1 v)) (< proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) ≡⟨ refl ⟩ + < interpEv (wk-ev π1 E) (< proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) , interpVal (wk-tm π1 v) > ； T.sigma ； T.map eval ； T.mu ≡⟨ cong (\f -> < interpEv (wk-ev π1 E) (< proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) , f > ； T.sigma ； T.map eval ； T.mu) (interpVal-wk-coh π1 v) ⟩ + < interpEv (wk-ev π1 E) (< proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) , proj₁ ； interpVal v > ； T.sigma ； T.map eval ； T.mu ≡⟨ cong (\f -> < f , proj₁ ； interpVal v > ； T.sigma ； T.map eval ； T.mu) (interpEv-wk-coh' {e = e} E) ⟩ + < < proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval , proj₁ ； interpVal v > ； T.sigma ； T.map eval ； T.mu ≡⟨ refl ⟩ + < proj₁ ； interpTm e ； T.map inj₁ , proj₂ > ； couneval ∎ + where open ≡-Reasoning + π1 = wk-wk wk-id + instance _ = wk-tm-val π1 v {{ϕ}} + +interpEv-wk-coh'' : (e : Γ ⊢ A `+ B) (e1 : (Γ ∙ A) ⊢ C) (e2 : (Γ ∙ B) ⊢ C) (E : Γ ⊢ C ⇛ D) + -> interpEv E (< id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) + ≡ < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev (wk-wk wk-id) E) (interpTm e1) , interpEv (wk-ev (wk-wk wk-id) E) (interpTm e2) ] ； T.mu +interpEv-wk-coh'' e e1 e2 ø = refl +interpEv-wk-coh'' e e1 e2 (app-r e3 E) = + interpEv (app-r e3 E) (< id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) ≡⟨ refl ⟩ + < interpTm e3 , interpEv E (< id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) > ； T.beta ； T.map eval ； T.mu ≡⟨ cong (\f -> < interpTm e3 , f > ； T.beta ； T.map eval ； T.mu) (interpEv-wk-coh'' e e1 e2 E) ⟩ + < interpTm e3 , < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev π1 E) (interpTm e1) , interpEv (wk-ev π2 E) (interpTm e2) ] ； T.mu > ； T.beta ； T.map eval ； T.mu ≡⟨ refl ⟩ + < interpTm e3 , < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev π1 E) (interpTm e1) , interpEv (wk-ev π2 E) (interpTm e2) ] ； T.mu > ； T.beta ； T.map eval ； T.mu ≡⟨ (funext \γ -> funext \k -> cong (interpTm e γ) (funext \{ (inj₁ x) -> refl ; (inj₂ y) -> refl } )) ⟩ + < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ < proj₁ ； interpTm e3 , interpEv (wk-ev π1 E) (interpTm e1) > ； T.beta ； T.map eval ； T.mu , < proj₁ ； interpTm e3 , interpEv (wk-ev π2 E) (interpTm e2) > ； T.beta ； T.map eval ； T.mu ] ； T.mu ≡⟨ refl ⟩ + < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ < interpTm (wk-tm π1 e3) , interpEv (wk-ev π1 E) (interpTm e1) > ； T.beta ； T.map eval ； T.mu , < interpTm (wk-tm π2 e3) , interpEv (wk-ev π2 E) (interpTm e2) > ； T.beta ； T.map eval ； T.mu ] ； T.mu ≡⟨ refl ⟩ + < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (app-r (wk-tm π1 e3) (wk-ev π1 E)) (interpTm e1) , interpEv (app-r (wk-tm π2 e3) (wk-ev π2 E)) (interpTm e2) ] ； T.mu ≡⟨ refl ⟩ + < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev π1 (app-r e3 E)) (interpTm e1) , interpEv (wk-ev π2 (app-r e3 E)) (interpTm e2) ] ； T.mu ∎ + where open ≡-Reasoning + π1 = wk-wk wk-id + π2 = wk-wk wk-id +interpEv-wk-coh'' e e1 e2 (app-l E v {{ϕ}}) = + interpEv (app-l E v) (< id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) ≡⟨ refl ⟩ + < interpEv E (< id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) , interpVal v > ； T.sigma ； T.map eval ； T.mu ≡⟨ cong (\f -> < f , interpVal v > ； T.sigma ； T.map eval ； T.mu) (interpEv-wk-coh'' e e1 e2 E) ⟩ + < < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev (wk-wk wk-id) E) (interpTm e1) , interpEv (wk-ev (wk-wk wk-id) E) (interpTm e2) ] ； T.mu , interpVal v > ； T.sigma ； T.map eval ； T.mu ≡⟨ (funext \γ -> funext \k -> cong (interpTm e γ) (funext \{ (inj₁ x) -> refl ; (inj₂ y) -> refl })) ⟩ + < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ < interpEv (wk-ev π1 E) (interpTm e1) , interpVal (wk-tm π1 v) > ； T.sigma ； T.map eval ； T.mu , < interpEv (wk-ev π2 E) (interpTm e2) , interpVal (wk-tm π2 v) > ； T.sigma ； T.map eval ； T.mu ] ； T.mu ≡⟨ refl ⟩ + < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (app-l (wk-ev π1 E) (wk-tm π1 v)) (interpTm e1) , interpEv (app-l (wk-ev π2 E) (wk-tm π2 v)) (interpTm e2) ] ； T.mu ≡⟨ refl ⟩ + < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev π1 (app-l E v)) (interpTm e1) , interpEv (wk-ev π2 (app-l E v)) (interpTm e2) ] ； T.mu ∎ + where open ≡-Reasoning + π1 = wk-wk wk-id + π2 = wk-wk wk-id + instance _ = wk-tm-val π1 v {{ϕ}} + instance _ = wk-tm-val π2 v {{ϕ}} + +interpEq : Γ ⊢ e1 ≈ e2 ∶ A -> interpTm e1 ≡ interpTm e2 +interpEq ≈-refl = refl +interpEq (≈-sym eq) = sym (interpEq eq) +interpEq (≈-trans eq1 eq2) = trans (interpEq eq1) (interpEq eq2) +interpEq (fst-cong eq) = cong (_； T.map proj₁) (interpEq eq) +interpEq (snd-cong eq) = cong (_； T.map proj₂) (interpEq eq) +interpEq (pair-cong eq1 eq2) = cong₂ (\f g -> < f , g > ； T.beta) (interpEq eq1) (interpEq eq2) +interpEq (fst-beta v1 v2) = + interpTm (pair v1 v2) ； T.map proj₁ ≡⟨ cong (_； T.map proj₁) (interpVal-tm-coh (pair v1 v2)) ⟩ + interpVal (pair v1 v2) ； T.eta ； T.map proj₁ ≡⟨ refl ⟩ + interpVal (pair v1 v2) ； proj₁ ； T.eta ≡⟨ refl ⟩ + interpVal v1 ； T.eta ≡⟨ sym (interpVal-tm-coh v1) ⟩ + interpTm v1 ∎ + where open ≡-Reasoning +interpEq (snd-beta v1 v2) = + interpTm (pair v1 v2) ； T.map proj₂ ≡⟨ cong (_； T.map proj₂) (interpVal-tm-coh (pair v1 v2)) ⟩ + interpVal (pair v1 v2) ； T.eta ； T.map proj₂ ≡⟨ refl ⟩ + interpVal (pair v1 v2) ； proj₂ ； T.eta ≡⟨ refl ⟩ + interpVal v2 ； T.eta ≡⟨ sym (interpVal-tm-coh v2) ⟩ + interpTm v2 ∎ + where open ≡-Reasoning +interpEq (pair-eta v) = + < interpTm v ； T.map proj₁ , interpTm v ； T.map proj₂ > ； T.beta ≡⟨ cong (\f -> < f ； T.map proj₁ , f ； T.map proj₂ > ； T.beta) (interpVal-tm-coh v) ⟩ + < interpVal v ； T.eta ； T.map proj₁ , interpVal v ； T.eta ； T.map proj₂ > ； T.beta ≡⟨ refl ⟩ + < interpVal v ； proj₁ ； T.eta , interpVal v ； proj₂ ； T.eta > ； T.beta ≡⟨ refl ⟩ + interpVal v ； T.eta ≡⟨ sym (interpVal-tm-coh v) ⟩ + interpTm v ∎ + where open ≡-Reasoning +interpEq (unit-eta v) = + interpTm v ≡⟨ interpVal-tm-coh v ⟩ + interpVal v ； T.eta ≡⟨ cong (_； T.eta) refl ⟩ + interpVal unit ； T.eta ≡⟨ sym (interpVal-tm-coh unit) ⟩ + interpTm unit ∎ + where open ≡-Reasoning +interpEq (lam-beta e v {{ϕ}}) = + < curry (interpTm e) ； T.eta , interpTm v > ； T.beta ； T.map eval ； T.mu ≡⟨ cong (\f -> < curry (interpTm e) ； T.eta , f > ； T.beta ； T.map eval ； T.mu) (interpVal-tm-coh v) ⟩ + < curry (interpTm e) ； T.eta , interpVal v ； T.eta > ； T.beta ； T.map eval ； T.mu ≡⟨ refl ⟩ + < curry (interpTm e), interpVal v > ； pmap T.eta T.eta ； T.beta ； T.map eval ； T.mu ≡⟨ refl ⟩ + < curry (interpTm e), interpVal v > ； T.eta ； T.map eval ； T.mu ≡⟨ refl ⟩ + < curry (interpTm e), interpVal v > ； eval ； T.eta ； T.mu ≡⟨ refl ⟩ + < curry (interpTm e), interpVal v > ； eval ≡⟨ refl ⟩ + < id , interpVal v > ； interpTm e ≡⟨ cong (\f -> < f , interpVal v > ； interpTm e) (sym interpSub-id-coh) ⟩ + < interpSub sub-id sub-id-sub , interpVal v > ； interpTm e ≡⟨ refl ⟩ + interpSub (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) ； interpTm e ≡⟨ sym (interpSub-tm-coh (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) e) ⟩ + interpTm (sub-tm (sub-ex sub-id v) e) ∎ + where open ≡-Reasoning +interpEq (lam-eta v {{ϕ}}) = + curry (< interpTm (wk-tm (wk-wk wk-id) v) , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta ≡⟨ cong (\f -> curry (< f , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta) (interpWk-tm-coh (wk-wk wk-id) v) ⟩ + curry (< interpWk (wk-wk wk-id) ； interpTm v , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta ≡⟨ cong (\f -> curry (< proj₁ ； f ； interpTm v , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta) interpWk-id-coh ⟩ + curry (< proj₁ ； interpTm v , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta ≡⟨ cong (\f -> curry (< proj₁ ； f , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta) (interpVal-tm-coh v) ⟩ + curry (< proj₁ ； interpVal v ； T.eta , interpTm (var h) > ； T.beta ； T.map eval ； T.mu) ； T.eta ≡⟨ refl ⟩ + interpVal v ； T.eta ≡⟨ sym (interpVal-tm-coh v) ⟩ + interpTm v ∎ + where open ≡-Reasoning +interpEq (case-inl-beta v {{ϕ}} e2 e3) = + < id , interpTm v ； T.map inj₁ > ； T.tau ； T.map distl ； T.map S.[ interpTm e2 , interpTm e3 ] ； T.mu ≡⟨ cong (\f -> < id , f ； T.map inj₁ > ； T.tau ； T.map distl ； T.map S.[ interpTm e2 , interpTm e3 ] ； T.mu) (interpVal-tm-coh v) ⟩ + < id , interpVal v ； T.eta ； T.map inj₁ > ； T.tau ； T.map distl ； T.map S.[ interpTm e2 , interpTm e3 ] ； T.mu ≡⟨ refl ⟩ + < id , interpVal v > ； interpTm e2 ≡⟨ cong (\f -> < f , interpVal v > ； interpTm e2) (sym interpSub-id-coh) ⟩ + < interpSub sub-id sub-id-sub , interpVal v > ； interpTm e2 ≡⟨ refl ⟩ + interpSub (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) ； interpTm e2 ≡⟨ sym (interpSub-tm-coh (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) e2) ⟩ + interpTm (sub-tm (sub-ex sub-id v) e2) ∎ + where open ≡-Reasoning +interpEq (case-inr-beta v {{ϕ}} e2 e3) = + < id , interpTm v ； T.map inj₂ > ； T.tau ； T.map distl ； T.map S.[ interpTm e2 , interpTm e3 ] ； T.mu ≡⟨ cong (\f -> < id , f ； T.map inj₂ > ； T.tau ； T.map distl ； T.map S.[ interpTm e2 , interpTm e3 ] ； T.mu) (interpVal-tm-coh v) ⟩ + < id , interpVal v ； T.eta ； T.map inj₂ > ； T.tau ； T.map distl ； T.map S.[ interpTm e2 , interpTm e3 ] ； T.mu ≡⟨ refl ⟩ + < id , interpVal v > ； interpTm e3 ≡⟨ cong (\f -> < f , interpVal v > ； interpTm e3) (sym interpSub-id-coh) ⟩ + < interpSub sub-id sub-id-sub , interpVal v > ； interpTm e3 ≡⟨ refl ⟩ + interpSub (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) ； interpTm e3 ≡⟨ sym (interpSub-tm-coh (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) e3) ⟩ + interpTm (sub-tm (sub-ex sub-id v) e3) ∎ + where open ≡-Reasoning +interpEq (colam-beta e v {{ϕ}}) = + < councurry (interpTm e) , interpTm v > ； T.tau ； T.map couneval ； T.mu ≡⟨ cong (\f -> < councurry (interpTm e) , f > ； T.tau ； T.map couneval ； T.mu) (interpVal-tm-coh v) ⟩ + < councurry (interpTm e) , interpVal v ； T.eta > ； T.tau ； T.map couneval ； T.mu ≡⟨ refl ⟩ + < councurry (interpTm e) , interpVal v > ； couneval ≡⟨ refl ⟩ + < id , interpVal v > ； interpTm e ≡⟨ cong (\f -> < f , interpVal v > ； interpTm e) (sym interpSub-id-coh) ⟩ + < interpSub sub-id sub-id-sub , interpVal v > ； interpTm e ≡⟨ refl ⟩ + interpSub (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) ； interpTm e ≡⟨ sym (interpSub-tm-coh (sub-ex sub-id v) (sub-ex sub-id-sub ϕ) e) ⟩ + interpTm (sub-tm (sub-ex sub-id v) e) ∎ + where open ≡-Reasoning +interpEq (colam-eta {A = A} e) = + councurry (< interpTm (wk-tm π1 e) , interpTm {A = A *} (var h) > ； T.tau ； T.map couneval ； T.mu) ≡⟨ cong (\f -> councurry (< f , interpTm {A = A *} (var h) > ； T.tau ； T.map couneval ； T.mu)) (interpWk-tm-coh π1 e) ⟩ + councurry (< interpWk π1 ； interpTm e , interpTm {A = A *} (var h) > ； T.tau ； T.map couneval ； T.mu) ≡⟨ cong (\f -> councurry (< f ； interpTm e , interpTm {A = A *} (var h) > ； T.tau ； T.map couneval ； T.mu)) (cong (proj₁ ；_) interpWk-id-coh) ⟩ + councurry (< proj₁ ； interpTm e , interpTm {A = A *} (var h) > ； T.tau ； T.map (cocurry id) ； T.mu) ≡⟨ refl ⟩ + councurry (cocurry (interpTm e)) ≡⟨ councurry-cocurry (interpTm e) ⟩ + interpTm e ∎ + where open ≡-Reasoning + π1 = wk-wk {A = A *} wk-id + +interpEq (colam-const {A = A} e) = + councurry (interpTm (wk-tm π1 e)) ≡⟨ cong councurry (interpWk-tm-coh π1 e) ⟩ + councurry (interpWk π1 ； interpTm e) ≡⟨ cong councurry (cong (\f -> proj₁ ； f ； interpTm e) interpWk-id-coh) ⟩ + councurry (proj₁ ； interpTm e) ≡⟨ refl ⟩ + interpTm e ； T.map inj₂ ∎ + where open ≡-Reasoning + π1 = wk-wk {A = A *} wk-id + +interpEq (colam-inr-pass e E) = + interpTm (colam (wk-ev π1 E [[ coapp (inr (wk e)) (var h) ]])) ≡⟨ refl ⟩ + councurry (interpTm (wk-ev π1 E [[ coapp (inr (wk e)) (var h) ]])) ≡⟨ cong councurry (interpWk-ev-coh' π1 E (coapp (inr (wk e)) (var h))) ⟩ + councurry (interpEv (wk-ev π1 E) (< interpWk π1 ； interpTm e ； T.map inj₂ , proj₂ > ； couneval)) ≡⟨ refl ⟩ + councurry (interpEv (wk-ev π1 E) (interpWk π1 ； interpTm e)) ≡⟨ cong councurry (interpEv-wk-coh π1 E (interpTm e)) ⟩ + councurry (interpWk π1 ； interpEv E (interpTm e)) ≡⟨ refl ⟩ + interpEv E (interpTm e) ； T.map inj₂ ≡⟨ refl ⟩ + interpTm (E [[ e ]]) ； T.map inj₂ ≡⟨ refl ⟩ + interpTm (inr (E [[ e ]])) ∎ + where open ≡-Reasoning + π1 = wk-wk wk-id + +interpEq (colam-inl-jump e E) = + interpTm (colam (wk-ev π1 E [[ coapp (inl (wk e)) (var h) ]])) ≡⟨ refl ⟩ + councurry (interpTm (wk-ev π1 E [[ coapp (inl (wk e)) (var h) ]])) ≡⟨ cong councurry (interpWk-ev-coh' π1 E (coapp (inl (wk e)) (var h))) ⟩ + councurry (interpEv (wk-ev π1 E) (< interpWk π1 ； interpTm e ； T.map inj₁ , proj₂ ； T.eta > ； T.tau ； T.map couneval ； T.mu)) ≡⟨ refl ⟩ + councurry (interpEv (wk-ev π1 E) (< interpWk π1 ； interpTm e ； T.map inj₁ , proj₂ > ； couneval)) ≡⟨ cong councurry (interpEv-wk-coh' {e = e} E) ⟩ + councurry (< interpWk π1 ； interpTm e ； T.map inj₁ , proj₂ > ； couneval) ≡⟨ councurry-cocurry (interpTm e ； T.map inj₁) ⟩ + interpTm e ； T.map inj₁ ≡⟨ refl ⟩ + interpTm (inl e) ∎ + where open ≡-Reasoning + π1 = wk-wk wk-id + +interpEq (case-colam-beta v {{ϕ}} e1 e2) = + interpTm (case (colam v) e1 e2) ≡⟨ refl ⟩ + < id , councurry (interpTm v) > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu ≡⟨ cong (\f -> < id , councurry f > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) (interpVal-tm-coh v) ⟩ + < id , councurry (interpVal v ； T.eta) > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu ≡⟨ refl ⟩ + < id , councurry (interpSub θ1 ϕ1 ； interpTm e2) > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm (var h) ] ； T.mu ≡⟨ cong (\f -> < id , councurry f > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm (var h) ] ； T.mu) (sym (interpSub-tm-coh θ1 ϕ1 e2)) ⟩ + < id , councurry (interpTm (sub-tm θ1 e2)) > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm (var h) ] ； T.mu ≡⟨ refl ⟩ + interpTm (case (colam (sub-tm θ1 e2)) e1 (var h)) ∎ + where open ≡-Reasoning + θ1 = sub-ex (sub-wk (wk-wk wk-id) sub-id) v + ϕ1 = sub-ex (sub-wk-sub (wk-wk wk-id) sub-id sub-id-sub) ϕ + +interpEq (case-zeta e e1 e2 E) = + interpTm (E [[ case e e1 e2 ]]) ≡⟨ refl ⟩ + interpEv E (< id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm e1 , interpTm e2 ] ； T.mu) ≡⟨ interpEv-wk-coh'' e e1 e2 E ⟩ + < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpEv (wk-ev π1 E) (interpTm e1) , interpEv (wk-ev π2 E) (interpTm e2) ] ； T.mu ≡⟨ refl ⟩ + < id , interpTm e > ； T.tau ； T.map distl ； T.map S.[ interpTm (wk-ev π1 E [[ e1 ]]) , interpTm (wk-ev π2 E [[ e2 ]]) ] ； T.mu ≡⟨ refl ⟩ + interpTm (case e (wk-ev π1 E [[ e1 ]]) (wk-ev π2 E [[ e2 ]])) ∎ + where open ≡-Reasoning + π1 = wk-wk wk-id + π2 = wk-wk wk-id \ No newline at end of file diff --git a/Coexp.LamLamBar.Syntax.html b/Coexp.LamLamBar.Syntax.html index f16332c..179f740 100644 --- a/Coexp.LamLamBar.Syntax.html +++ b/Coexp.LamLamBar.Syntax.html @@ -92,219 +92,219 @@ absurd = coapp (inl unit) wk-tm : Wk Γ Δ -> Δ ⊢ A -> Γ ⊢ A -wk-tm π (nat n) = nat n -wk-tm π (zero? e) = zero? (wk-tm π e) -wk-tm π (var x) = var (wk-mem π x) -wk-tm π (lam e) = lam (wk-tm (wk-cong π) e) -wk-tm π (app e1 e2) = app (wk-tm π e1) (wk-tm π e2) -wk-tm π (pair e1 e2) = pair (wk-tm π e1) (wk-tm π e2) -wk-tm π (fst e) = fst (wk-tm π e) -wk-tm π (snd e) = snd (wk-tm π e) -wk-tm π unit = unit -wk-tm π (inl e) = inl (wk-tm π e) -wk-tm π (inr e) = inr (wk-tm π e) -wk-tm π (case e1 e2 e3) = case (wk-tm π e1) (wk-tm (wk-cong π) e2) (wk-tm (wk-cong π) e3) -wk-tm π (colam e) = colam (wk-tm (wk-cong π) e) -wk-tm π (coapp e1 e2) = coapp (wk-tm π e1) (wk-tm π e2) - -open WkTm Tm wk-tm public - -sub-tm : Sub Γ Δ -> Δ ⊢ A -> Γ ⊢ A -sub-tm θ (nat n) = nat n -sub-tm θ (zero? e) = zero? (sub-tm θ e) -sub-tm θ (var x) = - sub-mem θ x -sub-tm θ (lam e) = - lam (sub-tm (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e) -sub-tm θ (app e1 e2) = app (sub-tm θ e1) (sub-tm θ e2) -sub-tm θ (pair e1 e2) = pair (sub-tm θ e1) (sub-tm θ e2) -sub-tm θ (fst e) = fst (sub-tm θ e) -sub-tm θ (snd e) = snd (sub-tm θ e) -sub-tm θ unit = unit -sub-tm θ (inl e) = inl (sub-tm θ e) -sub-tm θ (inr e) = inr (sub-tm θ e) -sub-tm θ (case e1 e2 e3) = - case (sub-tm θ e1) - (sub-tm (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e2) - (sub-tm (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e3) -sub-tm θ (colam e) = - colam (sub-tm (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e) -sub-tm θ (coapp e1 e2) = coapp (sub-tm θ e1) (sub-tm θ e2) - -variable - n : ℕ - x : A ∈ Γ - v v1 v2 : Γ ⊢ A - e e1 e2 e3 e4 : Γ ⊢ A - -data isVal {Γ} : Γ ⊢ A -> Set where - nat : isVal (nat n) - zero? : {{isVal v}} -> isVal (zero? v) - var : isVal (var x) - lam : isVal (lam e) - fst : {{isVal v}} -> isVal (fst v) - snd : {{isVal v}} -> isVal (snd v) - pair : {{isVal v1}} -> {{isVal v2}} -> isVal (pair v1 v2) - unit : isVal unit - inl : ∀ {B} -> {{isVal v}} -> isVal (inl {B = B} v) - inr : ∀ {A} -> {{isVal v}} -> isVal (inr {A = A} v) - -open Val isVal - -wk-tm-val : (π : Wk Γ Δ) -> (v : Δ ⊢ A) (ϕ : isVal v) -> isVal (wk-tm π v) -wk-tm-val π (nat n) nat = nat -wk-tm-val π (zero? v) (zero? {{ϕ}}) = zero? {{wk-tm-val π v ϕ}} -wk-tm-val π (var i) var = var -wk-tm-val π (lam v) lam = lam -wk-tm-val π (fst v) (fst {{ϕ}}) = fst {{wk-tm-val π v ϕ}} -wk-tm-val π (snd v) (snd {{ϕ}}) = snd {{wk-tm-val π v ϕ}} -wk-tm-val π (pair v1 v2) (pair {{ϕ1}} {{ϕ2}}) = pair {{wk-tm-val π v1 ϕ1}} {{wk-tm-val π v2 ϕ2}} -wk-tm-val π unit unit = unit -wk-tm-val π (inl v) (inl {{ϕ}}) = inl {{wk-tm-val π v ϕ}} -wk-tm-val π (inr v) (inr {{ϕ}}) = inr {{wk-tm-val π v ϕ}} - -open SubTm wk-tm-val var var public - -sub-tm-val : (θ : Sub Γ Δ) (ϕ : isSub θ) -> (v : Δ ⊢ A) (ψ : isVal v) -> isVal (sub-tm θ v) -sub-tm-val θ ϕ (nat n) nat = nat -sub-tm-val θ ϕ (zero? v) (zero? {{ψ}}) = zero? {{sub-tm-val θ ϕ v ψ}} -sub-tm-val θ ϕ (var i) var = sub-mem-val θ ϕ i -sub-tm-val θ ϕ (lam v) lam = lam -sub-tm-val θ ϕ (fst v) (fst {{ψ}}) = fst {{sub-tm-val θ ϕ v ψ}} -sub-tm-val θ ϕ (snd v) (snd {{ψ}}) = snd {{sub-tm-val θ ϕ v ψ}} -sub-tm-val θ ϕ (pair v1 v2) (pair {{ψ1}} {{ψ2}}) = pair {{sub-tm-val θ ϕ v1 ψ1}} {{sub-tm-val θ ϕ v2 ψ2}} -sub-tm-val θ ϕ unit unit = unit -sub-tm-val θ ϕ (inl v) (inl {{ψ}}) = inl {{sub-tm-val θ ϕ v ψ}} -sub-tm-val θ ϕ (inr v) (inr {{ψ}}) = inr {{sub-tm-val θ ϕ v ψ}} - -syntax Ev Γ C A = Γ ⊢ C ⇛ A - -data Ev (Γ : Ctx) (C : Ty) : Ty -> Set where - - ø : - ---------------- - Γ ⊢ C ⇛ C - - app-r : (e : Γ ⊢ A `⇒ B) -> (E : Γ ⊢ C ⇛ A) - ------------------------------------------------------------ - -> Γ ⊢ C ⇛ B - - app-l : (E : Γ ⊢ C ⇛ (A `⇒ B)) -> (v : Γ ⊢ A) {{ϕ : isVal v}} - ------------------------------------------------------------ - -> Γ ⊢ C ⇛ B - -infix 5 _[[_]] -_[[_]] : (E : Γ ⊢ A ⇛ B) -> (e : Γ ⊢ A) -> Γ ⊢ B -ø [[ e ]] = e -app-r e1 E [[ e ]] = app e1 (E [[ e ]]) -app-l E v [[ e ]] = app (E [[ e ]]) v - -wk-ev : Wk Γ Δ -> Δ ⊢ A ⇛ B -> Γ ⊢ A ⇛ B -wk-ev π ø = ø -wk-ev π (app-r e E) = app-r (wk-tm π e) (wk-ev π E) -wk-ev π (app-l E v {{ϕ}}) = app-l (wk-ev π E) (wk-tm π v) {{wk-tm-val π v ϕ}} - -syntax Eq Γ A e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A - -data Eq (Γ : Ctx) : (A : Ty) -> Γ ⊢ A -> Γ ⊢ A -> Set where - - -- equivalence rules - ≈-refl : - ------------- - Γ ⊢ e ≈ e ∶ A - - ≈-sym : Γ ⊢ e1 ≈ e2 ∶ A - ------------------ - -> Γ ⊢ e2 ≈ e1 ∶ A - - ≈-trans : Γ ⊢ e1 ≈ e2 ∶ A -> Γ ⊢ e2 ≈ e3 ∶ A - ------------------------------------- - -> Γ ⊢ e1 ≈ e3 ∶ A - - -- congruence rules - fst-cong : Γ ⊢ e1 ≈ e2 ∶ A `× B - --------------------------- - -> Γ ⊢ fst e1 ≈ fst e2 ∶ A - - snd-cong : Γ ⊢ e1 ≈ e2 ∶ A `× B - --------------------------- - -> Γ ⊢ snd e1 ≈ snd e2 ∶ B - - pair-cong : Γ ⊢ e1 ≈ e2 ∶ A -> Γ ⊢ e3 ≈ e4 ∶ B - ---------------------------------------- - -> Γ ⊢ pair e1 e3 ≈ pair e2 e4 ∶ A `× B - - -- and many more - - -- generators - -- pair beta - fst-beta : (v1 : Γ ⊢ A) {{ϕ1 : isVal v1}} -> (v2 : Γ ⊢ B) {{ϕ2 : isVal v2}} - --------------------------------------------------------------- - -> Γ ⊢ fst (pair v1 v2) ≈ v1 ∶ A - - snd-beta : (v1 : Γ ⊢ A) {{ϕ1 : isVal v1}} -> (v2 : Γ ⊢ B) {{ϕ2 : isVal v2}} - --------------------------------------------------------------- - -> Γ ⊢ snd (pair v1 v2) ≈ v2 ∶ B - - -- pair eta - pair-eta : (v : Γ ⊢ A `× B) {{ϕ : isVal v}} - ----------------------------------------- - -> Γ ⊢ pair (fst v) (snd v) ≈ v ∶ A `× B - - -- unit eta - unit-eta : (v : Γ ⊢ `Unit) {{ϕ : isVal v}} - -------------------------------- - -> Γ ⊢ v ≈ unit ∶ `Unit - - -- function beta: (λx.e)v ≈ [v/x]e - lam-beta : (e : (Γ ∙ A) ⊢ B) -> (v : Γ ⊢ A) {{ϕ : isVal v}} - ------------------------------------------------------ - -> Γ ⊢ app (lam e) v ≈ sub-tm (sub-ex sub-id v) e ∶ B - - -- function eta: λx.vx ≈ v - lam-eta : (v : Γ ⊢ A `⇒ B) {{ϕ : isVal v}} - ---------------------------------------------- - -> Γ ⊢ lam (app (wk v) (var h)) ≈ v ∶ A `⇒ B - - -- sum beta - case-inl-beta : (v : Γ ⊢ A) {{ϕ : isVal v}} (e2 : (Γ ∙ A) ⊢ C) (e3 : (Γ ∙ B) ⊢ C) - ------------------------------------------------------------------- - -> Γ ⊢ case (inl v) e2 e3 ≈ sub-tm (sub-ex sub-id v) e2 ∶ C - - case-inr-beta : (v : Γ ⊢ B) {{ϕ : isVal v}} (e2 : (Γ ∙ A) ⊢ C) (e3 : (Γ ∙ B) ⊢ C) - ------------------------------------------------------------------- - -> Γ ⊢ case (inr v) e2 e3 ≈ sub-tm (sub-ex sub-id v) e3 ∶ C - - -- sum eta +wk-tm π (nat n) = nat n +wk-tm π (zero? e) = zero? (wk-tm π e) +wk-tm π (var x) = var (wk-mem π x) +wk-tm π (lam e) = lam (wk-tm (wk-cong π) e) +wk-tm π (app e1 e2) = app (wk-tm π e1) (wk-tm π e2) +wk-tm π (pair e1 e2) = pair (wk-tm π e1) (wk-tm π e2) +wk-tm π (fst e) = fst (wk-tm π e) +wk-tm π (snd e) = snd (wk-tm π e) +wk-tm π unit = unit +wk-tm π (inl e) = inl (wk-tm π e) +wk-tm π (inr e) = inr (wk-tm π e) +wk-tm π (case e1 e2 e3) = case (wk-tm π e1) (wk-tm (wk-cong π) e2) (wk-tm (wk-cong π) e3) +wk-tm π (colam e) = colam (wk-tm (wk-cong π) e) +wk-tm π (coapp e1 e2) = coapp (wk-tm π e1) (wk-tm π e2) + +open WkTm Tm wk-tm public + +sub-tm : Sub Γ Δ -> Δ ⊢ A -> Γ ⊢ A +sub-tm θ (nat n) = nat n +sub-tm θ (zero? e) = zero? (sub-tm θ e) +sub-tm θ (var x) = + sub-mem θ x +sub-tm θ (lam e) = + lam (sub-tm (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e) +sub-tm θ (app e1 e2) = app (sub-tm θ e1) (sub-tm θ e2) +sub-tm θ (pair e1 e2) = pair (sub-tm θ e1) (sub-tm θ e2) +sub-tm θ (fst e) = fst (sub-tm θ e) +sub-tm θ (snd e) = snd (sub-tm θ e) +sub-tm θ unit = unit +sub-tm θ (inl e) = inl (sub-tm θ e) +sub-tm θ (inr e) = inr (sub-tm θ e) +sub-tm θ (case e1 e2 e3) = + case (sub-tm θ e1) + (sub-tm (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e2) + (sub-tm (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e3) +sub-tm θ (colam e) = + colam (sub-tm (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e) +sub-tm θ (coapp e1 e2) = coapp (sub-tm θ e1) (sub-tm θ e2) + +variable + n : ℕ + x : A ∈ Γ + v v1 v2 : Γ ⊢ A + e e1 e2 e3 e4 : Γ ⊢ A + +data isVal {Γ} : Γ ⊢ A -> Set where + instance nat : isVal (nat n) + instance zero? : {{isVal v}} -> isVal (zero? v) + instance var : isVal (var x) + instance lam : isVal (lam e) + instance fst : {{isVal v}} -> isVal (fst v) + instance snd : {{isVal v}} -> isVal (snd v) + instance pair : {{isVal v1}} -> {{isVal v2}} -> isVal (pair v1 v2) + instance unit : isVal unit + instance inl : ∀ {B} -> {{isVal v}} -> isVal (inl {B = B} v) + instance inr : ∀ {A} -> {{isVal v}} -> isVal (inr {A = A} v) + +open Val isVal + +wk-tm-val : (π : Wk Γ Δ) -> (v : Δ ⊢ A) {{ϕ : isVal v}} -> isVal (wk-tm π v) +wk-tm-val π (nat n) {{nat}} = nat +wk-tm-val π (zero? v) {{zero?}} = zero? {{wk-tm-val π v}} +wk-tm-val π (var i) {{var}} = var +wk-tm-val π (lam v) {{lam}} = lam +wk-tm-val π (fst v) {{fst}} = fst {{wk-tm-val π v}} +wk-tm-val π (snd v) {{snd}} = snd {{wk-tm-val π v}} +wk-tm-val π (pair v1 v2) {{pair}} = pair {{wk-tm-val π v1}} {{wk-tm-val π v2}} +wk-tm-val π unit {{unit}} = unit +wk-tm-val π (inl v) {{inl}} = inl {{wk-tm-val π v}} +wk-tm-val π (inr v) {{inr}} = inr {{wk-tm-val π v}} + +open SubTm wk-tm-val var var public + +sub-tm-val : (θ : Sub Γ Δ) (ϕ : isSub θ) -> (v : Δ ⊢ A) {{ψ : isVal v}} -> isVal (sub-tm θ v) +sub-tm-val θ ϕ (nat n) {{nat}} = nat +sub-tm-val θ ϕ (zero? v) {{zero?}} = zero? {{sub-tm-val θ ϕ v}} +sub-tm-val θ ϕ (var i) {{var}} = sub-mem-val θ ϕ i +sub-tm-val θ ϕ (lam v) {{lam}} = lam +sub-tm-val θ ϕ (fst v) {{fst}} = fst {{sub-tm-val θ ϕ v}} +sub-tm-val θ ϕ (snd v) {{snd}} = snd {{sub-tm-val θ ϕ v}} +sub-tm-val θ ϕ (pair v1 v2) {{pair}} = pair {{sub-tm-val θ ϕ v1}} {{sub-tm-val θ ϕ v2}} +sub-tm-val θ ϕ unit {{unit}} = unit +sub-tm-val θ ϕ (inl v) {{inl}} = inl {{sub-tm-val θ ϕ v}} +sub-tm-val θ ϕ (inr v) {{inr}} = inr {{sub-tm-val θ ϕ v}} + +syntax Ev Γ C A = Γ ⊢ C ⇛ A + +data Ev (Γ : Ctx) (C : Ty) : Ty -> Set where + + ø : + ---------------- + Γ ⊢ C ⇛ C + + app-r : (e : Γ ⊢ A `⇒ B) -> (E : Γ ⊢ C ⇛ A) + ------------------------------------------------------------ + -> Γ ⊢ C ⇛ B + + app-l : (E : Γ ⊢ C ⇛ (A `⇒ B)) -> (v : Γ ⊢ A) {{ϕ : isVal v}} + ------------------------------------------------------------ + -> Γ ⊢ C ⇛ B + +infix 5 _[[_]] +_[[_]] : (E : Γ ⊢ A ⇛ B) -> (e : Γ ⊢ A) -> Γ ⊢ B +ø [[ e ]] = e +app-r e1 E [[ e ]] = app e1 (E [[ e ]]) +app-l E v [[ e ]] = app (E [[ e ]]) v + +wk-ev : Wk Γ Δ -> Δ ⊢ A ⇛ B -> Γ ⊢ A ⇛ B +wk-ev π ø = ø +wk-ev π (app-r e E) = app-r (wk-tm π e) (wk-ev π E) +wk-ev π (app-l E v) = app-l (wk-ev π E) (wk-tm π v) {{wk-tm-val π v}} + +syntax Eq Γ A e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A + +data Eq (Γ : Ctx) : (A : Ty) -> Γ ⊢ A -> Γ ⊢ A -> Set where + + -- equivalence rules + ≈-refl : + ------------- + Γ ⊢ e ≈ e ∶ A + + ≈-sym : Γ ⊢ e1 ≈ e2 ∶ A + ------------------ + -> Γ ⊢ e2 ≈ e1 ∶ A + + ≈-trans : Γ ⊢ e1 ≈ e2 ∶ A -> Γ ⊢ e2 ≈ e3 ∶ A + ------------------------------------- + -> Γ ⊢ e1 ≈ e3 ∶ A + + -- congruence rules + fst-cong : Γ ⊢ e1 ≈ e2 ∶ A `× B + --------------------------- + -> Γ ⊢ fst e1 ≈ fst e2 ∶ A + + snd-cong : Γ ⊢ e1 ≈ e2 ∶ A `× B + --------------------------- + -> Γ ⊢ snd e1 ≈ snd e2 ∶ B + + pair-cong : Γ ⊢ e1 ≈ e2 ∶ A -> Γ ⊢ e3 ≈ e4 ∶ B + ---------------------------------------- + -> Γ ⊢ pair e1 e3 ≈ pair e2 e4 ∶ A `× B + + -- and many more + + -- generators + -- pair beta + fst-beta : (v1 : Γ ⊢ A) {{ϕ1 : isVal v1}} -> (v2 : Γ ⊢ B) {{ϕ2 : isVal v2}} + --------------------------------------------------------------- + -> Γ ⊢ fst (pair v1 v2) ≈ v1 ∶ A + + snd-beta : (v1 : Γ ⊢ A) {{ϕ1 : isVal v1}} -> (v2 : Γ ⊢ B) {{ϕ2 : isVal v2}} + --------------------------------------------------------------- + -> Γ ⊢ snd (pair v1 v2) ≈ v2 ∶ B + + -- pair eta + pair-eta : (v : Γ ⊢ A `× B) {{ϕ : isVal v}} + ----------------------------------------- + -> Γ ⊢ pair (fst v) (snd v) ≈ v ∶ A `× B + + -- unit eta + unit-eta : (v : Γ ⊢ `Unit) {{ϕ : isVal v}} + ----------------------------------------- + -> Γ ⊢ v ≈ unit ∶ `Unit + + -- function beta: (λx.e)v ≈ [v/x]e + lam-beta : (e : (Γ ∙ A) ⊢ B) -> (v : Γ ⊢ A) {{ϕ : isVal v}} + ------------------------------------------------------ + -> Γ ⊢ app (lam e) v ≈ sub-tm (sub-ex sub-id v) e ∶ B + + -- function eta: λx.vx ≈ v + lam-eta : (v : Γ ⊢ A `⇒ B) {{ϕ : isVal v}} + ---------------------------------------------- + -> Γ ⊢ lam (app (wk v) (var h)) ≈ v ∶ A `⇒ B + + -- sum beta + case-inl-beta : (v : Γ ⊢ A) {{ϕ : isVal v}} (e2 : (Γ ∙ A) ⊢ C) (e3 : (Γ ∙ B) ⊢ C) + -------------------------------------------------------------------- + -> Γ ⊢ case (inl v) e2 e3 ≈ sub-tm (sub-ex sub-id v) e2 ∶ C + + case-inr-beta : (v : Γ ⊢ B) {{ϕ : isVal v}} (e2 : (Γ ∙ A) ⊢ C) (e3 : (Γ ∙ B) ⊢ C) + -------------------------------------------------------------------- + -> Γ ⊢ case (inr v) e2 e3 ≈ sub-tm (sub-ex sub-id v) e3 ∶ C + + -- sum eta - -- coexponential beta: (~λx.e)v ≈ [v/x]e - colam-beta : (e : (Γ ∙ A *) ⊢ B) -> (v : Γ ⊢ A *) {{ϕ : isVal v}} - ---------------------------------------------------------- - -> Γ ⊢ coapp (colam e) v ≈ sub-tm (sub-ex sub-id v) e ∶ B - - -- coexponential eta: (~λx.~ex) ≈ e - colam-eta : (e : Γ ⊢ A `+ B) - ------------------------------------------------- - -> Γ ⊢ colam (coapp (wk e) (var h)) ≈ e ∶ A `+ B - - -- control effects - colam-const : (e : Γ ⊢ B) - ------------------------------------- - -> Γ ⊢ colam (wk e) ≈ inr e ∶ A `+ B - - colam-inr-pass : (e : Γ ⊢ B) (E : Γ ⊢ B ⇛ C) - ---------------------------------------------------------------------------------------------------- - -> Γ ⊢ colam (wk-ev (wk-wk wk-id) E [[ coapp (inr (wk e)) (var h) ]]) ≈ inr (E [[ e ]]) ∶ A `+ C - - colam-inl-jump : (e : Γ ⊢ A) (E : Γ ⊢ B ⇛ C) - ---------------------------------------------------------------------------------------------------- - -> Γ ⊢ colam (wk-ev (wk-wk wk-id) E [[ coapp (inl (wk e)) (var h) ]]) ≈ inl e ∶ A `+ C - - case-colam-beta : (v : (Γ ∙ A *) ⊢ B) {{ϕ : isVal v}} -> (e1 : (Γ ∙ A) ⊢ C) (e2 : (Γ ∙ B) ⊢ C) - --------------------------------------------------------------------------------------------------------------- - -> Γ ⊢ case (colam v) e1 e2 ≈ case (colam (sub-tm (sub-ex (sub-wk (wk-wk wk-id) sub-id) v) e2)) e1 (var h) ∶ C - - case-zeta : (e : Γ ⊢ A `+ B) (e1 : (Γ ∙ A) ⊢ C) (e2 : (Γ ∙ B) ⊢ C) (E : Γ ⊢ C ⇛ D) - ------------------------------------------------------------------------------------------------------------ - -> Γ ⊢ E [[ case e e1 e2 ]] ≈ case e (wk-ev (wk-wk wk-id) E [[ e1 ]]) (wk-ev (wk-wk wk-id) E [[ e2 ]]) ∶ D + -- coexponential beta: (~λx.e)v ≈ [v/x]e + colam-beta : (e : (Γ ∙ A *) ⊢ B) -> (v : Γ ⊢ A *) {{ϕ : isVal v}} + ---------------------------------------------------------- + -> Γ ⊢ coapp (colam e) v ≈ sub-tm (sub-ex sub-id v) e ∶ B + + -- coexponential eta: (~λx.~ex) ≈ e + colam-eta : (e : Γ ⊢ A `+ B) + ------------------------------------------------- + -> Γ ⊢ colam (coapp (wk e) (var h)) ≈ e ∶ A `+ B + + -- control effects + colam-const : (e : Γ ⊢ B) + ------------------------------------- + -> Γ ⊢ colam (wk e) ≈ inr e ∶ A `+ B + + colam-inr-pass : (e : Γ ⊢ B) (E : Γ ⊢ B ⇛ C) + ---------------------------------------------------------------------------------------------------- + -> Γ ⊢ colam (wk-ev (wk-wk wk-id) E [[ coapp (inr (wk e)) (var h) ]]) ≈ inr (E [[ e ]]) ∶ A `+ C + + colam-inl-jump : (e : Γ ⊢ A) (E : Γ ⊢ B ⇛ C) + ---------------------------------------------------------------------------------------------------- + -> Γ ⊢ colam (wk-ev (wk-wk wk-id) E [[ coapp (inl (wk e)) (var h) ]]) ≈ inl e ∶ A `+ C + + case-colam-beta : (v : (Γ ∙ A *) ⊢ B) {{ϕ : isVal v}} -> (e1 : (Γ ∙ A) ⊢ C) (e2 : (Γ ∙ B) ⊢ C) + --------------------------------------------------------------------------------------------------------------- + -> Γ ⊢ case (colam v) e1 e2 ≈ case (colam (sub-tm (sub-ex (sub-wk (wk-wk wk-id) sub-id) v) e2)) e1 (var h) ∶ C + + case-zeta : (e : Γ ⊢ A `+ B) (e1 : (Γ ∙ A) ⊢ C) (e2 : (Γ ∙ B) ⊢ C) (E : Γ ⊢ C ⇛ D) + ------------------------------------------------------------------------------------------------------------ + -> Γ ⊢ E [[ case e e1 e2 ]] ≈ case e (wk-ev (wk-wk wk-id) E [[ e1 ]]) (wk-ev (wk-wk wk-id) E [[ e2 ]]) ∶ D \ No newline at end of file diff --git a/Coexp.Meta.Prelude.html b/Coexp.Meta.Prelude.html index a85c6bb..bf1697f 100644 --- a/Coexp.Meta.Prelude.html +++ b/Coexp.Meta.Prelude.html @@ -70,51 +70,51 @@ sub-ε : isSub (sub-ε) sub-ex : (ϕ : isSub θ) -> (ψ : isVal v) -> isSub (sub-ex θ v) - module SubTm (wk-tm-val : ∀ {A Γ Δ} -> (π : Wk Γ Δ) -> (v : Tm Δ A) (ϕ : isVal v) -> isVal (wk-tm π v)) - (var : ∀ {A Γ} -> A ∈ Γ -> Tm Γ A) - (varIsVal : ∀ {Γ A} {x : A ∈ Γ} -> isVal (var x)) where + module SubTm (wk-tm-val : ∀ {A Γ Δ} -> (π : Wk Γ Δ) -> (v : Tm Δ A) {{ϕ : isVal v}} -> isVal (wk-tm π v)) + (var : ∀ {A Γ} -> A ∈ Γ -> Tm Γ A) + (varIsVal : ∀ {Γ A} {x : A ∈ Γ} -> isVal (var x)) where - sub-id : Sub Γ Γ - sub-id {Γ = ε} = sub-ε - sub-id {Γ = Γ ∙ A} = sub-ex (sub-wk (wk-wk wk-id) sub-id) (var h) + sub-id : Sub Γ Γ + sub-id {Γ = ε} = sub-ε + sub-id {Γ = Γ ∙ A} = sub-ex (sub-wk (wk-wk wk-id) sub-id) (var h) - sub-wk-sub : (π : Wk Γ Δ) -> (θ : Sub Δ Ψ) (ϕ : isSub θ) -> isSub (sub-wk π θ) - sub-wk-sub π sub-ε sub-ε = sub-ε - sub-wk-sub π (sub-ex θ e) (sub-ex ϕ ψ) = sub-ex (sub-wk-sub π θ ϕ) (wk-tm-val π e ψ) + sub-wk-sub : (π : Wk Γ Δ) -> (θ : Sub Δ Ψ) (ϕ : isSub θ) -> isSub (sub-wk π θ) + sub-wk-sub π sub-ε sub-ε = sub-ε + sub-wk-sub π (sub-ex θ e) (sub-ex ϕ ψ) = sub-ex (sub-wk-sub π θ ϕ) (wk-tm-val π e {{ψ}}) - sub-id-sub : {Γ : Ctx} -> isSub (sub-id {Γ}) - sub-id-sub {ε} = sub-ε - sub-id-sub {Γ ∙ A} = sub-ex (sub-wk-sub (wk-wk wk-id) (sub-id {Γ}) sub-id-sub) varIsVal + sub-id-sub : {Γ : Ctx} -> isSub (sub-id {Γ}) + sub-id-sub {ε} = sub-ε + sub-id-sub {Γ ∙ A} = sub-ex (sub-wk-sub (wk-wk wk-id) (sub-id {Γ}) sub-id-sub) varIsVal - sub-mem-val : (θ : Sub Γ Δ) (ϕ : isSub θ) (i : A ∈ Δ) -> isVal (sub-mem θ i) - sub-mem-val (sub-ex θ e) (sub-ex ϕ ψ) h = ψ - sub-mem-val (sub-ex θ e) (sub-ex ϕ ψ) (t i) = sub-mem-val θ ϕ i + sub-mem-val : (θ : Sub Γ Δ) (ϕ : isSub θ) (i : A ∈ Δ) -> isVal (sub-mem θ i) + sub-mem-val (sub-ex θ e) (sub-ex ϕ ψ) h = ψ + sub-mem-val (sub-ex θ e) (sub-ex ϕ ψ) (t i) = sub-mem-val θ ϕ i - module WkArr (Arr : Ctx -> Ty -> Ty -> Set) (wk-arr : ∀ {A B Γ Δ} -> Wk Γ Δ -> Arr Δ A B -> Arr Γ A B) where + module WkArr (Arr : Ctx -> Ty -> Ty -> Set) (wk-arr : ∀ {A B Γ Δ} -> Wk Γ Δ -> Arr Δ A B -> Arr Γ A B) where - wk : Arr Γ A B -> Arr (Γ ∙ C) A B - wk = wk-arr (wk-wk wk-id) + wk : Arr Γ A B -> Arr (Γ ∙ C) A B + wk = wk-arr (wk-wk wk-id) - module Sub (`1 : Ty) (var : ∀ {A Γ} -> A ∈ Γ -> Arr Γ `1 A) where + module Sub (`1 : Ty) (var : ∀ {A Γ} -> A ∈ Γ -> Arr Γ `1 A) where - data Sub (Γ : Ctx) : (Δ : Ctx) -> Set where - sub-ε : Sub Γ ε - sub-ex : (θ : Sub Γ Δ) -> (e : Arr Γ `1 A) -> Sub Γ (Δ ∙ A) + data Sub (Γ : Ctx) : (Δ : Ctx) -> Set where + sub-ε : Sub Γ ε + sub-ex : (θ : Sub Γ Δ) -> (e : Arr Γ `1 A) -> Sub Γ (Δ ∙ A) - sub-mem : Sub Γ Δ -> A ∈ Δ -> Arr Γ `1 A - sub-mem (sub-ex θ e) h = e - sub-mem (sub-ex θ e) (t i) = sub-mem θ i + sub-mem : Sub Γ Δ -> A ∈ Δ -> Arr Γ `1 A + sub-mem (sub-ex θ e) h = e + sub-mem (sub-ex θ e) (t i) = sub-mem θ i - sub-wk : Wk Γ Δ -> Sub Δ Ψ -> Sub Γ Ψ - sub-wk π sub-ε = sub-ε - sub-wk π (sub-ex θ e) = sub-ex (sub-wk π θ) (wk-arr π e) + sub-wk : Wk Γ Δ -> Sub Δ Ψ -> Sub Γ Ψ + sub-wk π sub-ε = sub-ε + sub-wk π (sub-ex θ e) = sub-ex (sub-wk π θ) (wk-arr π e) - sub-id : Sub Γ Γ - sub-id {Γ = ε} = sub-ε - sub-id {Γ = Γ ∙ A} = sub-ex (sub-wk (wk-wk wk-id) sub-id) (var h) + sub-id : Sub Γ Γ + sub-id {Γ = ε} = sub-ε + sub-id {Γ = Γ ∙ A} = sub-ex (sub-wk (wk-wk wk-id) sub-id) (var h) - module SubArr (sub-arr : ∀ {A B Γ Δ} -> Sub Γ Δ -> Arr Δ A B -> Arr Γ A B) where + module SubArr (sub-arr : ∀ {A B Γ Δ} -> Sub Γ Δ -> Arr Δ A B -> Arr Γ A B) where - sub : Arr Γ `1 A -> Arr (Γ ∙ A) B C -> Arr Γ B C - sub x f = sub-arr (sub-ex sub-id x) f + sub : Arr Γ `1 A -> Arr (Γ ∙ A) B C -> Arr Γ B C + sub x f = sub-arr (sub-ex sub-id x) f \ No newline at end of file diff --git a/Coexp.Zeta.Syntax.html b/Coexp.Zeta.Syntax.html index 14ca1ad..49ebb6d 100644 --- a/Coexp.Zeta.Syntax.html +++ b/Coexp.Zeta.Syntax.html @@ -50,18 +50,18 @@ wk-arr π (pass e) = pass (wk-arr π e) wk-arr π (ζ e) = ζ (wk-arr (wk-cong π) e) -open WkArr Arr wk-arr -open Sub `1 var +open WkArr Arr wk-arr +open Sub `1 var -sub-arr : Sub Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B -sub-arr θ (var i) = sub-mem θ i +sub-arr : Sub Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B +sub-arr θ (var i) = sub-mem θ i sub-arr θ id = id sub-arr θ bang = bang sub-arr θ (e1 ∘ e2) = sub-arr θ e1 ∘ sub-arr θ e2 sub-arr θ (pass e) = pass (sub-arr θ e) -sub-arr θ (ζ e) = ζ (sub-arr (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e) +sub-arr θ (ζ e) = ζ (sub-arr (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e) -open SubArr sub-arr +open SubArr sub-arr syntax Eq Γ A B e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A ->> B @@ -85,9 +85,9 @@ ζ-beta : (f : (Γ ∙ C) ⊢ A ->> B) (c : Γ ⊢ `1 ->> C) ------------------------------------------------ - -> Γ ⊢ pass {B = B} c ∘ ζ {C = C} f ≈ sub c f ∶ A ->> B + -> Γ ⊢ pass {B = B} c ∘ ζ {C = C} f ≈ sub c f ∶ A ->> B ζ-eta : (f : Γ ⊢ A ->> (C `⇒ B)) ------------------------------------ - -> Γ ⊢ ζ {C = C} (pass {B = B} (var h) ∘ wk f) ≈ f ∶ A ->> (C `⇒ B) + -> Γ ⊢ ζ {C = C} (pass {B = B} (var h) ∘ wk f) ≈ f ∶ A ->> (C `⇒ B) \ No newline at end of file diff --git a/Coexp.ZetaStar.Syntax.html b/Coexp.ZetaStar.Syntax.html index 6406790..57d6be0 100644 --- a/Coexp.ZetaStar.Syntax.html +++ b/Coexp.ZetaStar.Syntax.html @@ -52,18 +52,18 @@ wk-arr π (pass* e) = pass* (wk-arr π e) wk-arr π (ζ* e) = ζ* (wk-arr (wk-cong π) e) -open WkArr Arr wk-arr -open Sub `1 var +open WkArr Arr wk-arr +open Sub `1 var -sub-arr : Sub Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B -sub-arr θ (var i) = sub-mem θ i +sub-arr : Sub Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B +sub-arr θ (var i) = sub-mem θ i sub-arr θ id = id sub-arr θ bang = bang sub-arr θ (e1 ∘ e2) = sub-arr θ e1 ∘ sub-arr θ e2 sub-arr θ (pass* e) = pass* (sub-arr θ e) -sub-arr θ (ζ* e) = ζ* (sub-arr (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e) +sub-arr θ (ζ* e) = ζ* (sub-arr (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e) -open SubArr sub-arr +open SubArr sub-arr syntax Eq Γ A B e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A ->> B @@ -87,9 +87,9 @@ ζ*-beta : (f : (Γ ∙ C *) ⊢ A ->> B) (c : Γ ⊢ `1 ->> C *) ------------------------------------------------ - -> Γ ⊢ pass* {B = B} c ∘ ζ* {C = C} f ≈ sub c f ∶ A ->> B + -> Γ ⊢ pass* {B = B} c ∘ ζ* {C = C} f ≈ sub c f ∶ A ->> B ζ*-eta : (f : Γ ⊢ A ->> (C `+ B)) ------------------------------------ - -> Γ ⊢ ζ* {C = C} (pass* {B = B} (var h) ∘ wk f) ≈ f ∶ A ->> (C `+ B) + -> Γ ⊢ ζ* {C = C} (pass* {B = B} (var h) ∘ wk f) ≈ f ∶ A ->> (C `+ B) \ No newline at end of file