swapping variables

swapVar.agda

module Subst1 where
open import Term

infixl 20 _-_
_-_ : {σ : Ty} → (Γ : Con) → Var Γ σ → Con
ε - ()
(Γ , σ) - vz = Γ
(Γ , τ) - vs x = (Γ - x) , τ


data _>_⇔_<_ {σ τ : Ty} : {Γ : Con} {Δ : Con} →
  (s : Var Γ σ) → Var (Γ - s) τ →
  (t : Var Δ τ) → Var (Δ - t) σ → Set where
  vz₁ : {Γ : Con} (v : Var Γ τ) → vz > v ⇔ vs v < vz
  vz₂ : {Γ : Con} (v : Var Γ σ) → vs v > vz ⇔ vz < v
  vs  : {Γ : Con} {Δ : Con} {ν : Ty}
        {s₁ : Var Γ σ} {t₁ : Var (Γ - s₁) τ} →
        {t₂ : Var Δ τ} {s₂ : Var (Δ - t₂) σ} → 
        s₁ > t₁ ⇔ t₂ < s₂ →
        vs {τ = ν} s₁ > vs t₁ ⇔ vs {τ = ν} t₂ < vs s₂

open import Relation.Binary.PropositionalEquality

wkCSwap : {σ τ : Ty} {Γ : Con} {Δ : Con} →
          {s₁ : Var Γ σ} {t₁ : Var (Γ - s₁) τ} →
          {t₂ : Var Δ τ} {s₂ : Var (Δ - t₂) σ} →
          s₁ > t₁ ⇔ t₂ < s₂ →
          Γ - s₁ - t₁ ≡ Δ - t₂ - s₂
wkCSwap (vz₁ v) = refl
wkCSwap (vz₂ v) = refl
wkCSwap (vs  k) = cong (_, _) (wkCSwap k)

wkv : ∀ {Γ σ τ} → (x : Var Γ σ) → Var (Γ - x) τ → Var Γ τ
wkv vz y = vs y
wkv (vs x) vz = vz
wkv (vs x) (vs y) = vs (wkv x y)

open import Data.Product hiding (swap)
open import Function

swap : {Γ : Con} {σ τ : Ty}
        (s : Var Γ σ) (t : Var (Γ - s) τ) →
        ∃ (s > t ⇔ wkv s t <_)
swap vz     t      = vz , vz₁ t
swap (vs s) vz     = s  , vz₂ s
swap (vs s) (vs t) = map vs vs (swap s t)

wkTm : ∀ {Γ σ τ} → (x : Var Γ σ) → Tm (Γ - x) τ → Tm Γ τ
wkTm x (var v)     = var (wkv x v)
wkTm x (app t₁ t₂) = (app (wkTm x t₁) (wkTm x t₂))
wkTm x (Λ t)       = Λ (wkTm (vs x) t)
wkTm x (c k)       = c k

data _≅V_ : {Γ Δ : Con} {σ : Ty} → Var Γ σ → Var Δ σ → Set where
  vz : {Γ Δ : Con} {σ : Ty} → _≅V_ {Γ , σ} {Δ , σ} {σ} vz vz
  vs : {Γ Δ : Con} {σ τ : Ty} →
       {v₁ : Var Γ σ} {v₂ : Var Δ σ} →
       v₁ ≅V v₂ → 
       _≅V_ {Γ , τ} {Δ , τ} (vs v₁) (vs v₂)

data _≅T_ : {Γ Δ : Con} {σ : Ty} → Tm Γ σ → Tm Δ σ → Set where
  var : {Γ Δ : Con} {σ : Ty}
        {v₁ : Var Γ σ} {v₂ : Var Δ σ} →
        v₁ ≅V v₂ → var v₁ ≅T var v₂
  app : {Γ Δ : Con} {σ τ : Ty}
        {f₁ : Tm Γ (σ ⇒ τ)} {f₂ : Tm Δ (σ ⇒ τ)} →
        {t₁ : Tm Γ σ} {t₂ : Tm Δ σ} →
        f₁ ≅T f₂ → t₁ ≅T t₂ →
        app f₁ t₁ ≅T app f₂ t₂
  Λ   : {Γ Δ : Con} {σ τ : Ty}
        {b₁ : Tm (Γ , σ) τ} {b₂ : Tm (Δ , σ) τ} →
        b₁ ≅T b₂ →
        Λ b₁ ≅T Λ b₂
  c   : {Γ Δ : Con} {k : Const} →
        _≅T_ {Γ} {Δ} (c k) (c k)

wk≅ : {Γ : Con} {σ : Ty} (v : Var Γ σ)
      {ν : Ty} (n₁ : Var (Γ - v) ν) (n₂ : Var (Γ - v) ν) →
      n₁ ≅V n₂ → wkv v n₁ ≅V wkv v n₂
wk≅ vz     n₁ n₂ eq = vs eq
wk≅ (vs v) vz      vz      vz      = vz
wk≅ (vs v) (vs n₁) (vs n₂) (vs eq) = vs (wk≅ v n₁ n₂ eq)
wk≅ (vs v) vz (vs n₂) ()
wk≅ (vs v) (vs n₁) vz ()

swapV : {Γ Δ : Con} {σ τ : Ty}
        {s₁ : Var Γ σ} {t₁ : Var (Γ - s₁) τ} →
        {t₂ : Var Δ τ} {s₂ : Var (Δ - t₂) σ} →
        s₁ > t₁ ⇔ t₂ < s₂ →
        {ν : Ty} (n₁ : Var (Γ - s₁ - t₁) ν) (n₂ : Var (Δ - t₂ - s₂) ν) →
        n₁ ≅V n₂ → wkv s₁ (wkv t₁ n₁) ≅V wkv t₂ (wkv s₂ n₂)
swapV (vz₁ v)  n₁      n₂      eq      = vs (wk≅ v n₁ n₂ eq)
swapV (vz₂ v)  n₁      n₂      eq      = vs (wk≅ v n₁ n₂ eq)
swapV (vs prf) vz      vz      vz      = vz
swapV (vs prf) (vs n₁) (vs n₂) (vs eq) = vs (swapV prf n₁ n₂ eq)
swapV (vs prf) (vs n₁) vz ()
swapV (vs prf) vz (vs n₂) ()

swapT : {Γ Δ : Con} {σ τ : Ty}
        {s₁ : Var Γ σ} {t₁ : Var (Γ - s₁) τ} →
        {t₂ : Var Δ τ} {s₂ : Var (Δ - t₂) σ} →
        s₁ > t₁ ⇔ t₂ < s₂ →
        {ν : Ty} (n₁ : Tm (Γ - s₁ - t₁) ν) (n₂ : Tm (Δ - t₂ - s₂) ν) →
        n₁ ≅T n₂ → wkTm s₁ (wkTm t₁ n₁) ≅T wkTm t₂ (wkTm s₂ n₂)
swapT prf (var x)     (var x₁)    (var eq₁)    = var (swapV prf x x₁ eq₁)
swapT prf (app n₁ n₂) (app n₃ n₄) (app eq eq₁) =
  app (swapT prf n₁ n₃ eq) (swapT prf n₂ n₄ eq₁)
swapT prf (Λ n₁)      (Λ n₂)      (Λ eq)       = Λ (swapT (vs prf) n₁ n₂ eq)
swapT prf (c k)       (c .k)      c            = c
swapT _ (var _) (app _ _) ()
swapT _ (var _) (Λ _) ()
swapT _ (var _) (c _) ()
swapT _ (app _ _) (var _) ()
swapT _ (app _ _) (Λ _) ()
swapT _ (app _ _) (c _) ()
swapT _ (Λ _) (var _) ()
swapT _ (Λ _) (app _ _) ()
swapT _ (c _₁) (var _) ()
swapT _ (c _₁) (app _ _) ()

reflV : {Γ : Con} {σ : Ty} (v : Var Γ σ) → v ≅V v
reflV vz     = vz
reflV (vs x) = vs (reflV x)

reflT : {Γ : Con} {σ : Ty} (t : Tm Γ σ) → t ≅T t
reflT (var v)   = var (reflV v)
reflT (app f t) = app (reflT f) (reflT t)
reflT (Λ t)     = Λ (reflT t)
reflT (c k)     = c

reflT′ : {Γ Δ : Con} {σ : Ty} (eq : Γ ≡ Δ) (t : Tm Γ σ) →
         t ≅T subst (flip Tm σ) eq t
reflT′ refl t = reflT t

Vrefl : {Γ : Con} {σ : Ty} {t u : Var Γ σ} → t ≅V u → t ≡ u
Vrefl vz      = refl
Vrefl (vs eq) = cong vs (Vrefl eq)

Trefl : {Γ : Con} {σ : Ty} {t u : Tm Γ σ} → t ≅T u → t ≡ u
Trefl (var v)       = cong var (Vrefl v)
Trefl (app eq₁ eq₂) = cong₂ app (Trefl eq₁) (Trefl eq₂)
Trefl (Λ eq)        = cong Λ (Trefl eq)
Trefl c             = refl

THEOREM :
  {Γ Δ : Con} {σ τ : Ty} (s : Var Γ σ) (t : Var (Γ - s) τ) →
  {ν : Ty} (n : Tm (Γ - s - t) ν) →
  let coerce = subst (flip Tm ν) (wkCSwap (proj₂ (swap s t))) in
  wkTm s (wkTm t n) ≡ wkTm (wkv s t) (wkTm (proj₁ (swap s t)) (coerce n))
THEOREM s t n =
  let related = proj₂ (swap s t) in
  Trefl (swapT related n _ (reflT′ (wkCSwap related) n))