well-typed-syntax?.agda

module well-typed-syntax where
open import Data.Nat
infixl 2 _▻_
infixl 2 _▻Type_
infixl 3 _‘’_

mutual
  data Context : ℕ → Set where
    ε₀ : Context 0
    _▻_ : ∀ {n} (Γ : Context n) → Type Γ → Context (suc n)

  data Type : ∀ {n} → Context n → Set where
    _‘’_ : ∀ {n} {Γ : Context n} {A} → Type (Γ ▻ A) → Term {Γ = Γ} A → Type Γ
    W : ∀ {n} {Γ : Context n} {A} → Type Γ → Type (Γ ▻ A)
    W₁ : ∀ {n} {Γ : Context n} {A B} → Type (Γ ▻ A) → Type (Γ ▻ B ▻ W A)
    ‘Π’ : ∀ {n} {Γ : Context n} A → Type (Γ ▻ A) → Type Γ
    ‘Σ’ : ∀ {n} {Γ : Context n} T → Type (Γ ▻ T) → Type Γ
    ‘Context’ : Type ε₀
    ‘Type’ : Type (ε₀ ▻ ‘Context’)

  data Term : ∀ {n} {Γ : Context n} → Type Γ → Set where -- definitely missing some constructors, but haven't figured out which are semantic and which are structural
    _‘’_  : ∀ {n} {Γ : Context n} {A B} → Term (‘Π’ A B) → (a : Term {Γ = Γ} A) → Term (B ‘’ a)

    w : ∀ {n} {Γ : Context n} {A B : Type Γ} → Term B → Term (W {A = A} B)
    ‘λ∙’ : ∀ {n} {Γ : Context n} {A B} → Term B → Term {Γ = Γ} (‘Π’ A B)


  _▻Type_ : ∀ {n m} → Context n → Context m → Context (m + n)
  Γ ▻Type ε₀ = Γ
  Γ ▻Type (Γ' ▻ x) = Γ ▻Type Γ' ▻ weakenty Γ Γ' x

  weakenty : ∀ {n m} (Γ : Context n) (Γ' : Context m) → Type Γ' → Type (Γ ▻Type Γ')
  weakenty Γ Γ' (t₁ ‘’ x) = weakenty _ _ t₁ ‘’ weakentm _ _ x
  weakenty Γ ._ (W t₁) = W (weakenty _ _ t₁)
  weakenty Γ ._ (W₁ t₂) = W₁ (weakenty _ _ t₂)
  weakenty Γ Γ' (‘Π’ t b) = ‘Π’ (weakenty _ _ t) (weakenty _ _ b)
  weakenty Γ Γ' (‘Σ’ t b) = ‘Σ’ (weakenty _ _ t) (weakenty _ _ b)
  weakenty ε₀ .ε₀ ‘Context’ = ‘Context’
  weakenty (Γ ▻ x) .ε₀ ‘Context’ = W (weakenty _ _ ‘Context’)
  weakenty ε₀ .(ε₀ ▻ ‘Context’) ‘Type’ = ‘Type’
  weakenty (Γ ▻ x) .(ε₀ ▻ ‘Context’) ‘Type’ = W₁ (weakenty Γ (ε₀ ▻ ‘Context’) ‘Type’)

  weakentm : ∀ {n m} (Γ : Context n) {Γ' : Context m} (t : Type Γ') → Term t → Term (weakenty Γ Γ' t)
  weakentm Γ ._ (f ‘’ x) = weakentm _ _ f ‘’ weakentm _ _ x
  weakentm Γ ._ (w tm) = w (weakentm _ _ tm)
  weakentm Γ ._ (‘λ∙’ tm) = ‘λ∙’ (weakentm _ _ tm)