From 37880535fd43193967b1acca6621b129c0b94eb1 Mon Sep 17 00:00:00 2001 From: vikraman Date: Mon, 14 Oct 2024 17:02:33 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20vikraman?= =?UTF-8?q?/agda-coexp@366e260cd8f11d6fe2e5ccd0db979d80d9492881=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.Interp.html | 95 +++++++++++++ Coexp.Kappa.Syntax.html | 121 ++++++++-------- Coexp.KappaStar.Interp.html | 98 +++++++++++++ Coexp.KappaStar.Syntax.html | 131 +++++++++--------- Coexp.LamLamBar.Interp.html | 266 ++++++++++++++++++------------------ Coexp.Meta.Prelude.html | 55 +++++--- Coexp.Prelude.html | 152 ++++++++++----------- Coexp.Semantics.html | 175 +++++++++++++----------- Coexp.Zeta.Interp.html | 95 +++++++++++++ Coexp.Zeta.Syntax.html | 121 ++++++++-------- Coexp.ZetaStar.Interp.html | 104 ++++++++++++++ Coexp.ZetaStar.Syntax.html | 131 +++++++++--------- index.html | 22 +-- 13 files changed, 1005 insertions(+), 561 deletions(-) create mode 100644 Coexp.Kappa.Interp.html create mode 100644 Coexp.KappaStar.Interp.html create mode 100644 Coexp.Zeta.Interp.html create mode 100644 Coexp.ZetaStar.Interp.html diff --git a/Coexp.Kappa.Interp.html b/Coexp.Kappa.Interp.html new file mode 100644 index 0000000..fd3f270 --- /dev/null +++ b/Coexp.Kappa.Interp.html @@ -0,0 +1,95 @@ + +Coexp.Kappa.Interp
module Coexp.Kappa.Interp where
+
+open import Data.Nat
+open import Data.Unit
+open import Data.Empty
+open import Data.Product as P renaming (map to pmap)
+open import Data.Sum as S renaming (map to smap)
+open import Function using (const ; flip)
+open import Data.Bool hiding (T)
+open import Relation.Binary.PropositionalEquality
+
+open import Coexp.Prelude
+open import Coexp.Semantics
+open import Coexp.Kappa.Syntax
+
+interpTy : Ty -> Set
+interpTy `1       = ⊤
+interpTy (A `× B) = interpTy A × interpTy B
+
+interpCtx : Ctx -> Set
+interpCtx ε       = ⊤
+interpCtx (Γ ∙ A) = interpCtx Γ × interpTy A
+
+interpIn : A ∈ Γ -> interpCtx Γ -> ⊤ -> interpTy A
+interpIn h     = proj₂ ； elem
+interpIn (t i) = proj₁ ； interpIn i
+
+interpArr : Γ ⊢ A ->> B -> interpCtx Γ -> interpTy A -> interpTy B
+interpArr (var i)   = interpIn i
+interpArr id        = const idf
+interpArr bang      = const (const tt)
+interpArr (e1 ∘ e2) = < interpArr e1 , interpArr e2 > ； compose
+interpArr (lift e)  = curry (P.map₁ (flip (interpArr e) tt))
+interpArr (κ e)     = curry (interpArr e) ； uncurry
+
+interpWk : Wk Γ Δ -> interpCtx Γ -> interpCtx Δ
+interpWk wk-ε        = const tt
+interpWk (wk-cong π) = pmap (interpWk π) idf
+interpWk (wk-wk π)   = proj₁ ； interpWk π
+
+interpWk-id-coh : interpWk (wk-id {Γ}) ≡ idf
+interpWk-id-coh {Γ = ε} = refl
+interpWk-id-coh {Γ = Γ ∙ A} rewrite interpWk-id-coh {Γ} = refl
+{-# REWRITE interpWk-id-coh #-}
+
+interpSub : Sub Γ Δ -> interpCtx Γ -> interpCtx Δ
+interpSub sub-ε        = const tt
+interpSub (sub-ex θ e) = < interpSub θ , (_, tt) ； uncurry (interpArr e) >
+
+interpSub-mem-arr-coh : (θ : Sub Γ Δ) (i : A ∈ Δ) -> interpArr (sub-mem θ i) ≡ interpSub θ ； interpIn i
+interpSub-mem-arr-coh (sub-ex θ e) h     = refl
+interpSub-mem-arr-coh (sub-ex θ e) (t i) = interpSub-mem-arr-coh θ i
+
+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
+
+interpArr-wk-coh : (π : Wk Γ Δ) (e : Δ ⊢ A ->> B) -> interpArr (wk-arr π e) ≡ interpWk π ； interpArr e
+interpArr-wk-coh π (var i) = interpWk-mem-coh π i
+interpArr-wk-coh π id = refl
+interpArr-wk-coh π bang = refl
+interpArr-wk-coh π (e1 ∘ e2) rewrite interpArr-wk-coh π e1 | interpArr-wk-coh π e2 = refl
+interpArr-wk-coh π (lift e) rewrite interpArr-wk-coh π e = refl
+interpArr-wk-coh π (κ e) rewrite interpArr-wk-coh (wk-cong π) e = refl
+{-# REWRITE interpArr-wk-coh #-}
+
+interpSub-wk-coh : (π : Wk Γ Δ) (θ : Sub Δ Ψ) -> interpSub (sub-wk π θ) ≡ interpWk π ； interpSub θ
+interpSub-wk-coh π sub-ε = refl
+interpSub-wk-coh π (sub-ex θ e) rewrite interpSub-wk-coh π θ | interpArr-wk-coh π e = refl
+{-# REWRITE interpSub-wk-coh #-}
+
+interpSub-id-coh : interpSub (sub-id {Γ}) ≡ idf
+interpSub-id-coh {Γ = ε} = refl
+interpSub-id-coh {Γ = Γ ∙ A} = funext \p -> cong (_, p .proj₂) (happly interpSub-id-coh (p .proj₁))
+{-# REWRITE interpSub-id-coh #-}
+
+interpSub-arr-coh : (θ : Sub Γ Δ) (e : Δ ⊢ A ->> B) -> interpArr (sub-arr θ e) ≡ interpSub θ ； interpArr e
+interpSub-arr-coh θ (var i) = interpSub-mem-arr-coh θ i
+interpSub-arr-coh θ id = refl
+interpSub-arr-coh θ bang = refl
+interpSub-arr-coh θ (e1 ∘ e2) rewrite interpSub-arr-coh θ e1 | interpSub-arr-coh θ e2 = refl
+interpSub-arr-coh θ (lift e) rewrite interpSub-arr-coh θ e = refl
+interpSub-arr-coh θ (κ e) rewrite interpSub-arr-coh (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e = refl
+
+interpEq : Γ ⊢ e1 ≈ e2 ∶ A ->> B -> interpArr e1 ≡ interpArr e2
+interpEq (unitl _) = refl
+interpEq (unitr _) = refl
+interpEq (assoc _ _ _) = refl
+interpEq (term _ _) = refl
+interpEq (κ-beta f c) rewrite interpSub-arr-coh (sub-ex sub-id c) f = refl
+interpEq (κ-eta _) = refl
+
\ No newline at end of file diff --git a/Coexp.Kappa.Syntax.html b/Coexp.Kappa.Syntax.html index 4398366..6293af1 100644 --- a/Coexp.Kappa.Syntax.html +++ b/Coexp.Kappa.Syntax.html @@ -6,88 +6,91 @@ open import Data.Nat infixr 40 _`×_ -infixr 20 _∘_ +infixr 20 _∘_ data Ty : Set where `1 : Ty _`×_ : Ty -> Ty -> Ty -open Ctx Ty +open Ctx Ty public -syntax Arr Γ A B = Γ ⊢ A ->> B +syntax Arr Γ A B = Γ ⊢ A ->> B -data Arr : Ctx -> Ty -> Ty -> Set where +data Arr : Ctx -> Ty -> Ty -> Set where - var : (i : A ∈ Γ) - --------- - -> Γ ⊢ `1 ->> A + var : (i : A ∈ Γ) + --------- + -> Γ ⊢ `1 ->> A - id : - --------- - Γ ⊢ A ->> A + id : + --------- + Γ ⊢ A ->> A - bang : - ---------- - Γ ⊢ A ->> `1 + bang : + ---------- + Γ ⊢ A ->> `1 - _∘_ : Γ ⊢ B ->> C -> Γ ⊢ A ->> B - ------------------------------ - -> Γ ⊢ A ->> C + _∘_ : Γ ⊢ B ->> C -> Γ ⊢ A ->> B + ------------------------------ + -> Γ ⊢ A ->> C - lift : Γ ⊢ `1 ->> C - ------------------ - -> Γ ⊢ A ->> (C `× A) + lift : Γ ⊢ `1 ->> C + ------------------ + -> Γ ⊢ A ->> (C `× A) - κ : (Γ ∙ C) ⊢ A ->> B - ------------------ - -> Γ ⊢ C `× A ->> B + κ : (Γ ∙ C) ⊢ A ->> B + ------------------ + -> Γ ⊢ C `× A ->> B -wk-arr : Wk Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B -wk-arr π (var i) = var (wk-mem π i) -wk-arr π id = id -wk-arr π bang = bang -wk-arr π (e1 ∘ e2) = wk-arr π e1 ∘ wk-arr π e2 -wk-arr π (lift e) = lift (wk-arr π e) -wk-arr π (κ e) = κ (wk-arr (wk-cong π) e) +wk-arr : Wk Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B +wk-arr π (var i) = var (wk-mem π i) +wk-arr π id = id +wk-arr π bang = bang +wk-arr π (e1 ∘ e2) = wk-arr π e1 ∘ wk-arr π e2 +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 public +open SubVar `1 var public -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 : 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) -open SubArr sub-arr +open SubArr sub-arr -syntax Eq Γ A B e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A ->> B +variable + e e1 e2 e3 e4 : Γ ⊢ A ->> B -data Eq (Γ : Ctx) : (A B : Ty) -> Γ ⊢ A ->> B -> Γ ⊢ A ->> B -> Set where +syntax Eq Γ A B e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A ->> B - unitl : (f : Γ ⊢ A ->> B) - -------------- - -> Γ ⊢ f ≈ id ∘ f ∶ A ->> B +data Eq (Γ : Ctx) : (A B : Ty) -> Γ ⊢ A ->> B -> Γ ⊢ A ->> B -> Set where - unitr : (f : Γ ⊢ A ->> B) - -------------- - -> Γ ⊢ f ∘ id ≈ f ∶ A ->> B + unitl : (f : Γ ⊢ A ->> B) + -------------- + -> Γ ⊢ f ≈ id ∘ f ∶ A ->> B - assoc : (f : Γ ⊢ A ->> B) (g : Γ ⊢ B ->> C) (h : Γ ⊢ C ->> D) - --------------------------------------------------------- - -> Γ ⊢ (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) ∶ A ->> D + unitr : (f : Γ ⊢ A ->> B) + -------------- + -> Γ ⊢ f ∘ id ≈ f ∶ A ->> B - term : (f g : Γ ⊢ A ->> `1) - ------------------------- - -> Γ ⊢ f ≈ g ∶ A ->> `1 + assoc : (f : Γ ⊢ A ->> B) (g : Γ ⊢ B ->> C) (h : Γ ⊢ C ->> D) + --------------------------------------------------------- + -> Γ ⊢ (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) ∶ A ->> D - κ-beta : (f : (Γ ∙ C) ⊢ A ->> B) (c : Γ ⊢ `1 ->> C) - ------------------------------------------------ - -> Γ ⊢ κ {C = C} f ∘ lift {A = A} c ≈ sub c f ∶ A ->> B + term : (f g : Γ ⊢ A ->> `1) + ------------------------- + -> Γ ⊢ f ≈ g ∶ A ->> `1 - κ-eta : (f : Γ ⊢ C `× A ->> B) - --------------------------------------------------- - -> Γ ⊢ κ {C = C} (wk f ∘ lift {A = A} (var h)) ≈ f ∶ C `× A ->> B + κ-beta : (f : (Γ ∙ C) ⊢ A ->> B) (c : Γ ⊢ `1 ->> C) + ------------------------------------------------ + -> Γ ⊢ κ {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 \ No newline at end of file diff --git a/Coexp.KappaStar.Interp.html b/Coexp.KappaStar.Interp.html new file mode 100644 index 0000000..4fb90d1 --- /dev/null +++ b/Coexp.KappaStar.Interp.html @@ -0,0 +1,98 @@ + +Coexp.KappaStar.Interp
module Coexp.KappaStar.Interp (R : Set) where
+
+open import Data.Nat
+open import Data.Unit
+open import Data.Empty
+open import Data.Product as P renaming (map to pmap)
+open import Data.Sum as S renaming (map to smap)
+open import Function using (const ; flip ; _$_)
+open import Data.Bool hiding (T)
+open import Relation.Binary.PropositionalEquality
+
+open import Coexp.Prelude
+open import Coexp.Semantics
+open import Coexp.KappaStar.Syntax
+
+open Cont R
+
+interpTy : Ty -> Set
+interpTy `0 = ⊥
+interpTy (A `- B) = interpTy A × (interpTy B -> R)
+
+interpCtx : Ctx -> Set
+interpCtx ε       = ⊤
+interpCtx (Γ ∙ A) = interpCtx Γ × (interpTy A -> R)
+
+interpIn : A ∈ Γ -> interpCtx Γ -> interpTy A -> T ⊥
+interpIn h     = proj₂ ； coelem
+interpIn (t i) = proj₁ ； interpIn i
+
+interpArr : Γ ⊢ A ->> B -> interpCtx Γ -> interpTy A -> T (interpTy B)
+interpArr (covar i) = interpIn i
+interpArr id = const idk
+interpArr bang = const absurd
+interpArr (e1 ∘ e2) = < interpArr e1 , interpArr e2 > ； uncurry T.composek
+interpArr (lift* e) = curry (P.map₁ (curry (flip (uncurry (interpArr e)) absurd)) ； P.swap ； T.eta)
+interpArr (κ* e) = curry (interpArr e) ； uncurry ； flip contramap P.swap
+
+interpWk : Wk Γ Δ -> interpCtx Γ -> interpCtx Δ
+interpWk wk-ε        = const tt
+interpWk (wk-cong π) = pmap (interpWk π) idf
+interpWk (wk-wk π)   = proj₁ ； interpWk π
+
+interpWk-id-coh : interpWk (wk-id {Γ}) ≡ idf
+interpWk-id-coh {Γ = ε} = refl
+interpWk-id-coh {Γ = Γ ∙ A} rewrite interpWk-id-coh {Γ} = refl
+{-# REWRITE interpWk-id-coh #-}
+
+interpSub : Sub Γ Δ -> interpCtx Γ -> interpCtx Δ
+interpSub sub-ε        = const tt
+interpSub (sub-ex θ e) = < interpSub θ , interpArr e ； curry (eval ； (_$ absurd)) >
+
+interpSub-mem-arr-coh : (θ : Sub Γ Δ) (i : A ∈ Δ) -> interpArr (sub-mem θ i) ≡ interpSub θ ； interpIn i
+interpSub-mem-arr-coh (sub-ex θ e) h =
+  funext (\γ -> funext \k -> funext \f -> cong (interpArr e γ k) (absurd-eta f ⊥-elim))
+interpSub-mem-arr-coh (sub-ex θ e) (t i) = interpSub-mem-arr-coh θ i
+
+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
+
+interpArr-wk-coh : (π : Wk Γ Δ) (e : Δ ⊢ A ->> B) -> interpArr (wk-arr π e) ≡ interpWk π ； interpArr e
+interpArr-wk-coh π (covar i) = interpWk-mem-coh π i
+interpArr-wk-coh π id = refl
+interpArr-wk-coh π bang = refl
+interpArr-wk-coh π (e1 ∘ e2) rewrite interpArr-wk-coh π e1 | interpArr-wk-coh π e2 = refl
+interpArr-wk-coh π (lift* e) rewrite interpArr-wk-coh π e = refl
+interpArr-wk-coh π (κ* e) rewrite interpArr-wk-coh (wk-cong π) e = refl
+{-# REWRITE interpArr-wk-coh #-}
+
+interpSub-wk-coh : (π : Wk Γ Δ) (θ : Sub Δ Ψ) -> interpSub (sub-wk π θ) ≡ interpWk π ； interpSub θ
+interpSub-wk-coh π sub-ε = refl
+interpSub-wk-coh π (sub-ex θ e) rewrite interpSub-wk-coh π θ | interpArr-wk-coh π e = refl
+{-# REWRITE interpSub-wk-coh #-}
+
+interpSub-id-coh : interpSub (sub-id {Γ}) ≡ idf
+interpSub-id-coh {Γ = ε} = refl
+interpSub-id-coh {Γ = Γ ∙ A} = funext \p -> cong (_, p .proj₂) (happly interpSub-id-coh (p .proj₁))
+{-# REWRITE interpSub-id-coh #-}
+
+interpSub-arr-coh : (θ : Sub Γ Δ) (e : Δ ⊢ A ->> B) -> interpArr (sub-arr θ e) ≡ interpSub θ ； interpArr e
+interpSub-arr-coh θ (covar i) = interpSub-mem-arr-coh θ i
+interpSub-arr-coh θ id = refl
+interpSub-arr-coh θ bang = refl
+interpSub-arr-coh θ (e1 ∘ e2) rewrite interpSub-arr-coh θ e1 | interpSub-arr-coh θ e2 = refl
+interpSub-arr-coh θ (lift* e) rewrite interpSub-arr-coh θ e = refl
+interpSub-arr-coh θ (κ* e) rewrite interpSub-arr-coh (sub-ex (sub-wk (wk-wk wk-id) θ) (covar h)) e = refl
+
+interpEq : Γ ⊢ e1 ≈ e2 ∶ A ->> B -> interpArr e1 ≡ interpArr e2
+interpEq (unitl _) = refl
+interpEq (unitr _) = refl
+interpEq (assoc _ _ _) = refl
+interpEq (term f g) = funext \γ -> absurd-eta (interpArr f γ) (interpArr g γ)
+interpEq (κ*-beta f c) rewrite interpSub-arr-coh (sub-ex sub-id c) f = refl
+interpEq (κ*-eta _) = refl
+
\ No newline at end of file diff --git a/Coexp.KappaStar.Syntax.html b/Coexp.KappaStar.Syntax.html index c3d25bd..9588752 100644 --- a/Coexp.KappaStar.Syntax.html +++ b/Coexp.KappaStar.Syntax.html @@ -5,91 +5,92 @@ open import Coexp.Meta.Prelude open import Data.Nat -infix 50 _* -infixr 40 _`-_ -infixr 20 _∘_ +infixr 40 _`-_ +infixr 20 _∘_ -data Ty : Set where - `1 : Ty - _* : Ty -> Ty - _`-_ : Ty -> Ty -> Ty +data Ty : Set where + `0 : Ty + _`-_ : Ty -> Ty -> Ty -open Ctx Ty +open Ctx Ty public -syntax Arr Γ A B = Γ ⊢ A ->> B +syntax Arr Γ A B = Γ ⊢ A ->> B -data Arr : Ctx -> Ty -> Ty -> Set where +data Arr : Ctx -> Ty -> Ty -> Set where - var : (i : A ∈ Γ) - --------- - -> Γ ⊢ `1 ->> A + covar : (i : A ∈ Γ) + --------- + -> Γ ⊢ A ->> `0 - id : - --------- - Γ ⊢ A ->> A + id : + --------- + Γ ⊢ A ->> A - bang : - ---------- - Γ ⊢ A ->> `1 + bang : + ---------- + Γ ⊢ `0 ->> A - _∘_ : Γ ⊢ B ->> C -> Γ ⊢ A ->> B - ------------------------------ - -> Γ ⊢ A ->> C + _∘_ : Γ ⊢ B ->> C -> Γ ⊢ A ->> B + ------------------------------ + -> Γ ⊢ A ->> C - lift* : Γ ⊢ `1 ->> C * - --------------------- - -> Γ ⊢ A ->> (A `- C) + lift* : Γ ⊢ C ->> `0 + --------------------- + -> Γ ⊢ A ->> (A `- C) - κ* : (Γ ∙ C *) ⊢ A ->> B - ----------------------- - -> Γ ⊢ (A `- C) ->> B + κ* : (Γ ∙ C) ⊢ A ->> B + ----------------------- + -> Γ ⊢ (A `- C) ->> B -wk-arr : Wk Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B -wk-arr π (var i) = var (wk-mem π i) -wk-arr π id = id -wk-arr π bang = bang -wk-arr π (e1 ∘ e2) = wk-arr π e1 ∘ wk-arr π e2 -wk-arr π (lift* e) = lift* (wk-arr π e) -wk-arr π (κ* e) = κ* (wk-arr (wk-cong π) e) +wk-arr : Wk Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B +wk-arr π (covar i) = covar (wk-mem π i) +wk-arr π id = id +wk-arr π bang = bang +wk-arr π (e1 ∘ e2) = wk-arr π e1 ∘ wk-arr π e2 +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 public +open SubCoVar `0 covar public -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 : Sub Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B +sub-arr θ (covar 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) θ) (covar h)) e) -open SubArr sub-arr +open SubArr sub-arr -syntax Eq Γ A B e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A ->> B +variable + e e1 e2 e3 e4 : Γ ⊢ A ->> B -data Eq (Γ : Ctx) : (A B : Ty) -> Γ ⊢ A ->> B -> Γ ⊢ A ->> B -> Set where +syntax Eq Γ A B e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A ->> B - unitl : (f : Γ ⊢ A ->> B) - -------------- - -> Γ ⊢ f ≈ id ∘ f ∶ A ->> B +data Eq (Γ : Ctx) : (A B : Ty) -> Γ ⊢ A ->> B -> Γ ⊢ A ->> B -> Set where - unitr : (f : Γ ⊢ A ->> B) - -------------- - -> Γ ⊢ f ∘ id ≈ f ∶ A ->> B + unitl : (f : Γ ⊢ A ->> B) + -------------- + -> Γ ⊢ f ≈ id ∘ f ∶ A ->> B - assoc : (f : Γ ⊢ A ->> B) (g : Γ ⊢ B ->> C) (h : Γ ⊢ C ->> D) - --------------------------------------------------------- - -> Γ ⊢ (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) ∶ A ->> D + unitr : (f : Γ ⊢ A ->> B) + -------------- + -> Γ ⊢ f ∘ id ≈ f ∶ A ->> B - term : (f g : Γ ⊢ A ->> `1) - ------------------------- - -> Γ ⊢ f ≈ g ∶ A ->> `1 + assoc : (f : Γ ⊢ A ->> B) (g : Γ ⊢ B ->> C) (h : Γ ⊢ C ->> D) + --------------------------------------------------------- + -> Γ ⊢ (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) ∶ A ->> D - κ*-beta : (f : (Γ ∙ C *) ⊢ A ->> B) (c : Γ ⊢ `1 ->> C *) - ------------------------------------------------ - -> Γ ⊢ κ* {C = C} f ∘ lift* {A = A} c ≈ sub c f ∶ A ->> B + term : (f g : Γ ⊢ `0 ->> A) + ------------------------- + -> Γ ⊢ f ≈ g ∶ `0 ->> A - κ*-eta : (f : Γ ⊢ (A `- C) ->> B) - --------------------------------------------------- - -> Γ ⊢ κ* {C = C} (wk f ∘ lift* {A = A} (var h)) ≈ f ∶ (A `- C) ->> B + κ*-beta : (f : (Γ ∙ C) ⊢ A ->> B) (c : Γ ⊢ C ->> `0) + ------------------------------------------------ + -> Γ ⊢ κ* {C = C} f ∘ lift* {A = A} c ≈ sub c f ∶ A ->> B + + κ*-eta : (f : Γ ⊢ (A `- C) ->> B) + --------------------------------------------------- + -> Γ ⊢ κ* {C = C} (wk f ∘ lift* {A = A} (covar h)) ≈ f ∶ (A `- C) ->> B \ No newline at end of file diff --git a/Coexp.LamLamBar.Interp.html b/Coexp.LamLamBar.Interp.html index 034e4f4..36d671f 100644 --- a/Coexp.LamLamBar.Interp.html +++ b/Coexp.LamLamBar.Interp.html @@ -14,7 +14,7 @@ open import Coexp.Semantics open import Coexp.LamLamBar.Syntax -open Cont R +open Cont R -- interpretation of types -- functions are kleisli arrows @@ -23,7 +23,7 @@ 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 -> T (interpTy B) interpTy (A `+ B) = interpTy A ⊎ interpTy B -- interpretation of contexts @@ -37,39 +37,39 @@ interpIn (t i) = proj₁ ； interpIn i -- interpretation of terms -interpTm : Γ ⊢ A -> interpCtx Γ -> T (interpTy A) +interpTm : Γ ⊢ A -> interpCtx Γ -> T (interpTy A) interpTm (nat n) = - const n ； T.eta + const n ； T.eta interpTm (zero? e) = - interpTm e ； T.map is-zero + interpTm e ； T.map is-zero interpTm (var i) = - interpIn i ； T.eta + interpIn i ； T.eta interpTm (lam e) = - curry (interpTm e) ； T.eta + 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 + 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 + in < f , g > ； T.beta interpTm (fst e) = - interpTm e ； T.map proj₁ + interpTm e ； T.map proj₁ interpTm (snd e) = - interpTm e ； T.map proj₂ + interpTm e ； T.map proj₂ interpTm unit = - const tt ； T.eta + const tt ； T.eta interpTm (inl e) = - interpTm e ； T.map inj₁ + interpTm e ； T.map inj₁ interpTm (inr e) = - interpTm e ； T.map inj₂ + 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 + in < id , f > ； T.tau ； T.map distl ； T.map S.[ g1 , g2 ] ； T.mu interpTm (colam e) = - councurry (interpTm 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 + in < f , g > ； T.tau ； T.map couneval ； T.mu -- interpretation of weakening interpWk : Wk Γ Δ -> interpCtx Γ -> interpCtx Δ @@ -101,7 +101,7 @@ 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 }) + 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 #-} @@ -109,7 +109,7 @@ -- 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 (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₁ @@ -120,7 +120,7 @@ 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 : (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 @@ -177,7 +177,7 @@ 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 : (θ : 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 @@ -185,11 +185,11 @@ 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 ⟩ + 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 @@ -208,13 +208,13 @@ | 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 }) + 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 ⟩ + 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 @@ -231,7 +231,7 @@ k n evalTm (zero? e) γ k = evalTm e γ \n -> - k (is-zero n) + k (is-zero n) evalTm (var i) γ k = k (lookup i γ) evalTm (lam e) γ k = @@ -293,12 +293,12 @@ 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 }) + 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 })) + funext \γ -> funext \k -> + cong (evalTm e2 γ) (funext \k1 -> cong (evalTm e1 γ) (funext \{ (inj₁ a) -> refl ; (inj₂ b) -> refl })) -- soundness of equational theory @@ -308,14 +308,14 @@ 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 : Γ ⊢ 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 + 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 + 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 @@ -331,65 +331,65 @@ 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 ⟩ + < 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 : (π : 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-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 ∎ + 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 ∎ + 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 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 ∎ + 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 ∎ + 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 @@ -400,42 +400,42 @@ 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-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 (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 (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 ； 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) ⟩ + 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) ； 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 ⟩ @@ -443,84 +443,84 @@ 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) ⟩ + 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 , 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 , 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 ⟩ + < 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) ⟩ + 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₂ ∎ + 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 ⟩ + 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 ⟩ + 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 ⟩ + < 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 @@ -528,9 +528,9 @@ 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 ⟩ + 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 diff --git a/Coexp.Meta.Prelude.html b/Coexp.Meta.Prelude.html index bf1697f..4a060b3 100644 --- a/Coexp.Meta.Prelude.html +++ b/Coexp.Meta.Prelude.html @@ -95,26 +95,49 @@ 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 SubVar (`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 + + module SubCoVar (`0 : Ty) (covar : ∀ {A Γ} -> A ∈ Γ -> Arr Γ A `0) where + + data Sub (Γ : Ctx) : (Δ : Ctx) -> Set where + sub-ε : Sub Γ ε + sub-ex : (θ : Sub Γ Δ) -> (e : Arr Γ A `0) -> Sub Γ (Δ ∙ A) + + sub-mem : Sub Γ Δ -> A ∈ Δ -> Arr Γ A `0 + 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-id : Sub Γ Γ + sub-id {Γ = ε} = sub-ε + sub-id {Γ = Γ ∙ A} = sub-ex (sub-wk (wk-wk wk-id) sub-id) (covar h) + + module SubArr (sub-arr : ∀ {A B Γ Δ} -> Sub Γ Δ -> Arr Δ A B -> Arr Γ A B) where + + sub : Arr Γ A `0 -> 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.Prelude.html b/Coexp.Prelude.html index aa38a8a..e968bc8 100644 --- a/Coexp.Prelude.html +++ b/Coexp.Prelude.html @@ -1,82 +1,78 @@ Coexp.Prelude
module Coexp.Prelude where
 
-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
-
-{-# BUILTIN REWRITE _≡_ #-}
-
-module _ where
-  postulate
-    I : Set
-    i0 i1 : I
-    seg : i0 ≡ i1
-
-  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 #-}
-
-  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
-
--- 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 {!!}
-
-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
+open import Function
+open import Relation.Binary.PropositionalEquality
+
+postulate
+  TODO : ∀ {a} {A : Set a} -> A
+
+{-# BUILTIN REWRITE _≡_ #-}
+
+module _ where
+  postulate
+    I : Set
+    i0 i1 : I
+    seg : i0 ≡ i1
+
+  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 #-}
+
+  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
+
+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 fd9793f..ae76493 100644 --- a/Coexp.Semantics.html +++ b/Coexp.Semantics.html @@ -26,107 +26,128 @@ eval : {X Y : Set} -> (X -> Y) × X -> Y eval (f , x) = f x -distl : {X Y Z : Set} -> X × (Y ⊎ Z) -> X × Y ⊎ X × Z -distl = uncurry \x -> S.[ (x ,_) ； inj₁ , (x ,_) ； inj₂ ]′ +contramap : {X Y Z : Set} -> (X -> Y) -> (Z -> X) -> (Z -> Y) +contramap = _∘′_ -distr : {X Y Z : Set} -> X × Y ⊎ X × Z -> X × (Y ⊎ Z) -distr = S.[ pmap id inj₁ , pmap id inj₂ ]′ +compose : {X Y Z : Set} -> (Y -> Z) × (X -> Y) -> X -> Z +compose = uncurry contramap -⊎-eta : {X Y Z : Set} -> S.[ inj₁ {B = Y} , inj₂ {A = X} ]′ ≡ id {A = X ⊎ Y} -⊎-eta = funext \{ (inj₁ x) -> refl ; (inj₂ y) -> refl } +distl : {X Y Z : Set} -> X × (Y ⊎ Z) -> X × Y ⊎ X × Z +distl = uncurry \x -> S.[ (x ,_) ； inj₁ , (x ,_) ； inj₂ ]′ -is-zero : ℕ -> ⊤ ⊎ ⊤ -is-zero zero = inj₁ tt -is-zero (suc n) = inj₂ tt +distr : {X Y Z : Set} -> X × Y ⊎ X × Z -> X × (Y ⊎ Z) +distr = S.[ pmap id inj₁ , pmap id inj₂ ]′ -variable - X Y Z : Set - x y z : X +⊎-eta : {X Y Z : Set} -> S.[ inj₁ {B = Y} , inj₂ {A = X} ]′ ≡ id {A = X ⊎ Y} +⊎-eta = funext \{ (inj₁ x) -> refl ; (inj₂ y) -> refl } --- strong monad T -record MonadStructure (T : Set -> Set) : Set₁ where - field - map : ∀ {X Y} -> (X -> Y) -> T X -> T Y - map-id : map id ≡ id {A = T X} - map-comp : {f : X -> Y} {g : Y -> Z} -> map (f ； g) ≡ map f ； map g - eta : ∀ {X} -> X -> T X - mu : ∀ {X} -> T (T X) -> T X - unitl : map {Y = T X} eta ； mu ≡ id - unitr : eta {X = T X} ； mu ≡ id - assoc : mu {X = T X} ； mu ≡ map {Y = T X} mu ； mu +absurd : {X : Set} -> ⊥ -> X +absurd = ⊥-elim - -- haskell's bind - bind : T X × (X -> T Y) -> T Y - bind (k , f) = mu (map f k) +absurd-eta : {X : Set} -> (f g : ⊥ -> X) -> f ≡ g +absurd-eta f g = funext λ () - -- kleisli lift - lift : (X -> Y) -> X -> T Y - lift = eta ∘_ +is-zero : ℕ -> ⊤ ⊎ ⊤ +is-zero zero = inj₁ tt +is-zero (suc n) = inj₂ tt - -- kleisli extension - extend : (X -> T Y) -> T X -> T Y - extend f = map f ； mu +variable + X Y Z : Set + x y z : X - -- strength combinators - tau : X × T Y -> T (X × Y) - tau (x , k) = map (\z -> x , z) k +-- strong monad T +record MonadStructure (T : Set -> Set) : Set₁ where + field + map : ∀ {X Y} -> (X -> Y) -> T X -> T Y + map-id : map id ≡ id {A = T X} + map-comp : {f : X -> Y} {g : Y -> Z} -> map (f ； g) ≡ map f ； map g + eta : ∀ {X} -> X -> T X + mu : ∀ {X} -> T (T X) -> T X + unitl : map {Y = T X} eta ； mu ≡ id + unitr : eta {X = T X} ； mu ≡ id + assoc : mu {X = T X} ； mu ≡ map {Y = T X} mu ； mu - sigma : T X × Y -> T (X × Y) - sigma (k , y) = map (\z -> z , y) k + -- haskell's bind + bind : T X × (X -> T Y) -> T Y + bind (k , f) = mu (map f k) - alpha : T X × T Y -> T (X × Y) - alpha = sigma ； map tau ； mu + -- kleisli lift + lift : (X -> Y) -> X -> T Y + lift = eta ∘_ - beta : T X × T Y -> T (X × Y) - beta = tau ； map sigma ； mu + -- kleisli extension + extend : (X -> T Y) -> T X -> T Y + extend f = map f ； mu - -- haskell's applicative - ap : T (X -> Y) -> T X -> T Y - ap = curry (beta ； map eval) + composek : (Y -> T Z) -> (X -> T Y) -> X -> T Z + composek g f = f ； extend g -open MonadStructure + -- strength combinators + tau : X × T Y -> T (X × Y) + tau (x , k) = map (\z -> x , z) k -module Cont (R : Set) where + sigma : T X × Y -> T (X × Y) + sigma (k , y) = map (\z -> z , y) k - T : Set -> Set - T X = (X -> R) -> R + alpha : T X × T Y -> T (X × Y) + alpha = sigma ； map tau ； mu - M : MonadStructure T - map M f g k = g (f ； k) - map-id M = refl - map-comp M = refl - eta M x k = k x - mu M g k = g \h -> h k - unitl M = refl - unitr M = refl - assoc M = refl + beta : T X × T Y -> T (X × Y) + beta = tau ； map sigma ； mu - module T = MonadStructure M + -- haskell's applicative + ap : T (X -> Y) -> T X -> T Y + ap = curry (beta ； map eval) - cocurry : (Y -> T (X ⊎ Z)) -> (Y × (X -> R) -> T Z) - cocurry f (y , k1) k2 = f y S.[ k1 , k2 ]′ +open MonadStructure - councurry : (Y × (X -> R) -> T Z) -> (Y -> T (X ⊎ Z)) - councurry f y k = f (y , inj₁ ； k) (inj₂ ； k) +module Cont (R : Set) where - 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 }) + T : Set -> Set + T X = (X -> R) -> R - cocurry-councurry : (g : Y × (X -> R) -> T Z) -> cocurry (councurry g) ≡ g - cocurry-councurry g = - funext \(y , k) -> refl + M : MonadStructure T + map M f g k = g (f ； k) + map-id M = refl + map-comp M = refl + eta M x k = k x + mu M g k = g \h -> h k + unitl M = refl + unitr M = refl + assoc M = refl - coeval : Y -> T (X ⊎ (Y × (X -> R))) - coeval = councurry T.eta + module T = MonadStructure M - couneval' : (X ⊎ Y) × (X -> R) -> T Y - couneval' = cocurry T.eta + cocurry : (Y -> T (X ⊎ Z)) -> (Y × (X -> R) -> T Z) + cocurry f (y , k1) k2 = f y S.[ k1 , k2 ]′ - couneval : T (X ⊎ Y) × (X -> R) -> T Y - couneval = cocurry id + councurry : (Y × (X -> R) -> T Z) -> (Y -> T (X ⊎ Z)) + councurry f y k = f (y , inj₁ ； k) (inj₂ ； k) - 𝒜 : X × (X -> R) -> T Y - 𝒜 = cocurry (inj₁ ； 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 }) + + cocurry-councurry : (g : Y × (X -> R) -> T Z) -> cocurry (councurry g) ≡ g + cocurry-councurry g = + funext \(y , k) -> refl + + 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) + + idk : {X : Set} -> X -> T X + idk = T.eta + + coelem : {X : Set} -> (X -> R) -> X -> T ⊥ + coelem = const ； flip \ No newline at end of file diff --git a/Coexp.Zeta.Interp.html b/Coexp.Zeta.Interp.html new file mode 100644 index 0000000..6938228 --- /dev/null +++ b/Coexp.Zeta.Interp.html @@ -0,0 +1,95 @@ + +Coexp.Zeta.Interp
module Coexp.Zeta.Interp where
+
+open import Data.Nat
+open import Data.Unit
+open import Data.Empty
+open import Data.Product as P renaming (map to pmap)
+open import Data.Sum as S renaming (map to smap)
+open import Function using (const ; flip)
+open import Data.Bool hiding (T)
+open import Relation.Binary.PropositionalEquality
+
+open import Coexp.Prelude
+open import Coexp.Semantics
+open import Coexp.Zeta.Syntax
+
+interpTy : Ty -> Set
+interpTy `1       = ⊤
+interpTy (A `⇒ B) = interpTy A -> interpTy B
+
+interpCtx : Ctx -> Set
+interpCtx ε       = ⊤
+interpCtx (Γ ∙ A) = interpCtx Γ × interpTy A
+
+interpIn : A ∈ Γ -> interpCtx Γ -> ⊤ -> interpTy A
+interpIn h     = proj₂ ； elem
+interpIn (t i) = proj₁ ； interpIn i
+
+interpArr : Γ ⊢ A ->> B -> interpCtx Γ -> interpTy A -> interpTy B
+interpArr (var i) = interpIn i
+interpArr id = const idf
+interpArr bang = const (const tt)
+interpArr (e1 ∘ e2) = < interpArr e1 , interpArr e2 > ； compose
+interpArr (pass e) = curry (P.map₁ (flip (interpArr e) tt) ； P.swap ； eval)
+interpArr (ζ f) = curry (interpArr f) ； flip
+
+interpWk : Wk Γ Δ -> interpCtx Γ -> interpCtx Δ
+interpWk wk-ε        = const tt
+interpWk (wk-cong π) = pmap (interpWk π) idf
+interpWk (wk-wk π)   = proj₁ ； interpWk π
+
+interpWk-id-coh : interpWk (wk-id {Γ}) ≡ idf
+interpWk-id-coh {Γ = ε} = refl
+interpWk-id-coh {Γ = Γ ∙ A} rewrite interpWk-id-coh {Γ} = refl
+{-# REWRITE interpWk-id-coh #-}
+
+interpSub : Sub Γ Δ -> interpCtx Γ -> interpCtx Δ
+interpSub sub-ε        = const tt
+interpSub (sub-ex θ e) = < interpSub θ , (_, tt) ； uncurry (interpArr e) >
+
+interpSub-mem-arr-coh : (θ : Sub Γ Δ) (i : A ∈ Δ) -> interpArr (sub-mem θ i) ≡ interpSub θ ； interpIn i
+interpSub-mem-arr-coh (sub-ex θ e) h     = refl
+interpSub-mem-arr-coh (sub-ex θ e) (t i) = interpSub-mem-arr-coh θ i
+
+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
+
+interpArr-wk-coh : (π : Wk Γ Δ) (e : Δ ⊢ A ->> B) -> interpArr (wk-arr π e) ≡ interpWk π ； interpArr e
+interpArr-wk-coh π (var i) = interpWk-mem-coh π i
+interpArr-wk-coh π id = refl
+interpArr-wk-coh π bang = refl
+interpArr-wk-coh π (e1 ∘ e2) rewrite interpArr-wk-coh π e1 | interpArr-wk-coh π e2 = refl
+interpArr-wk-coh π (pass e) rewrite interpArr-wk-coh π e = refl
+interpArr-wk-coh π (ζ e) rewrite interpArr-wk-coh (wk-cong π) e = refl
+{-# REWRITE interpArr-wk-coh #-}
+
+interpSub-wk-coh : (π : Wk Γ Δ) (θ : Sub Δ Ψ) -> interpSub (sub-wk π θ) ≡ interpWk π ； interpSub θ
+interpSub-wk-coh π sub-ε = refl
+interpSub-wk-coh π (sub-ex θ e) rewrite interpSub-wk-coh π θ | interpArr-wk-coh π e = refl
+{-# REWRITE interpSub-wk-coh #-}
+
+interpSub-id-coh : interpSub (sub-id {Γ}) ≡ idf
+interpSub-id-coh {Γ = ε} = refl
+interpSub-id-coh {Γ = Γ ∙ A} = funext \p -> cong (_, p .proj₂) (happly interpSub-id-coh (p .proj₁))
+{-# REWRITE interpSub-id-coh #-}
+
+interpSub-arr-coh : (θ : Sub Γ Δ) (e : Δ ⊢ A ->> B) -> interpArr (sub-arr θ e) ≡ interpSub θ ； interpArr e
+interpSub-arr-coh θ (var i) = interpSub-mem-arr-coh θ i
+interpSub-arr-coh θ id = refl
+interpSub-arr-coh θ bang = refl
+interpSub-arr-coh θ (e1 ∘ e2) rewrite interpSub-arr-coh θ e1 | interpSub-arr-coh θ e2 = refl
+interpSub-arr-coh θ (pass e) rewrite interpSub-arr-coh θ e = refl
+interpSub-arr-coh θ (ζ e) rewrite interpSub-arr-coh (sub-ex (sub-wk (wk-wk wk-id) θ) (var h)) e = refl
+
+interpEq : Γ ⊢ e1 ≈ e2 ∶ A ->> B -> interpArr e1 ≡ interpArr e2
+interpEq (unitl _) = refl
+interpEq (unitr _) = refl
+interpEq (assoc _ _ _) = refl
+interpEq (term _ _) = refl
+interpEq (ζ-beta f c) rewrite interpSub-arr-coh (sub-ex sub-id c) f = refl
+interpEq (ζ-eta _) = refl
+
\ No newline at end of file diff --git a/Coexp.Zeta.Syntax.html b/Coexp.Zeta.Syntax.html index 49ebb6d..4219515 100644 --- a/Coexp.Zeta.Syntax.html +++ b/Coexp.Zeta.Syntax.html @@ -6,88 +6,91 @@ open import Data.Nat infixr 40 _`⇒_ -infixr 20 _∘_ +infixr 20 _∘_ data Ty : Set where `1 : Ty _`⇒_ : Ty -> Ty -> Ty -open Ctx Ty +open Ctx Ty public -syntax Arr Γ A B = Γ ⊢ A ->> B +syntax Arr Γ A B = Γ ⊢ A ->> B -data Arr : Ctx -> Ty -> Ty -> Set where +data Arr : Ctx -> Ty -> Ty -> Set where - var : (i : A ∈ Γ) - --------- - -> Γ ⊢ `1 ->> A + var : (i : A ∈ Γ) + --------- + -> Γ ⊢ `1 ->> A - id : - --------- - Γ ⊢ A ->> A + id : + --------- + Γ ⊢ A ->> A - bang : - ---------- - Γ ⊢ A ->> `1 + bang : + ---------- + Γ ⊢ A ->> `1 - _∘_ : Γ ⊢ B ->> C -> Γ ⊢ A ->> B - ------------------------------ - -> Γ ⊢ A ->> C + _∘_ : Γ ⊢ B ->> C -> Γ ⊢ A ->> B + ------------------------------ + -> Γ ⊢ A ->> C - pass : Γ ⊢ `1 ->> C - ------------------ - -> Γ ⊢ (C `⇒ B) ->> B + pass : Γ ⊢ `1 ->> C + ------------------ + -> Γ ⊢ (C `⇒ B) ->> B - ζ : (Γ ∙ C) ⊢ A ->> B - ------------------ - -> Γ ⊢ A ->> (C `⇒ B) + ζ : (Γ ∙ C) ⊢ A ->> B + ------------------ + -> Γ ⊢ A ->> (C `⇒ B) -wk-arr : Wk Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B -wk-arr π (var i) = var (wk-mem π i) -wk-arr π id = id -wk-arr π bang = bang -wk-arr π (e1 ∘ e2) = wk-arr π e1 ∘ wk-arr π e2 -wk-arr π (pass e) = pass (wk-arr π e) -wk-arr π (ζ e) = ζ (wk-arr (wk-cong π) e) +wk-arr : Wk Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B +wk-arr π (var i) = var (wk-mem π i) +wk-arr π id = id +wk-arr π bang = bang +wk-arr π (e1 ∘ e2) = wk-arr π e1 ∘ wk-arr π e2 +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 public +open SubVar `1 var public -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 : 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) -open SubArr sub-arr +open SubArr sub-arr -syntax Eq Γ A B e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A ->> B +variable + e e1 e2 e3 e4 : Γ ⊢ A ->> B -data Eq (Γ : Ctx) : (A B : Ty) -> Γ ⊢ A ->> B -> Γ ⊢ A ->> B -> Set where +syntax Eq Γ A B e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A ->> B - unitl : (f : Γ ⊢ A ->> B) - -------------- - -> Γ ⊢ f ≈ id ∘ f ∶ A ->> B +data Eq (Γ : Ctx) : (A B : Ty) -> Γ ⊢ A ->> B -> Γ ⊢ A ->> B -> Set where - unitr : (f : Γ ⊢ A ->> B) - -------------- - -> Γ ⊢ f ∘ id ≈ f ∶ A ->> B + unitl : (f : Γ ⊢ A ->> B) + -------------- + -> Γ ⊢ f ≈ id ∘ f ∶ A ->> B - assoc : (f : Γ ⊢ A ->> B) (g : Γ ⊢ B ->> C) (h : Γ ⊢ C ->> D) - --------------------------------------------------------- - -> Γ ⊢ (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) ∶ A ->> D + unitr : (f : Γ ⊢ A ->> B) + -------------- + -> Γ ⊢ f ∘ id ≈ f ∶ A ->> B - term : (f g : Γ ⊢ A ->> `1) - ------------------------- - -> Γ ⊢ f ≈ g ∶ A ->> `1 + assoc : (f : Γ ⊢ A ->> B) (g : Γ ⊢ B ->> C) (h : Γ ⊢ C ->> D) + --------------------------------------------------------- + -> Γ ⊢ (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) ∶ A ->> D - ζ-beta : (f : (Γ ∙ C) ⊢ A ->> B) (c : Γ ⊢ `1 ->> C) - ------------------------------------------------ - -> Γ ⊢ pass {B = B} c ∘ ζ {C = C} f ≈ sub c f ∶ A ->> B + term : (f g : Γ ⊢ A ->> `1) + ------------------------- + -> Γ ⊢ f ≈ g ∶ A ->> `1 - ζ-eta : (f : Γ ⊢ A ->> (C `⇒ B)) - ------------------------------------ - -> Γ ⊢ ζ {C = C} (pass {B = B} (var h) ∘ wk f) ≈ f ∶ A ->> (C `⇒ B) + ζ-beta : (f : (Γ ∙ C) ⊢ A ->> B) (c : Γ ⊢ `1 ->> C) + ------------------------------------------------ + -> Γ ⊢ 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) \ No newline at end of file diff --git a/Coexp.ZetaStar.Interp.html b/Coexp.ZetaStar.Interp.html new file mode 100644 index 0000000..1bd5bff --- /dev/null +++ b/Coexp.ZetaStar.Interp.html @@ -0,0 +1,104 @@ + +Coexp.ZetaStar.Interp
module Coexp.ZetaStar.Interp (R : Set) where
+
+open import Data.Nat
+open import Data.Unit
+open import Data.Empty
+open import Data.Product as P renaming (map to pmap)
+open import Data.Sum as S renaming (map to smap)
+open import Function using (const ; flip ; _$_)
+open import Data.Bool hiding (T)
+open import Relation.Binary.PropositionalEquality
+
+open import Coexp.Prelude
+open import Coexp.Semantics
+open import Coexp.ZetaStar.Syntax
+
+open Cont R
+
+interpTy : Ty -> Set
+interpTy `0 = ⊥
+interpTy (A `+ B) = interpTy A ⊎ interpTy B
+
+interpCtx : Ctx -> Set
+interpCtx ε       = ⊤
+interpCtx (Γ ∙ A) = interpCtx Γ × (interpTy A -> R)
+
+interpIn : A ∈ Γ -> interpCtx Γ -> interpTy A -> T ⊥
+interpIn h     = proj₂ ； coelem
+interpIn (t i) = proj₁ ； interpIn i
+
+interpArr : Γ ⊢ A ->> B -> interpCtx Γ -> interpTy A -> T (interpTy B)
+interpArr (covar i) = interpIn i
+interpArr id = const idk
+interpArr bang = const absurd
+interpArr (e1 ∘ e2) = < interpArr e1 , interpArr e2 > ； uncurry T.composek
+interpArr (pass* e) = curry (distl ； S.[ uncurry (interpArr e) ； T.map absurd , proj₂ ； T.eta ])
+interpArr (ζ* e) = curry (interpArr e) ； flip ； uncurry ； councurry
+
+interpWk : Wk Γ Δ -> interpCtx Γ -> interpCtx Δ
+interpWk wk-ε        = const tt
+interpWk (wk-cong π) = pmap (interpWk π) idf
+interpWk (wk-wk π)   = proj₁ ； interpWk π
+
+interpWk-id-coh : interpWk (wk-id {Γ}) ≡ idf
+interpWk-id-coh {Γ = ε} = refl
+interpWk-id-coh {Γ = Γ ∙ A} rewrite interpWk-id-coh {Γ} = refl
+{-# REWRITE interpWk-id-coh #-}
+
+interpSub : Sub Γ Δ -> interpCtx Γ -> interpCtx Δ
+interpSub sub-ε        = const tt
+interpSub (sub-ex θ e) = < interpSub θ , interpArr e ； curry (eval ； (_$ absurd)) >
+
+interpSub-mem-arr-coh : (θ : Sub Γ Δ) (i : A ∈ Δ) -> interpArr (sub-mem θ i) ≡ interpSub θ ； interpIn i
+interpSub-mem-arr-coh (sub-ex θ e) h =
+  funext \γ -> funext \k -> funext \f -> cong (interpArr e γ k) (absurd-eta f ⊥-elim)
+interpSub-mem-arr-coh (sub-ex θ e) (t i) = interpSub-mem-arr-coh θ i
+
+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
+
+interpArr-wk-coh : (π : Wk Γ Δ) (e : Δ ⊢ A ->> B) -> interpArr (wk-arr π e) ≡ interpWk π ； interpArr e
+interpArr-wk-coh π (covar i) = interpWk-mem-coh π i
+interpArr-wk-coh π id = refl
+interpArr-wk-coh π bang = refl
+interpArr-wk-coh π (e1 ∘ e2) rewrite interpArr-wk-coh π e1 | interpArr-wk-coh π e2 = refl
+interpArr-wk-coh π (pass* e) rewrite interpArr-wk-coh π e =
+  funext \γ -> funext \{ (inj₁ c) -> refl ; (inj₂ b) -> refl }
+interpArr-wk-coh π (ζ* e) rewrite interpArr-wk-coh (wk-cong π) e = refl
+{-# REWRITE interpArr-wk-coh #-}
+
+interpSub-wk-coh : (π : Wk Γ Δ) (θ : Sub Δ Ψ) -> interpSub (sub-wk π θ) ≡ interpWk π ； interpSub θ
+interpSub-wk-coh π sub-ε = refl
+interpSub-wk-coh π (sub-ex θ e) rewrite interpSub-wk-coh π θ | interpArr-wk-coh π e = refl
+{-# REWRITE interpSub-wk-coh #-}
+
+interpSub-id-coh : interpSub (sub-id {Γ}) ≡ idf
+interpSub-id-coh {Γ = ε} = refl
+interpSub-id-coh {Γ = Γ ∙ A} = funext \p -> cong (_, p .proj₂) (happly interpSub-id-coh (p .proj₁))
+{-# REWRITE interpSub-id-coh #-}
+
+interpSub-arr-coh : (θ : Sub Γ Δ) (e : Δ ⊢ A ->> B) -> interpArr (sub-arr θ e) ≡ interpSub θ ； interpArr e
+interpSub-arr-coh θ (covar i) = interpSub-mem-arr-coh θ i
+interpSub-arr-coh θ id = refl
+interpSub-arr-coh θ bang = refl
+interpSub-arr-coh θ (e1 ∘ e2) rewrite interpSub-arr-coh θ e1 | interpSub-arr-coh θ e2 = refl
+interpSub-arr-coh θ (pass* e) rewrite interpSub-arr-coh θ e =
+  funext \γ -> funext \{ (inj₁ c) -> refl ; (inj₂ b) -> refl }
+interpSub-arr-coh θ (ζ* e) rewrite interpSub-arr-coh (sub-ex (sub-wk (wk-wk wk-id) θ) (covar h)) e = refl
+
+interpEq : Γ ⊢ e1 ≈ e2 ∶ A ->> B -> interpArr e1 ≡ interpArr e2
+interpEq (unitl _) = refl
+interpEq (unitr _) = refl
+interpEq (assoc _ _ _) = refl
+interpEq (term f g) = funext \γ -> absurd-eta (interpArr f γ) (interpArr g γ)
+interpEq (ζ*-beta f c) rewrite interpSub-arr-coh (sub-ex sub-id c) f =
+  funext \γ -> funext \a -> funext \k -> cong (\h -> interpArr f (γ , h) a k) $
+    funext \z -> cong (interpArr c γ z) (absurd-eta (⊥-elim ； k) ⊥-elim)
+interpEq (ζ*-eta f) =
+  funext \γ -> funext \a -> funext \k -> cong (interpArr f γ a) $
+    funext \{ (inj₁ c) -> refl ; (inj₂ b) -> refl }
+
\ No newline at end of file diff --git a/Coexp.ZetaStar.Syntax.html b/Coexp.ZetaStar.Syntax.html index 57d6be0..141d0dc 100644 --- a/Coexp.ZetaStar.Syntax.html +++ b/Coexp.ZetaStar.Syntax.html @@ -5,91 +5,92 @@ open import Coexp.Meta.Prelude open import Data.Nat -infix 50 _* -infixr 40 _`+_ -infixr 20 _∘_ +infixr 40 _`+_ +infixr 20 _∘_ -data Ty : Set where - `1 : Ty - _* : Ty -> Ty - _`+_ : Ty -> Ty -> Ty +data Ty : Set where + `0 : Ty + _`+_ : Ty -> Ty -> Ty -open Ctx Ty +open Ctx Ty public -syntax Arr Γ A B = Γ ⊢ A ->> B +syntax Arr Γ A B = Γ ⊢ A ->> B -data Arr : Ctx -> Ty -> Ty -> Set where +data Arr : Ctx -> Ty -> Ty -> Set where - var : (i : A ∈ Γ) - --------- - -> Γ ⊢ `1 ->> A + covar : (i : A ∈ Γ) + --------- + -> Γ ⊢ A ->> `0 - id : - --------- - Γ ⊢ A ->> A + id : + --------- + Γ ⊢ A ->> A - bang : - ---------- - Γ ⊢ A ->> `1 + bang : + ---------- + Γ ⊢ `0 ->> A - _∘_ : Γ ⊢ B ->> C -> Γ ⊢ A ->> B - ------------------------------ - -> Γ ⊢ A ->> C + _∘_ : Γ ⊢ B ->> C -> Γ ⊢ A ->> B + ------------------------------ + -> Γ ⊢ A ->> C - pass* : Γ ⊢ `1 ->> C * - ---------------------- - -> Γ ⊢ (C `+ B) ->> B + pass* : Γ ⊢ C ->> `0 + ---------------------- + -> Γ ⊢ (C `+ B) ->> B - ζ* : (Γ ∙ C *) ⊢ A ->> B - ----------------------- - -> Γ ⊢ A ->> (C `+ B) + ζ* : (Γ ∙ C) ⊢ A ->> B + ----------------------- + -> Γ ⊢ A ->> (C `+ B) -wk-arr : Wk Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B -wk-arr π (var i) = var (wk-mem π i) -wk-arr π id = id -wk-arr π bang = bang -wk-arr π (e1 ∘ e2) = wk-arr π e1 ∘ wk-arr π e2 -wk-arr π (pass* e) = pass* (wk-arr π e) -wk-arr π (ζ* e) = ζ* (wk-arr (wk-cong π) e) +wk-arr : Wk Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B +wk-arr π (covar i) = covar (wk-mem π i) +wk-arr π id = id +wk-arr π bang = bang +wk-arr π (e1 ∘ e2) = wk-arr π e1 ∘ wk-arr π e2 +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 public +open SubCoVar `0 covar public -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 : Sub Γ Δ -> Δ ⊢ A ->> B -> Γ ⊢ A ->> B +sub-arr θ (covar 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) θ) (covar h)) e) -open SubArr sub-arr +open SubArr sub-arr -syntax Eq Γ A B e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A ->> B +variable + e e1 e2 e3 e4 : Γ ⊢ A ->> B -data Eq (Γ : Ctx) : (A B : Ty) -> Γ ⊢ A ->> B -> Γ ⊢ A ->> B -> Set where +syntax Eq Γ A B e1 e2 = Γ ⊢ e1 ≈ e2 ∶ A ->> B - unitl : (f : Γ ⊢ A ->> B) - -------------- - -> Γ ⊢ f ≈ id ∘ f ∶ A ->> B +data Eq (Γ : Ctx) : (A B : Ty) -> Γ ⊢ A ->> B -> Γ ⊢ A ->> B -> Set where - unitr : (f : Γ ⊢ A ->> B) - -------------- - -> Γ ⊢ f ∘ id ≈ f ∶ A ->> B + unitl : (f : Γ ⊢ A ->> B) + -------------- + -> Γ ⊢ f ≈ id ∘ f ∶ A ->> B - assoc : (f : Γ ⊢ A ->> B) (g : Γ ⊢ B ->> C) (h : Γ ⊢ C ->> D) - --------------------------------------------------------- - -> Γ ⊢ (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) ∶ A ->> D + unitr : (f : Γ ⊢ A ->> B) + -------------- + -> Γ ⊢ f ∘ id ≈ f ∶ A ->> B - term : (f g : Γ ⊢ A ->> `1) - ------------------------- - -> Γ ⊢ f ≈ g ∶ A ->> `1 + assoc : (f : Γ ⊢ A ->> B) (g : Γ ⊢ B ->> C) (h : Γ ⊢ C ->> D) + --------------------------------------------------------- + -> Γ ⊢ (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) ∶ A ->> D - ζ*-beta : (f : (Γ ∙ C *) ⊢ A ->> B) (c : Γ ⊢ `1 ->> C *) - ------------------------------------------------ - -> Γ ⊢ pass* {B = B} c ∘ ζ* {C = C} f ≈ sub c f ∶ A ->> B + term : (f g : Γ ⊢ `0 ->> A) + ------------------------- + -> Γ ⊢ f ≈ g ∶ `0 ->> A - ζ*-eta : (f : Γ ⊢ A ->> (C `+ B)) - ------------------------------------ - -> Γ ⊢ ζ* {C = C} (pass* {B = B} (var h) ∘ wk f) ≈ f ∶ A ->> (C `+ B) + ζ*-beta : (f : (Γ ∙ C) ⊢ A ->> B) (c : Γ ⊢ C ->> `0) + ------------------------------------------------ + -> Γ ⊢ pass* {B = B} c ∘ ζ* {C = C} f ≈ sub c f ∶ A ->> B + + ζ*-eta : (f : Γ ⊢ A ->> (C `+ B)) + ------------------------------------ + -> Γ ⊢ ζ* {C = C} (pass* {B = B} (covar h) ∘ wk f) ≈ f ∶ A ->> (C `+ B) \ No newline at end of file diff --git a/index.html b/index.html index 594bad0..9472441 100644 --- a/index.html +++ b/index.html @@ -6,13 +6,17 @@ -- An exhaustive list of all modules: import Coexp.Everything -import Coexp.Kappa.Syntax -import Coexp.KappaStar.Syntax -import Coexp.LamLamBar.Interp -import Coexp.LamLamBar.Syntax -import Coexp.Meta.Prelude -import Coexp.Prelude -import Coexp.Semantics -import Coexp.Zeta.Syntax -import Coexp.ZetaStar.Syntax +import Coexp.Kappa.Interp +import Coexp.Kappa.Syntax +import Coexp.KappaStar.Interp +import Coexp.KappaStar.Syntax +import Coexp.LamLamBar.Interp +import Coexp.LamLamBar.Syntax +import Coexp.Meta.Prelude +import Coexp.Prelude +import Coexp.Semantics +import Coexp.Zeta.Interp +import Coexp.Zeta.Syntax +import Coexp.ZetaStar.Interp +import Coexp.ZetaStar.Syntax \ No newline at end of file