{-# OPTIONS --without-K --rewriting #-} module ag-000Q where open import MLTT.Spartan hiding (_⊔_; id) open import ag-000M using (Ty; _⇒_; Con; ◇; _▷_) open import ag-000N open import ag-000O open import ag-000P
⁺-nat[]v : (i : Γ ⊢[ V ] A) → (xs : Δ ⊩[ q ] Γ) → i [ xs ⁺ B ] ＝ there[ q ] (i [ xs ]) B ⁺-nat[]v here (xs , x) = refl ⁺-nat[]v (there j _) (xs , x) = ⁺-nat[]v j xs [id] : x [ id ] ＝ x [id] {x = here} = refl [id] {x = there i B} = (i [ id ⁺ B ]) ＝⟨ ⁺-nat[]v {q = V} i id ⟩ there (i [ id ]) B ＝⟨ ap (λ - → there - B) [id] ⟩ there i B ∎ [id] {x = ` i} = ap `_ [id] [id] {x = t · u} = ((t [ id ]) · (u [ id ])) ＝⟨ ap (t [ id ] ·_) [id] ⟩ ((t [ id ]) · u) ＝⟨ ap (_· u) [id] ⟩ (t · u) ∎ [id] {x = ƛ t} = ap ƛ_ [id] ◦id : xs ◦ id ＝ xs ◦id {xs = ε} = refl ◦id {xs = xs , x} = (xs ◦ id) , (x [ id ]) ＝⟨ ap ((xs ◦ id) ,_) [id] ⟩ (xs ◦ id) , x ＝⟨ ap (_, x) ◦id ⟩ xs , x ∎