add point substs to IF erasure

IF.agda

@@ -256,5 +256,13 @@ TmP∙ (tP $̂P τ)  = TmP∙ tP
 [idP]tP {tP = tP $̂P τ}       = happly2 _$̂P_ [idP]tP τ
 {-# REWRITE [idP]tP #-}
 
+vsP[,P]tP : ∀{Γc}{Γ Δ : Con Γc}{A A'}{tP : TmP Δ A}{sP}{σP : SubP Γ Δ}
+            → (vsP {A' = A'} tP) [ σP ,P sP ]tP ≡ tP [ σP ]tP
+vsP[,P]tP {tP = varP x} = refl
+vsP[,P]tP {tP = tP $P sP} {rP} {σP} = _$P_ & vsP[,P]tP {tP = tP}{rP}{σP}
+                                      ⊗ vsP[,P]tP {tP = sP} {rP} {σP}
+vsP[,P]tP {tP = tP $̂P τ} {sP} {σP} = (λ tP → tP $̂P τ)
+                                      & vsP[,P]tP {tP = tP}{sP}{σP}
+{-# REWRITE vsP[,P]tP #-}
 
 --TODO complete calculus here

IFE.agda

@@ -78,3 +78,44 @@ idᴱ {Γc ▶c B} = (λ σ → σ , vz) & (wk & idᴱ {Γc = Γc})
 π₂ᴱ : ∀{Γc Δc A}{σ : Sub Γc (Δc ▶c A)} → ᴱt (π₂ σ) ≡ π₂ (ᴱs σ)
 π₂ᴱ {σ = σ , x} = refl
 {-# REWRITE π₂ᴱ #-}
+
+ᴱtP : ∀{Γc}{Γ : Con Γc}{A} → TmP Γ A → TmP (ᴱC Γ) (ᴱP A)
+ᴱtP (varP vvzP)     = varP vvzP
+ᴱtP (varP (vvsP x)) = vsP (ᴱtP (varP x))
+ᴱtP (tP $P sP)      = ᴱtP tP $P ᴱtP sP
+ᴱtP (tP $̂P τ)       = ᴱtP tP $̂P τ
+
+ᴱsP : ∀{Γc}{Γ Δ : Con Γc} → SubP Γ Δ → SubP (ᴱC Γ) (ᴱC Δ)
+ᴱsP εP         = εP
+ᴱsP (σP ,P tP) = ᴱsP σP ,P ᴱtP tP
+
+vsP,ᴱ : ∀{Γc}{Γ : Con Γc}{A A'}{tP : TmP Γ A}
+        → ᴱtP (vsP {A' = A'} tP) ≡ vsP (ᴱtP tP)
+vsP,ᴱ {tP = varP x}   = refl
+vsP,ᴱ {tP = tP $P sP} = _$P_ & vsP,ᴱ {tP = tP}
+                        ⊗ vsP,ᴱ {tP = sP}
+vsP,ᴱ {tP = tP $̂P τ}  = (λ tP → tP $̂P τ) & vsP,ᴱ {tP = tP}
+{-# REWRITE vsP,ᴱ #-}
+
+[]ᴱtP : ∀{Γc}{Γ Δ : Con Γc}{A}{tP : TmP Δ A}{σP : SubP Γ Δ}
+        → ᴱtP (tP [ σP ]tP) ≡ ᴱtP tP [ ᴱsP σP ]tP
+[]ᴱtP {tP = varP vvzP}     {σP ,P _} = refl
+[]ᴱtP {tP = varP (vvsP x)} {σP ,P _} = []ᴱtP {tP = varP x} {σP}
+[]ᴱtP {tP = tP $P sP}      {σP}      = _$P_ & []ᴱtP {tP = tP} {σP}
+                                         ⊗ []ᴱtP {tP = sP} {σP}
+[]ᴱtP {tP = tP $̂P τ}       {σP}      = (λ tP → tP $̂P τ)
+                                         & []ᴱtP {tP = tP} {σP}
+{-# REWRITE []ᴱtP #-}
+
+wkP,ᴱ : ∀{Γc}{Γ Δ : Con Γc}{A}(σP : SubP Γ Δ)
+        → ᴱsP (wkP {A = A} σP) ≡ wkP (ᴱsP σP)
+wkP,ᴱ εP         = refl
+wkP,ᴱ (σP ,P tP) = (λ x → x ,P _) & wkP,ᴱ σP
+{-# REWRITE wkP,ᴱ #-}
+
+idPᴱ : ∀{Γc}{Γ : Con Γc} → ᴱsP (idP {Γ = Γ}) ≡ idP
+idPᴱ {Γ = ∙}      = refl
+idPᴱ {Γ = Γ ▶P A} = (λ σP → wkP σP ,P vzP) & (idPᴱ {Γ = Γ})
+{-# REWRITE idPᴱ #-}
+
+--TODO complete substitution calculus

IFW.agda

@@ -6,35 +6,20 @@ open import IFA
 open import IFD
 open import IFE
 
-module IFW where
+module IFW {Ωc}(Ω : Con Ωc)
+  {ωc : _ᵃc {zero} (ᴱc Ωc)}(ω : (ᴱC Ω ᵃC) ωc) where
 
-ʷS : TyS → Set₁
-ʷS U        = Set
-ʷS (Π̂S T B) = (τ : T) → ʷS (B τ)
+  data Nat : Set where
+    Z : Nat
+    S : Nat → Nat
 
-ʷc : (Γc : SCon)(γc : ᴱc Γc ᵃc) → ᵈc {zero}{suc zero} (ᴱc Γc) γc
-ʷc ∙c        γc       = lift tt
-ʷc (Γc ▶c B) (γc , α) = ʷc Γc γc , λ _ → ʷS B
-
-ʷP' : (B : TyS) → ʷS B
-ʷP' U        = ⊤
-ʷP' (Π̂S T B) = λ τ → ʷP' (B τ)
-
-ʷt : ∀{Γc B}(t : Tm Γc B){γc : ᴱc Γc ᵃc}(α : (ᴱt t ᵃt) γc)
-     → ᵈt (ᴱt t) (ʷc Γc γc) α
-ʷt (var vvz)     {γc , β} αʷ = ʷP' _
-ʷt (var (vvs x))          αʷ = ʷt (var x) αʷ
-ʷt (t $S τ)               αʷ = ʷt t αʷ
-
-ʷP : ∀{Γc}(A : TyP Γc){γc : ᴱc Γc ᵃc}(α : (ᴱP A ᵃP) γc)
-     → ᵈP (ᴱP A) (ʷc Γc γc) α
-ʷP (El a)   α = ʷt a α
-ʷP (Π̂P T A) α = λ τ → ʷP (A τ) (α τ)
-ʷP (a ⇒P A) α = λ β βʷ → ʷP A (α β)
-
-ʷC : ∀{Γc}(Γ : Con Γc){γc}(γ : (ᴱC Γ ᵃC) γc)
-      → ᵈC (ᴱC Γ) (ʷc Γc γc) γ
-ʷC ∙        γ       = lift tt
-ʷC (Γ ▶P A) (γ , α) = ʷC Γ γ , ʷP A α
+  ʷS : TyS → Set₁
+  ʷS U        = Set
+  ʷS (Π̂S T B) = (τ : T) → ʷS (B τ)
 
+  ʷc : ∀{Γc}(σ : Sub Ωc Γc) → ᵈc {suc zero} (ᴱc Γc) ((ᴱs σ ᵃs) ωc)
+  ʷc ε                 = lift tt
+  ʷc (_,_ {B = B} σ t) = ʷc σ , λ _ → ʷS B
 
+  ʷP : ∀{A}(tP : TmP Ω A) → ᵈP (ᴱP A) (ʷc id) (({!!} ᵃtP) ω)
+  ʷP = {!!}