Preservation proof doesn't go through.

newtry.agda

module newtry where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (True; toWitness)
open import Data.Fin
open import Data.Nat
open import Data.Product
open import Data.Empty
open import Data.Unit

data Term (n : ℕ) : Set where
    var : Fin n → Term n
    app : Term n → Term n → Term n
    lam : Term (suc n) → Term n
    pi : Term n → Term (suc n) → Term n
    u : ℕ → Term n

data Context : ℕ → Set where
    ∅ : Context zero
    _,_ : ∀{n} → Context n → Term n → Context (suc n)

extend' : ∀{n} → Fin (suc n) → Fin n → Fin (suc n)
extend' 0F x = suc x
extend' (suc n) 0F = 0F
extend' (suc n) (suc x) = suc (extend' n x)

extend : ∀{n} → Fin (suc n) → Term n → Term (suc n)
extend n (var x) = var (extend' n x)
extend n (app t v) = app (extend n t) (extend n v)
extend n (lam t) = lam (extend (suc n) t)
extend n (pi t v) = pi (extend n t) (extend (suc n) v)
extend n (u i) = u i

lookup : ∀{n} → Context n → Fin n → Term n
lookup (ctx , x) 0F = extend 0F x
lookup (ctx , x) (suc n) = extend 0F (lookup ctx n)

exts : ∀ {n} (p : Fin (suc n) → Term n) → Fin (suc (suc n)) → Term (suc n)
exts p 0F = var 0F
exts p (suc x) = extend 0F (p x)

subst : ∀{n} → (Fin (suc n) → Term n) → Term (suc n) → Term n
subst p (var x) = p x
subst p (app t v) = app (subst p t) (subst p v)
subst p (lam t) = lam (subst (exts p) t)
subst p (pi t v) = pi (subst p t) (subst (exts p) v)
subst p (u n) = u n

infix 10 _⇒_
infix 10 _⇒*_

_[_] : ∀{n} → Term (suc n) → Term n → Term n
_[_] {n} f x = subst p f
  where p : Fin (suc n) → Term n
        p 0F = x
        p (suc i) = var i

data _⇒_ {n} : Term n → Term n → Set where
    betaLam : ∀ {p x y}
      → p [ x ] ≡ y
      → app (lam p) x ⇒ y
    etaLam : ∀ {p q}
      → p ⇒ q
      → lam p ⇒ lam q
    eta1 : ∀ {p q x}
      → p ⇒ q
      → app p x ⇒ app q x
    eta2 : ∀ {p q x}
      → p ⇒ q
      → app x p ⇒ app x q
    pi1 : ∀ {p q x}
      → p ⇒ q
      → pi p x ⇒ pi q x
    pi2 : ∀ {p q x}
      → p ⇒ q
      → pi x p ⇒ pi x q

data _⇒*_ {n} : Term n → Term n → Set where
    refl : ∀ {a} → a ⇒* a
    step : ∀ {a b c} → a ⇒ b → b ⇒* c → a ⇒* c

data Normal {n} : Term n → Set
data Neutral {n} : Term n → Set

data Neutral where
    var : ∀{n} → Neutral (var n)
    app : ∀{x y} → Neutral x → Normal y → Neutral (app x y)

data Normal where
    neutral : ∀{x} → Neutral x → Normal x
    lam : ∀{x} → Normal x → Normal (lam x)
    pi : ∀{x y} → Normal x → Normal y → Normal (pi x y)
    u : ∀{n} → Normal (u n)

mutual
  neutralNotReduce : ∀{i} {n m : Term i} → (Neutral n) → n ⇒ m → ⊥
  neutralNotReduce (app x y) (eta1 xm) = neutralNotReduce x xm
  neutralNotReduce (app x y) (eta2 ym) = normalNotReduce y ym

  normalNotReduce : ∀{i} {n m : Term i} → (Normal n) → n ⇒ m → ⊥
  normalNotReduce (neutral x) nm = neutralNotReduce x nm
  normalNotReduce (lam n) (etaLam nm) = normalNotReduce n nm
  normalNotReduce (pi x y) (pi1 xm) = normalNotReduce x xm
  normalNotReduce (pi x y) (pi2 ym) = normalNotReduce y ym

data _⊢_∶_ {n} : Context n → Term n → Term n → Set where
    var : ∀ {G n t}
        → G ⊢ var n ∶ t
    app : ∀ {G f a g x y}
        → G ⊢ f ∶ pi a g
        → G ⊢ x ∶ a
        → (app (lam g) x) ⇒* y × Normal y
        → G ⊢ app f x ∶ y
    lam : ∀ {G A f B}
        → (G , A) ⊢ f ∶ B
        → G ⊢ lam f ∶ pi A B
    pi : ∀ {G x n g}
        → G ⊢ x ∶ u n
        → (G , x) ⊢ g ∶ u n
        → G ⊢ pi x g ∶ u n
    u : ∀ {G n}
        → G ⊢ u n ∶ u (suc n)
    ↑ : ∀ {G x n}
        → G ⊢ x ∶ u n
        → G ⊢ x ∶ u (suc n)

data Progress {n} (t : Term n) : Set where
  step : ∀ {v} → t ⇒ v → Progress t
  done : Normal t → Progress t

progress : ∀{n ctx} {term type : Term n} → ctx ⊢ term ∶ type → Progress term
progress var = done (neutral var)
progress (app t v conv) with progress t
progress (app t v conv) | step x = step (eta1 x)
progress (app t v conv) | done x with progress v
progress (app t v conv) | done x | step y = step (eta2 y)
progress (app t v conv) | done (neutral x) | done y = done (neutral (app x y))
progress (app t v conv) | done (lam x) | done y = step (betaLam refl)
progress (lam t) with progress t
progress (lam t) | step x = step (etaLam x)
progress (lam t) | done x = done (lam x)
progress (pi t v) with progress t
progress (pi t v) | step x = step (pi1 x)
progress (pi t v) | done x with progress v
progress (pi t v) | done x | step y = step (pi2 y)
progress (pi t v) | done x | done y = done (pi x y)
progress u = done u
progress (↑ t) = progress t

transform : ∀ {n} {g : Term (suc n)} {x q type : Term n}
          → app (lam g) x ⇒* type
          → x ⇒ q 
          → app (lam g) q ⇒* type
transform x xq = {!!}

transform' : ∀ {n i} {ctx : Context n} {x q : Term n} {g : Term (suc n)}
             → (ctx , x) ⊢ g ∶ u i
             → (x ⇒ q)
             → (ctx , q) ⊢ g ∶ u i
transform' var trans = {!!}
transform' (app t v x) trans = {!!}
transform' (pi t v) trans = pi (transform' t trans) {!transform' v trans!}
transform' u trans = u
transform' (↑ term) trans = ↑ (transform' term trans)

preserveSubst : ∀{n} {ctx : Context n} {x a type : Term n} {f g : Term (suc n)}
  → ctx ⊢ x ∶ a
  → (ctx , a) ⊢ f ∶ g
  → app (lam g) x ⇒* type × Normal type
  → ctx ⊢ f [ x ] ∶ type
preserveSubst x f (gxn , norm) = {!!}

preserve : ∀{n ctx} {t v type : Term n} → ctx ⊢ t ∶ type → t ⇒ v → ctx ⊢ v ∶ type
preserve (app (lam t) v conv) (betaLam refl) = preserveSubst v t conv
preserve (app t v conv) (eta1 s) = app (preserve t s) v conv
preserve (app t v (TN , nT)) (eta2 s) = app t (preserve v s) (transform TN s , nT)
preserve (lam t) (etaLam s) = lam (preserve t s)
preserve (pi t v) (pi1 s) = pi (preserve t s) (transform' v s)
preserve (pi t v) (pi2 s) = pi t (preserve v s)
preserve (↑ term) s = ↑ (preserve term s)