Mwe.agda

module Mwe where

open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)

data Type : Set where
  ⊤ : Type
  _⇒_ : Type → Type → Type
infix 30 _⇒_

data Context : Set where
  ∅ : Context
  _,_ : Context → Type → Context


data _∋_ : Context → Type → Set where
  Z : ∀ {Γ A}
   → (Γ , A) ∋ A

  S_ : ∀ {Γ A B}
    → Γ ∋ A
    → (Γ , B) ∋ A

data Term : Context → Set where
  var : ∀ {Γ A} → Γ ∋ A → Term Γ
  ƛ : ∀ {Γ A} → Term (Γ , A) → Term Γ
  _$_ : ∀ {Γ} → Term Γ → Term Γ → Term Γ


Rename : Context → Context → Set
Rename Γ Δ = ∀ {A} → Γ ∋ A → Δ ∋ A

Subst : Context → Context → Set
Subst Γ Δ = ∀ {A} → Γ ∋ A → Term Δ

ext : ∀ {Γ Δ} → Rename Γ Δ
  → (∀ {B} → Rename (Γ , B) (Δ , B))
ext ρ Z = Z
ext ρ (S x) = S ρ x

rename : ∀ {Γ Δ}
  → Rename Γ Δ
  → (Term Γ → Term Δ)
rename ρ (var x) = var (ρ x)
rename ρ (ƛ t) = ƛ (rename (ext ρ) t)
rename ρ (t₁ $ t₂) = rename ρ t₁ $ rename ρ t₂

exts : ∀ {Γ Δ} → Subst Γ Δ
  → (∀ {B} → Subst (Γ , B) (Δ , B))
exts σ Z = var Z
exts σ (S x) = rename S_ (σ x)

subst : ∀ {Γ Δ} → Subst Γ Δ →
                  (Term Γ → Term Δ)
subst σ (var x) = σ x
subst σ (ƛ t) = ƛ (subst (exts σ) t)
subst σ (t₁ $ t₂) = subst σ t₁ $ subst σ t₂


commute-subst-rename : ∀ {Γ Δ} {M : Term Γ} {σ : Subst Γ Δ}
                         {ρ : ∀ {Γ A} → Rename Γ (Γ , A)}
     → (∀ {A C} {x : Γ ∋ C} → exts σ {B = A} (ρ {Γ} {A} x) ≡ rename (ρ {Γ = Δ}) (σ x))
     → ∀ {A} → subst (exts σ {B = A}) (rename ρ M) ≡ rename ρ (subst σ M)
commute-subst-rename {M = var x} = {!!}
commute-subst-rename {M = ƛ {A = A} M} H = cong ƛ {!!}
commute-subst-rename {M = M $ M₁} = {!!}