context-append.agda

data Context : ℕ → Set
data _+c_ {n : ℕ} (Γ : Context n) : ℕ → Set
data Type : ∀ {n} → Context n → Set
data Term : ∀ {n} (Γ : Context n) → Type Γ → Set

_++_ : ∀ {n m} (Γ : Context n) → Γ +c m → Context (m + n)
_cw_ : ∀ {x n m} {Γ : Context x} (Δ : Γ +c n) → Γ +c m → (Γ ++ Δ) +c m

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

data _+c_ {n : ℕ} (Γ : Context n) where
  ε₀ : Γ +c 0
  _▻c_ : ∀ {m} (Δ : Γ +c m) → Type (Γ ++ Δ) → Γ +c suc m

Γ ++ ε₀ = Γ
Γ ++ (Δ ▻c x) = Γ ++ Δ ▻ x

data Type  where
  Wₙ : ∀ {x n m} {Γ : Context x} {Δ₁ : Γ +c n} {Δ₂ : Γ +c m} (B : Type (Γ ++ Δ₂)) → Type (Γ ++ Δ₁ ++ Δ₁ cw Δ₂)
  _‘’_ : ∀ {n} {Γ : Context n} {A} (T : Type (Γ ▻ A)) (a : Term Γ A) → Type Γ -- do we need this one?
  ‘Σ’ : ∀ {n} {Γ : Context n} T → Type (Γ ▻ T) → Type Γ
  _‘→’_ : ∀ {n} {Γ : Context n} A → Type (Γ ▻ A) → Type Γ
  U : ∀ {n} {Γ : Context n} → Type Γ -- for now only one universe
  El : ∀ {n} {Γ : Context n} → Term Γ U → Type Γ

Δ₁ cw ε₀ = ε₀
Δ₁ cw (Δ₂ ▻c x) = (Δ₁ cw Δ₂) ▻c Wₙ {Δ₁ = Δ₁} {Δ₂ = Δ₂} x

data Term where
  wₙ : ∀ {x n m} {Γ : Context x} {Δ₁ : Γ +c n} {Δ₂ : Γ +c m} {B : Type (Γ ++ Δ₂)} → Term (Γ ++ Δ₂) B → Term (Γ ++ Δ₁ ++ Δ₁ cw Δ₂) (Wₙ {Δ₁ = Δ₁} {Δ₂ = Δ₂} B)
  wₙΣ : ∀ {x n m} {Γ : Context x} {Δ₁ : Γ +c n} {Δ₂ : Γ +c m} {A B} → Term (Γ ++ Δ₁ ++ Δ₁ cw Δ₂) (Wₙ {Δ₂ = Δ₂} (‘Σ’ A B)) → Term (Γ ++ Δ₁ ++ Δ₁ cw Δ₂) (‘Σ’ (Wₙ A) (Wₙ {Δ₂ = Δ₂ ▻c A} B))
  wₙΠ : ∀ {x n m} {Γ : Context x} {Δ₁ : Γ +c n} {Δ₂ : Γ +c m} {A B} → Term (Γ ++ Δ₁ ++ Δ₁ cw Δ₂) (Wₙ {Δ₂ = Δ₂} (A ‘→’ B)) → Term (Γ ++ Δ₁ ++ Δ₁ cw Δ₂) (Wₙ A ‘→’ Wₙ {Δ₂ = Δ₂ ▻c A} B)
  _‘’ₜ_ : ∀ {n} {Γ : Context n} {A B} → Term Γ (A ‘→’ B) → (a : Term Γ A) → Term Γ (B ‘’ a)
  ‘’₀ : ∀ {n} {Γ : Context n} {A B : Type Γ} {a : Term Γ A} → Term Γ (Wₙ {Δ₁ = ε₀ ▻c A} {ε₀} B ‘’ a) → Term Γ B
  _‘λ∙’_ : ∀ {n} {Γ : Context n} {A B} → Term (Γ ▻ A) B → Term Γ (A ‘→’ B)
  ‘Var₀’ : ∀ {n} {Γ : Context n} {T} → Term (Γ ▻ T) (Wₙ {Γ = Γ} {ε₀ ▻c T} {ε₀} T)
  ‘proj₁’ : ∀ {n} {Γ : Context n} {T P} → Term Γ (‘Σ’ T P ‘→’ Wₙ {Γ = Γ} {ε₀ ▻c ‘Σ’ T P} {ε₀} T)
  ‘proj₂’ : ∀ {n} {Γ : Context n} {T P} → Term Γ (‘Σ’ T P ‘→’ (Wₙ {Δ₁ = ε₀ ▻c ‘Σ’ T P} {Δ₂ = ε₀ ▻c T} P ‘’ ‘’₀ (‘proj₁’ ‘’ₜ wₙΣ ‘Var₀’)))
  ‘existsT’ : ∀ {n} {Γ : Context n} {T P} (x : Term Γ T) → Term Γ (P ‘’ x) → Term Γ (‘Σ’ T P)
  ty : ∀ {n} {Γ : Context n} → Type Γ → Term Γ U