From c0633cbe9c0abc6f3c46955c307f47a939fc5385 Mon Sep 17 00:00:00 2001 From: vikraman Date: Sun, 13 Oct 2024 18:52:29 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20vikraman?= =?UTF-8?q?/agda-coexp@07d9c4a715e5fbeec97c16ba7459596608466065=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Coexp.LamLamBar.Interp.html | 812 +++++++++++++++++++++++------------- Coexp.LamLamBar.Syntax.html | 564 +++++++++++++------------ Coexp.Prelude.html | 87 +++- Coexp.Semantics.html | 26 +- 4 files changed, 901 insertions(+), 588 deletions(-) diff --git a/Coexp.LamLamBar.Interp.html b/Coexp.LamLamBar.Interp.html index 6679de3..2e7da7d 100644 --- a/Coexp.LamLamBar.Interp.html +++ b/Coexp.LamLamBar.Interp.html @@ -19,306 +19,516 @@ -- interpretation of types -- functions are kleisli arrows interpTy : Ty -> Set -interpTy `Nat = ℕ +interpTy `Nat = ℕ interpTy `Unit = ⊤ -interpTy `Void = ⊥ -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) = - (\_ -> 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 = - (\_ -> tt) ； T.eta -interpTm (absurd e) = - interpTm e ； T.map ⊥-elim -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 coeval'' ； T.mu -interpTm (lett e1 e2) = - let f = interpTm e1 ; g = curry (interpTm e2) - in < f , g > ； T.bind - --- interpretation of weakening -interpWk : Wk Γ Δ -> interpCtx Γ -> interpCtx Δ -interpWk wk-ε = \_ -> 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 - -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 π (absurd e) rewrite interpWk-tm-coh π e = 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 -interpWk-tm-coh π (lett e1 e2) rewrite interpWk-tm-coh π e1 | interpWk-tm-coh (wk-cong π) e2 = refl - --- interpretation of values -interpVal : (e : Γ ⊢ A) -> isVal e -> interpCtx Γ -> interpTy A -interpVal (nat n) nat = \_ -> 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 = \_ -> tt -interpVal (inl e) (inl {{ϕ}}) = interpVal e ϕ ； inj₁ -interpVal (inr e) (inr {{ϕ}}) = interpVal e ϕ ； inj₂ -interpVal (lett e1 e2) (lett {{ϕ1}} {{ϕ2}}) = < curry (interpVal e2 ϕ2) , interpVal e1 ϕ1 > ； eval - --- 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-tm-coh (lett e1 e2) (lett {{ϕ1}} {{ϕ2}}) - rewrite interpVal-tm-coh e1 ϕ1 | interpVal-tm-coh e2 ϕ2 = 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 -interpVal-wk-coh π (lett v1 v2) (lett {{ϕ1}} {{ϕ2}}) rewrite interpVal-wk-coh π v1 ϕ1 | interpVal-wk-coh (wk-cong π) v2 ϕ2 = refl - -open Val isVal - --- interpretation of substitutions -interpSub : (θ : Sub Γ Δ) (ϕ : isSub θ) -> interpCtx Γ -> interpCtx Δ -interpSub sub-ε sub-ε = \_ -> 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 - -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 - -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 θ ϕ (absurd e) rewrite interpSub-tm-coh θ ϕ e = 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 -- TODO: write proper proof - 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 -interpSub-tm-coh {Γ = Γ} θ ϕ (lett {A = A} e1 e2) rewrite -- TODO: write proper proof - 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-wk-coh (wk-wk {A = A} wk-id) θ ϕ - | interpWk-id-coh {Γ = Γ} = - 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 (absurd e) γ k = - evalTm e γ ⊥-elim -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 (lett e1 e2) γ k = - evalTm e1 γ \a -> - evalTm e2 (γ , a) k - -_ : 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 (absurd e) rewrite adequacy e = - funext (\γ -> funext \k -> cong (evalTm e γ) (funext \())) -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 })) -adequacy (lett e1 e2) rewrite adequacy e1 | adequacy e2 = refl +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 \ No newline at end of file diff --git a/Coexp.LamLamBar.Syntax.html b/Coexp.LamLamBar.Syntax.html index 0229670..f16332c 100644 --- a/Coexp.LamLamBar.Syntax.html +++ b/Coexp.LamLamBar.Syntax.html @@ -5,270 +5,306 @@ open import Coexp.Meta.Prelude open import Data.Nat -infix 50 _* -infixr 40 _`×_ -infixr 35 _`+_ -infixr 25 _`⇒_ +infix 50 _* +infixr 40 _`×_ +infixr 35 _`+_ +infixr 25 _`⇒_ data Ty : Set where - `Unit `Void `Nat : Ty - _* : Ty -> Ty - _`×_ _`⇒_ _`+_ : Ty -> Ty -> Ty - -`Bool : Ty -`Bool = `Unit `+ `Unit - -open Ctx Ty public - -syntax Tm Γ A = Γ ⊢ A - -data Tm : Ctx -> Ty -> Set where - - nat : (n : ℕ) - ----------- - -> Γ ⊢ `Nat - - zero? : Γ ⊢ `Nat - ----------- - -> Γ ⊢ `Bool - - var : (i : A ∈ Γ) - --------- - -> Γ ⊢ A - - lam : (Γ ∙ A) ⊢ B - ----------------- - -> Γ ⊢ A `⇒ B - - app : Γ ⊢ A `⇒ B -> Γ ⊢ A - ------------------------- - -> Γ ⊢ B - - pair : Γ ⊢ A -> Γ ⊢ B - ------------------- - -> Γ ⊢ A `× B - - fst : Γ ⊢ A `× B - --------------- - -> Γ ⊢ A - - snd : Γ ⊢ A `× B - --------------- - -> Γ ⊢ B - - unit : - ----------- - Γ ⊢ `Unit - - absurd : Γ ⊢ `Void - ------------ - -> Γ ⊢ A - - inl : Γ ⊢ A - --------------- - -> Γ ⊢ A `+ B - - inr : Γ ⊢ B - --------------- - -> Γ ⊢ A `+ B - - case : Γ ⊢ A `+ B -> (Γ ∙ A) ⊢ C -> (Γ ∙ B) ⊢ C - --------------------------------------------- - -> Γ ⊢ C - - colam : (Γ ∙ A *) ⊢ B - ----------------- - -> Γ ⊢ A `+ B - - coapp : Γ ⊢ A `+ B -> Γ ⊢ A * - -------------------------- - -> Γ ⊢ B - - lett : Γ ⊢ A -> (Γ ∙ A) ⊢ B - ----------------------- - -> Γ ⊢ B - -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 π (absurd e) = absurd (wk-tm π e) -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) -wk-tm π (lett e1 e2) = lett (wk-tm π e1) (wk-tm (wk-cong π) 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 θ (absurd e) = absurd (sub-tm θ e) -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) -sub-tm θ (lett e1 e2) = - lett (sub-tm θ e1) (sub-tm (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) 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) - lett : {{isVal e1}} -> {{isVal e2}} -> isVal (lett e1 e2) - -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 ϕ}} -wk-tm-val π (lett v1 v2) (lett {{ϕ1}} {{ϕ2}}) = lett {{wk-tm-val π v1 ϕ1}} {{wk-tm-val (wk-cong π) v2 ϕ2}} - -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 ψ}} -sub-tm-val θ ϕ (lett v1 v2) (lett {{ψ1}} {{ψ2}}) = - lett {{sub-tm-val θ ϕ v1 ψ1}} - {{sub-tm-val (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) (sub-ex (sub-wk-sub (wk-wk wk-id) θ ϕ) var) v2 ψ2}} - -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.~vx) ≈ v - colam-eta : (v : Γ ⊢ A `+ B) {{ϕ : isVal v}} - ------------------------------------------------- - -> Γ ⊢ colam (coapp (wk v) (var h)) ≈ v ∶ A `+ B - - -- let beta: (let x = e in x) ≈ e - lett-unit : - -------------------------- - Γ ⊢ lett e (var h) ≈ e ∶ A + `Unit `Nat : Ty + _* : Ty -> Ty + _`×_ _`⇒_ _`+_ : Ty -> Ty -> Ty + +`Bool : Ty +`Bool = `Unit `+ `Unit + +open Ctx Ty public + +syntax Tm Γ A = Γ ⊢ A + +data Tm : Ctx -> Ty -> Set where + + nat : (n : ℕ) + ----------- + -> Γ ⊢ `Nat + + zero? : Γ ⊢ `Nat + ----------- + -> Γ ⊢ `Bool + + var : (i : A ∈ Γ) + --------- + -> Γ ⊢ A + + lam : (Γ ∙ A) ⊢ B + ----------------- + -> Γ ⊢ A `⇒ B + + app : Γ ⊢ A `⇒ B -> Γ ⊢ A + ------------------------- + -> Γ ⊢ B + + pair : Γ ⊢ A -> Γ ⊢ B + ------------------- + -> Γ ⊢ A `× B + + fst : Γ ⊢ A `× B + --------------- + -> Γ ⊢ A + + snd : Γ ⊢ A `× B + --------------- + -> Γ ⊢ B + + unit : + ----------- + Γ ⊢ `Unit + + inl : Γ ⊢ A + --------------- + -> Γ ⊢ A `+ B + + inr : Γ ⊢ B + --------------- + -> Γ ⊢ A `+ B + + case : Γ ⊢ A `+ B -> (Γ ∙ A) ⊢ C -> (Γ ∙ B) ⊢ C + --------------------------------------------- + -> Γ ⊢ C + + colam : (Γ ∙ A *) ⊢ B + ----------------- + -> Γ ⊢ A `+ B + + coapp : Γ ⊢ A `+ B -> Γ ⊢ A * + -------------------------- + -> Γ ⊢ B + +-- syntactic sugar +lett : Γ ⊢ A -> (Γ ∙ A) ⊢ B + ----------------------- + -> Γ ⊢ B +lett e1 e2 = app (lam e2) e1 + +absurd : Γ ⊢ `Unit * + ---------------- + -> Γ ⊢ A +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 + + -- 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.Prelude.html b/Coexp.Prelude.html index fb3fe02..aa38a8a 100644 --- a/Coexp.Prelude.html +++ b/Coexp.Prelude.html @@ -1,27 +1,82 @@ Coexp.Prelude
module Coexp.Prelude where
 
-open import Relation.Binary.PropositionalEquality
+open import Data.Product as P renaming (map to pmap)
+open import Function
+open import Relation.Binary.PropositionalEquality
 
-postulate
-  TODO : ∀ {a} {A : Set a} -> A
+postulate
+  TODO : ∀ {a} {A : Set a} -> A
 
-postulate
-  funext : ∀ {a b} {A : Set a} {B : Set b} {f g : A -> B} -> ((x : A) -> f x ≡ g x) -> f ≡ g
+{-# BUILTIN REWRITE _≡_ #-}
 
-happly : ∀ {a b} {A : Set a} {B : Set b} {f g : A -> B} -> f ≡ g -> (x : A) -> f x ≡ g x
-happly refl _ = refl
+module _ where
+  postulate
+    I : Set
+    i0 i1 : I
+    seg : i0 ≡ i1
 
-open import Data.Nat
+  module _ {p} {P : I -> Set p} where
+    postulate
+      I-elim : (p0 : P i0) (p1 : P i1) (p : subst P seg p0 ≡ p1) -> ∀ i -> P i
+      I-elim-i0 : ∀ {p0} {p1} {p} -> I-elim p0 p1 p i0 ≡ p0
+      {-# REWRITE I-elim-i0 #-}
+      I-elim-i1 : ∀ {p0} {p1} {p} -> I-elim p0 p1 p i1 ≡ p1
+      {-# REWRITE I-elim-i1 #-}
 
-recNat : ∀ {a} {A : Set a} -> A -> (A -> A) -> ℕ -> A
-recNat a f zero = a
-recNat a f (suc n) = f (recNat a f n)
+  module _ {p} {P : Set p} where
+    postulate
+      I-rec : (p0 p1 : P) (p : p0 ≡ p1) -> I -> P
+      I-rec-i0 : ∀ {p0} {p1} {p} -> I-rec p0 p1 p i0 ≡ p0
+      {-# REWRITE I-rec-i0 #-}
+      I-rec-i1 : ∀ {p0} {p1} {p} -> I-rec p0 p1 p i1 ≡ p1
+      {-# REWRITE I-rec-i1 #-}
+      I-rec-seg : ∀ {p0} {p1} {p} -> cong (I-rec p0 p1 p) seg ≡ p
 
-primNat : ∀ {a} {A : Set a} -> A -> (ℕ -> A -> A) -> ℕ -> A
-primNat a f zero = a
-primNat a f (suc n) = f n (primNat a f n)
+-- I-rec-const : ∀ {p} {P : Set p} (p : P) -> ∀ i -> I-rec p p refl i ≡ p
+-- I-rec-const p = I-elim refl refl {!!}
 
-precNat : ∀ {a} {A : Set a} -> A -> (ℕ -> A -> A) -> ℕ -> A
-precNat a f n = recNat a (f n) n
+funext : ∀ {a b} {A : Set a} {B : Set b} {f g : A -> B} -> ((x : A) -> f x ≡ g x) -> f ≡ g
+funext {f = f} {g = g} H = cong (flip \a -> I-rec (f a) (g a) (H a)) seg
+
+happly : ∀ {a b} {A : Set a} {B : Set b} {f g : A -> B} -> f ≡ g -> (x : A) -> f x ≡ g x
+happly p x = cong (_$ x) p
+
+happly-funext : ∀ {a b} {A : Set a} {B : Set b} {f g : A -> B} (H : (x : A) -> f x ≡ g x) -> ∀ x -> happly (funext H) x ≡ H x
+happly-funext {f = f} {g = g} H x =
+  happly (funext H) x                                         ≡⟨ refl ⟩
+  cong (_$ x) (cong (flip \a -> I-rec (f a) (g a) (H a)) seg) ≡⟨ sym (cong-∘ seg) ⟩
+  cong ((_$ x) ∘ (flip \a -> I-rec (f a) (g a) (H a))) seg    ≡⟨ I-rec-seg ⟩
+  H x ∎
+  where open ≡-Reasoning
+
+-- funext-refl : ∀ {a b} {A : Set a} {B : Set b} {f : A -> B} -> funext (\x -> refl {x = f x}) ≡ refl {x = f}
+-- funext-refl {f = f} =
+--   cong (\y x -> I-rec (f x) (f x) refl y) seg ≡⟨ refl ⟩
+--   cong (\y -> (\x -> I-rec (f x) (f x) refl y)) seg ≡⟨ cong (\h -> cong (\y -> (\x -> h y)) seg) {!!} ⟩
+--   cong (\y -> (\x -> (\i -> f x) y)) seg ≡⟨ {!!} ⟩
+--   refl {x = f} ∎
+--   where open ≡-Reasoning
+
+-- funext-happly : ∀ {a b} {A : Set a} {B : Set b} {f g : A -> B} (p : f ≡ g) -> funext (happly p) ≡ p
+-- funext-happly {f = f} {g = g} p =
+--   funext (happly p)                                           ≡⟨ refl ⟩
+--   cong (flip \a -> I-rec (f a) (g a) (cong (_$ a) p)) seg     ≡⟨ refl ⟩
+--   cong (\i a -> I-rec (f a) (g a) (cong (\h -> h a) p) i) seg ≡⟨ {!!} ⟩
+--   cong (I-rec f g p) seg                                      ≡⟨ I-rec-seg ⟩
+--   p ∎
+--   where open ≡-Reasoning
+
+open import Data.Nat
+
+recNat : ∀ {a} {A : Set a} -> A -> (A -> A) -> ℕ -> A
+recNat a f zero = a
+recNat a f (suc n) = f (recNat a f n)
+
+primNat : ∀ {a} {A : Set a} -> A -> (ℕ -> A -> A) -> ℕ -> A
+primNat a f zero = a
+primNat a f (suc n) = f n (primNat a f n)
+
+precNat : ∀ {a} {A : Set a} -> A -> (ℕ -> A -> A) -> ℕ -> A
+precNat a f n = recNat a (f n) n
\ No newline at end of file diff --git a/Coexp.Semantics.html b/Coexp.Semantics.html index 5a7648b..fd9793f 100644 --- a/Coexp.Semantics.html +++ b/Coexp.Semantics.html @@ -33,7 +33,7 @@ distr = S.[ pmap id inj₁ , pmap id inj₂ ]′ ⊎-eta : {X Y Z : Set} -> S.[ inj₁ {B = Y} , inj₂ {A = X} ]′ ≡ id {A = X ⊎ Y} -⊎-eta = funext \{ (inj₁ x) -> refl ; (inj₂ y) -> refl } +⊎-eta = funext \{ (inj₁ x) -> refl ; (inj₂ y) -> refl } is-zero : ℕ -> ⊤ ⊎ ⊤ is-zero zero = inj₁ tt @@ -109,12 +109,24 @@ councurry : (Y × (X -> R) -> T Z) -> (Y -> T (X ⊎ Z)) councurry f y k = f (y , inj₁ ； k) (inj₂ ； k) - coeval : Y -> T (X ⊎ (Y × (X -> R))) - coeval = councurry T.eta + councurry-cocurry : (f : Y -> T (X ⊎ Z)) -> councurry (cocurry f) ≡ f + councurry-cocurry f = + funext \y -> funext \k -> + cong (f y) (funext \{ (inj₁ x) -> refl ; (inj₂ z) -> refl }) - coeval' : (X ⊎ Y) × (X -> R) -> T Y - coeval' = cocurry T.eta + cocurry-councurry : (g : Y × (X -> R) -> T Z) -> cocurry (councurry g) ≡ g + cocurry-councurry g = + funext \(y , k) -> refl - coeval'' : T (X ⊎ Y) × (X -> R) -> T Y - coeval'' = cocurry id + coeval : Y -> T (X ⊎ (Y × (X -> R))) + coeval = councurry T.eta + + couneval' : (X ⊎ Y) × (X -> R) -> T Y + couneval' = cocurry T.eta + + couneval : T (X ⊎ Y) × (X -> R) -> T Y + couneval = cocurry id + + 𝒜 : X × (X -> R) -> T Y + 𝒜 = cocurry (inj₁ ； T.eta) \ No newline at end of file