vflambda.agda

open import Data.List

mutual
  data Typ : Set₁ where
    ground : Set → Typ
    tyw : Typ → Subst → Typ

  data Subst : Set where
    id : Subst
    ↑ : Subst
    _∙_ : Term → Subst → Subst
    _∘_ : Subst → Subst → Subst

  data Term : Set where
    one : Term
    trw : Term → Subst → Term

Ctx : Set₁
Ctx = List Typ

mutual
  data jctx : Ctx → Set₁ where
    ctempty : jctx []
    ctcons : ∀{Γ σ} → jtype Γ σ → jctx (σ ∷ Γ)

  data jtype : Ctx → Typ → Set₁ where
    tysubst : ∀{Γ Γ' s σ} → jsubst Γ' s Γ → jtype Γ σ → jtype Γ' (tyw σ s)

  data jsubst : Ctx → Subst → Ctx → Set₁ where
    sbid : ∀{Γ} → jsubst Γ id Γ
    sbshift : ∀{Γ σ} → jsubst (σ ∷ Γ) ↑ Γ
    sbcomp : ∀{Γ₁ Γ₂ Γ₃ s₁ s₂} → jsubst Γ₁ s₁ Γ₂ → jsubst Γ₂ s₂ Γ₃ → jsubst Γ₁ (s₂ ∘ s₁) Γ₃
    sbapp : ∀{Γ Γ' s σ M'} → jsubst Γ' s Γ → jtype Γ σ → jterm Γ' M' (tyw σ s) → jsubst Γ' (M' ∙ s) (σ ∷ Γ)

  data jterm : Ctx → Term → Typ → Set₁ where
    trone : ∀{Γ σ} → jterm (σ ∷ Γ) one (tyw σ ↑)
    trsubst : ∀{Γ Γ' σ s M} → jsubst Γ' s Γ → jterm Γ M σ → jterm Γ' (trw M s) (tyw σ s)

  _⊢_/_ = jterm

data eqTyp : Typ → Typ → Set₁ where
  etycomp : ∀{σ s t} → eqTyp (tyw (tyw σ s) t) (tyw σ (s ∘ t))
  etyid : ∀{σ} → eqTyp (tyw σ id) σ

data eqSubst : Subst → Subst → Set₁ where
  esbshift : ∀{M s} → eqSubst (↑ ∘ (M ∙ s)) s
  esbassoc : ∀{s₁ s₂ s₃} → eqSubst ((s₁ ∘ s₂) ∘ s₃) (s₁ ∘ (s₂ ∘ s₃))
  esbidl : ∀{s} → eqSubst (id ∘ s) s
  esbidr : ∀{s} → eqSubst (s ∘ id) s
  esbapp : ∀{M s t} → eqSubst ((M ∙ s) ∘ t) ((trw M t) ∙ (s ∘ t))
  esbone : ∀{s} → eqSubst ((trw one s) ∙ (↑ ∘ s)) s

data eqTerm : Term → Term → Set₁ where
  etrone : ∀{M s} → eqTerm (trw one (M ∙ s)) M
  etrcomp : ∀{M s t} → eqTerm (trw (trw M s) t) (trw M (s ∘ t))