{-# OPTIONS --rewriting #-} module A201801.StdLPTT where open import A201801.Prelude open import A201801.Category open import A201801.Fin open import A201801.FinLemmas open import A201801.Vec open import A201801.VecLemmas open import A201801.S4TTTerms open import A201801.S4TTTermsLemmas -------------------------------------------------------------------------------- -- TODO: unfinished -- infixr 8 _⊃_ -- data Form : Nat → Set -- where -- BASE : ∀ {d} → Form d -- _⊃_ : ∀ {d} → Form d → Form d → Form d -- [_]_ : ∀ {d} → Term₁ d → Form d → Form d -- -------------------------------------------------------------------------------- -- MRENₚ : ∀ {d d′} → d′ ≥ d → Form d -- → Form d′ -- MRENₚ e BASE = BASE -- MRENₚ e (A ⊃ B) = MRENₚ e A ⊃ MRENₚ e B -- MRENₚ e ([ M ] A) = [ MREN e M ] MRENₚ e A -- MWKₚ : ∀ {d} → Form d -- → Form (suc d) -- MWKₚ A = MRENₚ (drop id≥) A -- MSUBₚ : ∀ {d n} → Terms₁ d n → Form n -- → Form d -- MSUBₚ x BASE = BASE -- MSUBₚ x (A ⊃ B) = MSUBₚ x A ⊃ MSUBₚ x B -- MSUBₚ x ([ M ] A) = [ MSUB x M ] MSUBₚ x A -- MCUTₚ : ∀ {d} → Term₁ d → Form (suc d) -- → Form d -- MCUTₚ M A = MSUBₚ (MIDS₁ , M) A -- -------------------------------------------------------------------------------- -- id-MRENₚ : ∀ {d} → (A : Form d) -- → MRENₚ id≥ A ≡ A -- id-MRENₚ BASE = refl -- id-MRENₚ (A ⊃ B) = _⊃_ & id-MRENₚ A ⊗ id-MRENₚ B -- id-MRENₚ ([ M ] A) = [_]_ & id-MREN M ⊗ id-MRENₚ A -- comp-MRENₚ : ∀ {d d′ d″} → (e₁ : d′ ≥ d) (e₂ : d″ ≥ d′) (A : Form d) -- → MRENₚ (e₁ ∘≥ e₂) A ≡ MRENₚ e₂ (MRENₚ e₁ A) -- comp-MRENₚ e₁ e₂ BASE = refl -- comp-MRENₚ e₁ e₂ (A ⊃ B) = _⊃_ & comp-MRENₚ e₁ e₂ A ⊗ comp-MRENₚ e₁ e₂ B -- comp-MRENₚ e₁ e₂ ([ M ] A) = [_]_ & comp-MREN e₁ e₂ M ⊗ comp-MRENₚ e₁ e₂ A -- -------------------------------------------------------------------------------- -- infix 7 _true -- record Truth (d : Nat) : Set -- where -- constructor _true -- field -- A : Form d -- -------------------------------------------------------------------------------- -- MRENₜ : ∀ {d d′} → d′ ≥ d → Truth d -- → Truth d′ -- MRENₜ e (A true) = MRENₚ e A true -- MWKₜ : ∀ {d} → Truth d -- → Truth (suc d) -- MWKₜ (A true) = MWKₚ A true -- MSUBₜ : ∀ {d n} → Terms₁ d n → Truth n -- → Truth d -- MSUBₜ x (A true) = MSUBₚ x A true -- MCUTₜ : ∀ {d} → Term₁ d → Truth (suc d) -- → Truth d -- MCUTₜ M (A true) = MCUTₚ M A true -- -------------------------------------------------------------------------------- -- id-MRENₜ : ∀ {d} → (Aₜ : Truth d) -- → MRENₜ id≥ Aₜ ≡ Aₜ -- id-MRENₜ (A true) = _true & id-MRENₚ A -- comp-MRENₜ : ∀ {d d′ d″} → (e₁ : d′ ≥ d) (e₂ : d″ ≥ d′) (Aₜ : Truth d) -- → MRENₜ (e₁ ∘≥ e₂) Aₜ ≡ MRENₜ e₂ (MRENₜ e₁ Aₜ) -- comp-MRENₜ e₁ e₂ (A true) = _true & comp-MRENₚ e₁ e₂ A -- -------------------------------------------------------------------------------- -- Truths : Nat → Nat → Set -- Truths d g = Vec (Truth d) g -- -------------------------------------------------------------------------------- -- MRENSₜ : ∀ {d d′ g} → d′ ≥ d → Truths d g -- → Truths d′ g -- MRENSₜ e Γ = MAPS (MRENₜ e) Γ -- MWKSₜ : ∀ {d g} → Truths d g -- → Truths (suc d) g -- MWKSₜ Γ = MAPS MWKₜ Γ -- -------------------------------------------------------------------------------- -- id-MRENSₜ : ∀ {d g} → (Γ : Truths d g) -- → MRENSₜ id≥ Γ ≡ Γ -- id-MRENSₜ ∙ = refl -- id-MRENSₜ (Γ , Aₜ) = _,_ & id-MRENSₜ Γ ⊗ id-MRENₜ Aₜ -- comp-MRENSₜ : ∀ {d d′ d″ g} → (e₁ : d′ ≥ d) (e₂ : d″ ≥ d′) (Γ : Truths d g) -- → MRENSₜ (e₁ ∘≥ e₂) Γ ≡ MRENSₜ e₂ (MRENSₜ e₁ Γ) -- comp-MRENSₜ e₁ e₂ ∙ = refl -- comp-MRENSₜ e₁ e₂ (Γ , Aₜ) = _,_ & comp-MRENSₜ e₁ e₂ Γ ⊗ comp-MRENₜ e₁ e₂ Aₜ -- resp-MRENSₜ-⊇ : ∀ {d d′ g g′ e₂} → {Γ : Truths d g} {Γ′ : Truths d g′} -- → (e₁ : d′ ≥ d) → Γ′ ⊇⟨ e₂ ⟩ Γ -- → MRENSₜ e₁ Γ′ ⊇⟨ e₂ ⟩ MRENSₜ e₁ Γ -- resp-MRENSₜ-⊇ e₁ done = done -- resp-MRENSₜ-⊇ e₁ (drop η) = resp-MRENSₜ-⊇ e₁ η ∘⊇ drop id⊇ -- resp-MRENSₜ-⊇ e₁ (keep η) = keep (resp-MRENSₜ-⊇ e₁ η) -- resp-MWKSₜ-⊇ : ∀ {d g g′ e} → {Γ : Truths d g} {Γ′ : Truths d g′} -- → Γ′ ⊇⟨ e ⟩ Γ -- → MWKSₜ Γ′ ⊇⟨ e ⟩ MWKSₜ Γ -- resp-MWKSₜ-⊇ η = resp-MRENSₜ-⊇ (drop id≥) η -- resp-MRENSₜ-∋ : ∀ {d d′ g i} → {Γ : Truths d g} {A : Form d} -- → (e : d′ ≥ d) → Γ ∋⟨ i ⟩ A true -- → MRENSₜ e Γ ∋⟨ i ⟩ MRENₚ e A true -- resp-MRENSₜ-∋ e zero = zero -- resp-MRENSₜ-∋ e (suc 𝒾) = suc (resp-MRENSₜ-∋ e 𝒾) -- resp-MWKSₜ-∋ : ∀ {d g i} → {Γ : Truths d g} {A : Form d} -- → Γ ∋⟨ i ⟩ A true -- → MWKSₜ Γ ∋⟨ i ⟩ MWKₚ A true -- resp-MWKSₜ-∋ 𝒾 = resp-MRENSₜ-∋ (drop id≥) 𝒾 -- -------------------------------------------------------------------------------- -- infix 7 _valid -- record Validity (d : Nat) : Set -- where -- constructor _valid -- field -- A : Form d -- -------------------------------------------------------------------------------- -- MRENᵥ : ∀ {d d′} → d′ ≥ d → Validity d -- → Validity d′ -- MRENᵥ e (A valid) = MRENₚ e A valid -- MWKᵥ : ∀ {d} → Validity d -- → Validity (suc d) -- MWKᵥ (A valid) = MWKₚ A valid -- MSUBᵥ : ∀ {d n} → Terms₁ d n → Validity n -- → Validity d -- MSUBᵥ x (A valid) = MSUBₚ x A valid -- MCUTᵥ : ∀ {d} → Term₁ d → Validity (suc d) -- → Validity d -- MCUTᵥ M (A valid) = MCUTₚ M A valid -- -------------------------------------------------------------------------------- -- id-MRENᵥ : ∀ {d} → (Aᵥ : Validity d) -- → MRENᵥ id≥ Aᵥ ≡ Aᵥ -- id-MRENᵥ (A valid) = _valid & id-MRENₚ A -- comp-MRENᵥ : ∀ {d d′ d″} → (e₁ : d′ ≥ d) (e₂ : d″ ≥ d′) (Aᵥ : Validity d) -- → MRENᵥ (e₁ ∘≥ e₂) Aᵥ ≡ MRENᵥ e₂ (MRENᵥ e₁ Aᵥ) -- comp-MRENᵥ e₁ e₂ (A valid) = _valid & comp-MRENₚ e₁ e₂ A -- -------------------------------------------------------------------------------- -- data Validities : Nat → Set -- where -- ∙ : Validities zero -- _,_ : ∀ {d} → Validities d → Validity d -- → Validities (suc d) -- -------------------------------------------------------------------------------- -- infix 4 _⊇⟪_⟫_ -- data _⊇⟪_⟫_ : ∀ {d d′} → Validities d′ → d′ ≥ d → Validities d → Set -- where -- done : ∙ ⊇⟪ done ⟫ ∙ -- drop : ∀ {d d′ e} → {Δ : Validities d} {Δ′ : Validities d′} {Aᵥ : Validity d′} -- → Δ′ ⊇⟪ e ⟫ Δ -- → Δ′ , Aᵥ ⊇⟪ drop e ⟫ Δ -- keep : ∀ {d d′ e} → {Δ : Validities d} {Δ′ : Validities d′} {Aᵥ : Validity d} -- {Aᵥ° : Validity d′} {{_ : MRENᵥ e Aᵥ ≡ Aᵥ°}} -- → Δ′ ⊇⟪ e ⟫ Δ -- → Δ′ , Aᵥ° ⊇⟪ keep e ⟫ Δ , Aᵥ -- id⊇◈ : ∀ {d} → {Δ : Validities d} -- → Δ ⊇⟪ id≥ ⟫ Δ -- id⊇◈ {Δ = ∙} = done -- id⊇◈ {Δ = Δ , Aᵥ} = keep {{id-MRENᵥ Aᵥ}} id⊇◈ -- _∘⊇◈_ : ∀ {d d′ d″ e₁ e₂} → {Δ : Validities d} {Δ′ : Validities d′} {Δ″ : Validities d″} -- → Δ′ ⊇⟪ e₁ ⟫ Δ → Δ″ ⊇⟪ e₂ ⟫ Δ′ -- → Δ″ ⊇⟪ e₁ ∘≥ e₂ ⟫ Δ -- η₁ ∘⊇◈ done = η₁ -- η₁ ∘⊇◈ drop η₂ = drop (η₁ ∘⊇◈ η₂) -- drop η₁ ∘⊇◈ keep η₂ = drop (η₁ ∘⊇◈ η₂) -- keep {e = e₁} {Aᵥ = Aᵥ} {{refl}} η₁ ∘⊇◈ keep {e = e₂} {{refl}} η₂ -- = keep {{comp-MRENᵥ e₁ e₂ Aᵥ}} (η₁ ∘⊇◈ η₂) -- -------------------------------------------------------------------------------- -- infix 4 _∋⟪_⟫_ -- data _∋⟪_⟫_ : ∀ {d} → Validities d → Fin d → Validity d → Set -- where -- zero : ∀ {d} → {Δ : Validities d} {Aᵥ : Validity d} -- {Aᵥ° : Validity (suc d)} {{_ : MWKᵥ Aᵥ ≡ Aᵥ°}} -- → Δ , Aᵥ ∋⟪ zero ⟫ Aᵥ° -- suc : ∀ {d i} → {Δ : Validities d} {Aᵥ : Validity d} {Bᵥ : Validity d} -- {Aᵥ° : Validity (suc d)} {{_ : MWKᵥ Aᵥ ≡ Aᵥ°}} -- → Δ ∋⟪ i ⟫ Aᵥ -- → Δ , Bᵥ ∋⟪ suc i ⟫ Aᵥ° -- ren∋◈ : ∀ {d d′ e i} → {Δ : Validities d} {Δ′ : Validities d′} {Aᵥ : Validity d} -- → Δ′ ⊇⟪ e ⟫ Δ → Δ ∋⟪ i ⟫ Aᵥ -- → Δ′ ∋⟪ REN∋ e i ⟫ MRENᵥ e Aᵥ -- ren∋◈ {i = i} {Aᵥ = Aᵥ} done 𝒾 = coerce 𝒾 ((\ Aᵥ′ → ∙ ∋⟪ i ⟫ Aᵥ′) & id-MRENᵥ Aᵥ ⁻¹) -- ren∋◈ {Aᵥ = Aᵥ} (drop {e = e} η) 𝒾 = suc {{comp-MRENᵥ e (drop id≥) Aᵥ ⁻¹}} (ren∋◈ η 𝒾) -- ren∋◈ (keep {e = e} {Aᵥ = Aᵥ} {{refl}} η) (zero {{refl}}) -- = zero {{ comp-MRENᵥ e (drop id≥) Aᵥ ⁻¹ -- ⋮ comp-MRENᵥ (drop id≥) (keep e) Aᵥ -- }} -- ren∋◈ (keep {e = e} {{refl}} η) (suc {Aᵥ = Aᵥ} {{refl}} 𝒾) -- = suc {{ comp-MRENᵥ e (drop id≥) Aᵥ ⁻¹ -- ⋮ comp-MRENᵥ (drop id≥) (keep e) Aᵥ -- }} (ren∋◈ η 𝒾) -- -------------------------------------------------------------------------------- -- infix 4 _⊢_⦂_ -- record Derivation (d : Nat) : Set -- where -- constructor _⊢_⦂_ -- field -- {g} : Nat -- Γ : Truths d g -- M : Term d g -- Aₜ : Truth d -- infix 3 _⨾_ -- data _⨾_ : ∀ {d} → Validities d → Derivation d → Set -- where -- var : ∀ {d g i} → {Δ : Validities d} {Γ : Truths d g} -- {A : Form d} -- → Γ ∋⟨ i ⟩ A true -- → Δ ⨾ Γ ⊢ VAR i ⦂ A true -- lam : ∀ {d g M} → {Δ : Validities d} {Γ : Truths d g} -- {A B : Form d} -- → Δ ⨾ Γ , A true ⊢ M ⦂ B true -- → Δ ⨾ Γ ⊢ LAM M ⦂ A ⊃ B true -- app : ∀ {d g M N} → {Δ : Validities d} {Γ : Truths d g} -- {A B : Form d} -- → Δ ⨾ Γ ⊢ M ⦂ A ⊃ B true → Δ ⨾ Γ ⊢ N ⦂ A true -- → Δ ⨾ Γ ⊢ APP M N ⦂ B true -- mvar : ∀ {d g i} → {Δ : Validities d} {Γ : Truths d g} -- {A : Form d} -- → Δ ∋⟪ i ⟫ A valid -- → Δ ⨾ Γ ⊢ MVAR i ⦂ A true -- box : ∀ {d g M} → {Δ : Validities d} {Γ : Truths d g} -- {A : Form d} -- → Δ ⨾ ∙ ⊢ M ⦂ A true -- → Δ ⨾ Γ ⊢ BOX M ⦂ [ M ] A true -- letbox : ∀ {d g M N O} → {Δ : Validities d} {Γ : Truths d g} -- {A : Form d} {B : Form (suc d)} -- {Γ° : Truths (suc d) g} {{_ : Γ° ≡ MWKSₜ Γ}} -- {B° : Form d} {{_ : B° ≡ MCUTₚ O B}} -- → Δ ⨾ Γ ⊢ M ⦂ [ O ] A true → Δ , A valid ⨾ Γ° ⊢ N ⦂ B true -- → Δ ⨾ Γ ⊢ LETBOX M N ⦂ B° true -- -------------------------------------------------------------------------------- -- ren : ∀ {d g g′ e M} → {Δ : Validities d} {Γ : Truths d g} {Γ′ : Truths d g′} -- {A : Form d} -- → Γ′ ⊇⟨ e ⟩ Γ → Δ ⨾ Γ ⊢ M ⦂ A true -- → Δ ⨾ Γ′ ⊢ REN e M ⦂ A true -- ren η (var 𝒾) = var (ren∋ η 𝒾) -- ren η (lam 𝒟) = lam (ren (keep η) 𝒟) -- ren η (app 𝒟 ℰ) = app (ren η 𝒟) (ren η ℰ) -- ren η (mvar 𝒾) = mvar 𝒾 -- ren η (box 𝒟) = box 𝒟 -- ren η (letbox {{refl}} {{refl}} 𝒟 ℰ) -- = letbox {{refl}} {{refl}} (ren η 𝒟) (ren (resp-MWKSₜ-⊇ η) ℰ) -- wk : ∀ {d g M} → {Δ : Validities d} {Γ : Truths d g} -- {A B : Form d} -- → Δ ⨾ Γ ⊢ M ⦂ A true -- → Δ ⨾ Γ , B true ⊢ WK M ⦂ A true -- wk 𝒟 = ren (drop id⊇) 𝒟 -- vz : ∀ {d g} → {Δ : Validities d} {Γ : Truths d g} -- {A : Form d} -- → Δ ⨾ Γ , A true ⊢ VZ ⦂ A true -- vz = var zero -- -------------------------------------------------------------------------------- -- comp-MWKₚ-MRENₚ-keep : ∀ {d d′} → (e : d′ ≥ d) (A : Form d) -- → (MRENₚ (keep e) ∘ MWKₚ) A ≡ (MWKₚ ∘ MRENₚ e) A -- comp-MWKₚ-MRENₚ-keep e A = comp-MRENₚ (drop id≥) (keep e) A ⁻¹ -- ⋮ (\ e′ → MRENₚ (drop e′) A) & (lid∘ e ⋮ rid∘ e ⁻¹) -- ⋮ comp-MRENₚ e (drop id≥) A -- comp-MWKSₜ-MRENSₜ-keep : ∀ {d d′ g} → (e : d′ ≥ d) (Γ : Truths d g) -- → (MRENSₜ (keep e) ∘ MWKSₜ) Γ ≡ (MWKSₜ ∘ MRENSₜ e) Γ -- comp-MWKSₜ-MRENSₜ-keep e ∙ = refl -- comp-MWKSₜ-MRENSₜ-keep e (Γ , A true) = _,_ & comp-MWKSₜ-MRENSₜ-keep e Γ -- ⊗ _true & comp-MWKₚ-MRENₚ-keep e A -- comp-MRENₚ-MSUBₚ : ∀ {d d′ n} → (e : d′ ≥ d) (x : Terms₁ d n) (A : Form n) -- → MSUBₚ (MRENS₁ e x) A ≡ (MRENₚ e ∘ MSUBₚ x) A -- comp-MRENₚ-MSUBₚ e x BASE = refl -- comp-MRENₚ-MSUBₚ e x (A ⊃ B) = _⊃_ & comp-MRENₚ-MSUBₚ e x A ⊗ comp-MRENₚ-MSUBₚ e x B -- comp-MRENₚ-MSUBₚ e x ([ M ] A) = [_]_ & comp-MREN-MSUB e x M ⊗ comp-MRENₚ-MSUBₚ e x A -- comp-MSUBₚ-MRENₚ : ∀ {d n n′} → (x : Terms₁ d n′) (e : n′ ≥ n) (A : Form n) -- → MSUBₚ (GETS x e) A ≡ (MSUBₚ x ∘ MRENₚ e) A -- comp-MSUBₚ-MRENₚ x e BASE = refl -- comp-MSUBₚ-MRENₚ x e (A ⊃ B) = _⊃_ & comp-MSUBₚ-MRENₚ x e A ⊗ comp-MSUBₚ-MRENₚ x e B -- comp-MSUBₚ-MRENₚ x e ([ M ] A) = [_]_ & comp-MSUB-MREN x e M ⊗ comp-MSUBₚ-MRENₚ x e A -- oops : ∀ {d d′} → (e : d′ ≥ d) -- → MRENS e MIDS₁ ≡ GETS MIDS₁ e -- oops done = refl -- oops (drop e) = comp-MRENS e (drop id≥) MIDS₁ -- ⋮ MWKS & oops e -- ⋮ comp-MRENS-GETS (drop id≥) MIDS₁ e ⁻¹ -- oops (keep e) = (_, MVZ) & ( comp-MWKS-MRENS-keep e MIDS₁ -- ⋮ MWKS & oops e -- ⋮ comp-MRENS-GETS (drop id≥) MIDS₁ e ⁻¹ -- ) -- mren : ∀ {d d′ g e M} → {Δ : Validities d} {Δ′ : Validities d′} {Γ : Truths d g} -- {A : Form d} -- → Δ′ ⊇⟪ e ⟫ Δ → Δ ⨾ Γ ⊢ M ⦂ A true -- → Δ′ ⨾ MRENSₜ e Γ ⊢ MREN e M ⦂ MRENₚ e A true -- mren η (var 𝒾) = var (resp-MRENSₜ-∋ _ 𝒾) -- mren η (lam 𝒟) = lam (mren η 𝒟) -- mren η (app 𝒟 ℰ) = app (mren η 𝒟) (mren η ℰ) -- mren η (mvar 𝒾) = mvar (ren∋◈ η 𝒾) -- mren η (box 𝒟) = box (mren η 𝒟) -- mren {e = e} η (letbox {O = O} {Γ = Γ} {A = A} {B} {{refl}} {{refl}} 𝒟 ℰ) -- = letbox -- {{comp-MWKSₜ-MRENSₜ-keep e Γ}} -- {{( comp-MRENₚ-MSUBₚ e (MIDS₁ , O) B ⁻¹ -- ⋮ (\ x′ → MSUBₚ (x′ , MREN e O) B) & oops e -- ⋮ comp-MSUBₚ-MRENₚ (MIDS₁ , MREN e O) (keep e) B -- )}} -- (mren η 𝒟) -- (mren (keep {{refl}} η) ℰ) -- mwk : ∀ {d g M} → {Δ : Validities d} {Γ : Truths d g} -- {A B : Form d} -- → Δ ⨾ Γ ⊢ M ⦂ A true -- → Δ , B valid ⨾ MWKSₜ Γ ⊢ MWK M ⦂ MWKₚ A true -- mwk 𝒟 = mren (drop id⊇◈) 𝒟 -- mvz : ∀ {d g} → {Δ : Validities d} {Γ : Truths d g} -- {A : Form d} -- → Δ , A valid ⨾ MWKSₜ Γ ⊢ MVZ ⦂ MWKₚ A true -- mvz = mvar zero -- --------------------------------------------------------------------------------