{-# OPTIONS --without-K --safe #-} module Minimal.TypedSem where open import Lib open import Minimal.Statics open Extensional public mutual Env : Set Env = ℕ → D data D : Set where tru : D fls : D Λ : (t : Exp) → (ρ : Env) → D ↑ : (T : Typ) → (e : Dn) → D data Dn : Set where l : (x : ℕ) → Dn _$_ : Dn → (d : Df) → Dn data Df : Set where ↓ : (T : Typ) → (a : D) → Df infixl 10 [_]_$′_ pattern l′ T x = ↑ T (l x) pattern [_]_$′_ T x y = ↑ T (_$_ x y) variable a a′ a″ : D b b′ b″ : D f f′ f″ : D e e′ e″ : Dn d d′ d″ d‴ : Df ρ ρ′ ρ″ : Env infixl 8 _↦_ _↦_ : Env → D → Env (ρ ↦ d) zero = d (ρ ↦ d) (suc x) = ρ x drop : Env → Env drop ρ n = ρ (suc n) infix 4 _∙_↘_ ⟦_⟧_↘_ ⟦_⟧s_↘_ mutual data _∙_↘_ : D → D → D → Set where Λ∙ : ⟦ t ⟧ ρ ↦ a ↘ b → ------------------ Λ t ρ ∙ a ↘ b $∙ : ∀ S T e a → ↑ (S ⟶ T) e ∙ a ↘ ↑ T (e $ ↓ S a) data ⟦_⟧_↘_ : Exp → Env → D → Set where ⟦v⟧ : ∀ n → ⟦ v n ⟧ ρ ↘ ρ n ⟦tru⟧ : ⟦ tru ⟧ ρ ↘ tru ⟦fls⟧ : ⟦ fls ⟧ ρ ↘ fls ⟦Λ⟧ : ∀ t → ⟦ Λ t ⟧ ρ ↘ Λ t ρ ⟦$⟧ : ⟦ r ⟧ ρ ↘ f → ⟦ s ⟧ ρ ↘ a → f ∙ a ↘ b → ------------------------ ⟦ r $ s ⟧ ρ ↘ b ⟦[]⟧ : ⟦ σ ⟧s ρ ↘ ρ′ → ⟦ t ⟧ ρ′ ↘ a → --------------------- ⟦ t [ σ ] ⟧ ρ ↘ a data ⟦_⟧s_↘_ : Subst → Env → Env → Set where ⟦↑⟧ : ⟦ ↑ ⟧s ρ ↘ drop ρ ⟦I⟧ : ⟦ I ⟧s ρ ↘ ρ ⟦∘⟧ : ⟦ τ ⟧s ρ ↘ ρ′ → ⟦ σ ⟧s ρ′ ↘ ρ″ → ----------------- ⟦ σ ∘ τ ⟧s ρ ↘ ρ″ ⟦,⟧ : ⟦ σ ⟧s ρ ↘ ρ′ → ⟦ t ⟧ ρ ↘ a → --------------------- ⟦ σ , t ⟧s ρ ↘ ρ′ ↦ a mutual ap-det : f ∙ a ↘ b → f ∙ a ↘ b′ → b ≡ b′ ap-det (Λ∙ ↘b) (Λ∙ ↘b′) = ⟦⟧-det ↘b ↘b′ ap-det ($∙ S T e _) ($∙ .S .T .e _) = refl ⟦⟧-det : ⟦ t ⟧ ρ ↘ a → ⟦ t ⟧ ρ ↘ b → a ≡ b ⟦⟧-det (⟦v⟧ n) (⟦v⟧ .n) = refl ⟦⟧-det ⟦tru⟧ ⟦tru⟧ = refl ⟦⟧-det ⟦fls⟧ ⟦fls⟧ = refl ⟦⟧-det (⟦Λ⟧ t) (⟦Λ⟧ .t) = refl ⟦⟧-det (⟦$⟧ ↘f ↘a ↘b) (⟦$⟧ ↘f′ ↘a′ ↘b′) rewrite ⟦⟧-det ↘f ↘f′ | ⟦⟧-det ↘a ↘a′ | ap-det ↘b ↘b′ = refl ⟦⟧-det (⟦[]⟧ ↘ρ′ ↘a) (⟦[]⟧ ↘ρ″ ↘b) rewrite ⟦⟧s-det ↘ρ′ ↘ρ″ | ⟦⟧-det ↘a ↘b = refl ⟦⟧s-det : ⟦ σ ⟧s ρ ↘ ρ′ → ⟦ σ ⟧s ρ ↘ ρ″ → ρ′ ≡ ρ″ ⟦⟧s-det ⟦↑⟧ ⟦↑⟧ = refl ⟦⟧s-det ⟦I⟧ ⟦I⟧ = refl ⟦⟧s-det (⟦∘⟧ ↘ρ′ ↘ρ″) (⟦∘⟧ ↘ρ‴ ↘ρ⁗) rewrite ⟦⟧s-det ↘ρ′ ↘ρ‴ | ⟦⟧s-det ↘ρ″ ↘ρ⁗ = refl ⟦⟧s-det (⟦,⟧ ↘ρ′ ↘a) (⟦,⟧ ↘ρ″ ↘b) rewrite ⟦⟧s-det ↘ρ′ ↘ρ″ | ⟦⟧-det ↘a ↘b = refl infix 4 Rf_-_↘_ Re_-_↘_ mutual data Rf_-_↘_ : ℕ → Df → Nf → Set where Rtru : ∀ n → Rf n - ↓ Bo tru ↘ tru Rfls : ∀ n → Rf n - ↓ Bo fls ↘ fls RΛ : ∀ n → f ∙ l′ S n ↘ a → Rf (suc n) - ↓ T a ↘ w → --------------------- Rf n - ↓ (S ⟶ T) f ↘ Λ w Rne : ∀ n → Re n - e ↘ u → --------------------- Rf n - ↓ Bo (↑ T e) ↘ ne u data Re_-_↘_ : ℕ → Dn → Ne → Set where Rl : ∀ n x → Re n - l x ↘ v (n ∸ x ∸ 1) R$ : ∀ n → Re n - e ↘ u → Rf n - d ↘ w → --------------------- Re n - e $ d ↘ u $ w mutual Rf-det : ∀ {n} → Rf n - d ↘ w → Rf n - d ↘ w′ → w ≡ w′ Rf-det (Rtru _) (Rtru _) = refl Rf-det (Rfls _) (Rfls _) = refl Rf-det (RΛ _ ↘a ↘w) (RΛ _ ↘a′ ↘w′) rewrite ap-det ↘a ↘a′ = cong Λ (Rf-det ↘w ↘w′) Rf-det (Rne _ ↘u) (Rne _ ↘u′) = cong ne (Re-det ↘u ↘u′) Re-det : ∀ {n} → Re n - e ↘ u → Re n - e ↘ u′ → u ≡ u′ Re-det (Rl _ x) (Rl _ .x) = refl Re-det (R$ _ ↘u ↘w) (R$ _ ↘u′ ↘w′) rewrite Re-det ↘u ↘u′ | Rf-det ↘w ↘w′ = refl record Nbe n ρ t T w : Set where field ⟦t⟧ : D ↘⟦t⟧ : ⟦ t ⟧ ρ ↘ ⟦t⟧ ↓⟦t⟧ : Rf n - ↓ T ⟦t⟧ ↘ w InitialEnv : Ctx → Env InitialEnv [] i = tru InitialEnv (T ∷ Γ) zero = l′ T (L.length Γ) InitialEnv (T ∷ Γ) (suc i) = InitialEnv Γ i