{-# OPTIONS --safe --without-K #-}
module IK.Term.NormalForm.Properties where

open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; trans ; cong ; cong₂)

open import IK.Term.Base

open import IK.Term.NormalForm.Base

wkNePresId : (n : Ne Γ a) → wkNe idWk n ≡ n
wkNfPresId : (n : Nf Γ a) → wkNf idWk n ≡ n

wkNePresId (var   v)   = cong  var (wkVarPresId v)
wkNePresId (app   n m) = cong₂ app (wkNePresId  n) (wkNfPresId m)
wkNePresId (unbox n e) with ←#IsPre# e | #→IsPost# e
... | refl | refl = cong₂ unbox
  (trans (cong₂ wkNe (sliceLeftId e) refl) (wkNePresId n))
  (wkLFExtPresId e)

wkNfPresId (up  n) = cong up  (wkNePresId n)
wkNfPresId (lam n) = cong lam (wkNfPresId n)
wkNfPresId (box n) = cong box (wkNfPresId n)

wkNePres∙ : (w : Γ ⊆ Γ') (w' : Γ' ⊆ Δ) (n : Ne Γ a)
  → wkNe w' (wkNe w n) ≡ wkNe (w ∙ w') n
wkNfPres∙ : (w : Γ ⊆ Γ') (w' : Γ' ⊆ Δ) (n : Nf Γ a)
  → wkNf w' (wkNf w n) ≡ wkNf (w ∙ w') n

wkNePres∙ w w' (var   v)   = cong  var (wkVarPres∙ w w' v)
wkNePres∙ w w' (app   n m) = cong₂ app (wkNePres∙  w w' n) (wkNfPres∙ w w' m)
wkNePres∙ w w' (unbox n e) = cong₂ unbox
  (trans (wkNePres∙ _ _ _) (cong₂ wkNe (sliceLeftPres∙ w w' e) refl)) (wkLFExtPres∙ w w' e)

wkNfPres∙ w w' (up  n) = cong up  (wkNePres∙ w w' n)
wkNfPres∙ w w' (lam n) = cong lam (wkNfPres∙ (keep w) (keep w') n)
wkNfPres∙ w w' (box n) = cong box (wkNfPres∙ (keep# w) (keep# w') n)

------------------------
-- Naturality conditions
------------------------

-- Normal forms and neutrals obey "naturality" of embeddding, i.e.,
-- weakening can be commuted with embedding.

-- the mutual brothers normal forms and neutrals who,
-- as always, must be handled (mutually) together
nat-embNe : (w : Γ ⊆ Γ') (n : Ne Γ a)
  → wkTm w (embNe n) ≡ embNe (wkNe w n)
nat-embNf : (w : Γ ⊆ Γ') (n : Nf Γ a)
  → wkTm w (embNf n) ≡ embNf (wkNf w n)

nat-embNf w (up  x) = nat-embNe w x
nat-embNf w (lam n) = cong lam (nat-embNf (keep w) n)
nat-embNf w (box n) = cong box (nat-embNf (keep# w) n)

nat-embNe w (var x)     = refl
nat-embNe w (app n x)   = cong₂ app (nat-embNe w n) (nat-embNf w x)
nat-embNe w (unbox n x) = cong₂ unbox (nat-embNe (sliceLeft x w) n) refl

Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.