add tP to IFS

IFReindexing.agda

@@ -17,10 +17,19 @@ module IFReindexing {Ωc}(Ω : Con Ωc)
   (ʷˢc : ˢc (ᴱc Ωc) (ʷc Ω (conᵃ (ᴱC Ω)) id))
   (ʷˢC : ˢC (ᴱC Ω) ʷˢc (ʷC Ω (conᵃ (ᴱC Ω)) idP)) where
 
-ᴿS'' : ∀{B}(t : Tm Ωc B) → _ᵃS {suc zero} B
-ᴿS'' {U}      t = ∃ λ α → hdfill Ω (conᵃ (ᴱC Ω)) t (ˢt (ᴱt t) ʷˢc α)
-ᴿS'' {T ⇒̂S B} t = λ τ → ᴿS'' (t $S τ)
+ᴿS : ∀{B}(t : Tm Ωc B) → _ᵃS {suc zero} B
+ᴿS {U}      t = ∃ λ α → hdfill Ω (conᵃ (ᴱC Ω)) t (ˢt (ᴱt t) ʷˢc α)
+ᴿS {T ⇒̂S B} t = λ τ → ᴿS (t $S τ)
 
 ᴿc : ∀{Γc}(σ : Sub Ωc Γc) → _ᵃc {suc zero} Γc
 ᴿc ε       = lift tt
-ᴿc (σ , t) = ᴿc σ , ᴿS'' t
+ᴿc (σ , t) = ᴿc σ , ᴿS t
+
+ᴿP : (A : TyP Ωc)(tP : TmP Ω A) → _ᵃP {suc zero} A (ᴿc id)
+ᴿP (El a)   tP = {!!}
+ᴿP (Π̂P T A) tP = λ τ → ᴿP (A τ) (tP $̂P τ)
+ᴿP (a ⇒P A) tP = λ α → ᴿP A (tP $P {!!})
+
+ᴿC : ∀{Γ}(σP : SubP Ω Γ) → _ᵃC {suc zero} Γ (ᴿc id)
+ᴿC εP         = lift tt
+ᴿC (σP ,P tP) = ᴿC σP , ᴿP _ tP

IFS.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --rewriting #-}
+{-# OPTIONS --rewriting --allow-unsolved-metas #-}
 module IFS where
 
 open import Lib hiding (id; _∘_)
@@ -31,3 +31,10 @@ open import IFD
 ˢs : ∀{ℓ' ℓ Γc Δc} σ {γc}{γcᵈ : ᵈc {ℓ'}{ℓ} Γc γc} → ˢc Γc γcᵈ → ˢc Δc (ᵈs σ γcᵈ)
 ˢs ε       γcˢ = lift tt
 ˢs (σ , t) γcˢ = ˢs σ γcˢ , ˢt t γcˢ
+
+ˢtP : ∀{ℓ' ℓ Γc Γ}{A : TyP Γc}(tP : TmP Γ A){γc}{γcᵈ : ᵈc {ℓ'}{ℓ} Γc γc}{γcˢ : ˢc Γc γcᵈ}
+      {γ}{γᵈ : ᵈC Γ γcᵈ γ} → ˢC Γ γcˢ γᵈ → ˢP A γcˢ (ᵈtP tP γᵈ)
+ˢtP (varP vvzP)              (γˢ , αˢ) = αˢ
+ˢtP (varP (vvsP vP))         (γˢ , αˢ) = ˢtP (varP vP) γˢ
+ˢtP (t $P s)         {γ = γ} γˢ        = coe (ˢP _ _ & (ᵈtP t _ _ & ˢtP s γˢ)) (ˢtP t γˢ ((s ᵃtP) γ))
+ˢtP (t $̂P τ)                 γˢ        = ˢtP t γˢ τ

IFW.agda

@@ -62,7 +62,7 @@ hdfill (t $S τ) α = hdfill t α τ
 ʷt=id t α = ʷt= id t α
 {-# REWRITE ʷt=id #-}
 
-ʷP : ∀ A (α : (ᴱP A ᵃP) ωc)(X : Set ℓ) → ᵈP (ᴱP A) (ʷc id) α
+ʷP : ∀ A (α : (ᴱP A ᵃP) ωc)(X : Set ℓ) → ᵈP (ᴱP A) (ʷc id) α -- maybe put the term itself into the signature
 ʷP (El a)   α X = hdfill a (f2 (f1 (ʷv' (hd a) X))) -- check again, maybe revive old ʷt'
 ʷP (Π̂P T A) ϕ X = λ τ → ʷP (A τ) (ϕ τ) X
 ʷP (a ⇒P A) ϕ X = λ α αᵈ → ʷP A (ϕ α) (X × hdfill a αᵈ)