restored to undo dead-end

src/Typed.lagda

@@ -248,31 +248,21 @@ fresh-lemma x∈ refl =  1+n≰n (⊔-lemma x∈)
 ### Identifier maps
 
 \begin{code}
-Map : List Id → Set
-Map xs = ∀ {x} → x ∈ xs → Term
-
-default : ∀ (xs : List Id) → Map xs
-default xs = φ
-  where
-  φ : ∀ {x : Id} (x∈ : x ∈ xs) → Term
-  φ {x} x∈  =  ` x
+∅ : Id → Term
+∅ x = ` x
 
 infixl 5 _,_↦_
 
-_,_↦_ : ∀ {xs} → Map xs → (x : Id) → Term → Map (x ∷ xs)
-(φ , x ↦ M) here        =  M
-(φ , x ↦ M) (there w∈)  =  φ w∈
+_,_↦_ : (Id → Term) → Id → Term → (Id → Term)
+(ρ , x ↦ M) w with w ≟ x
+...               | yes _   =  M
+...               | no  _   =  ρ w
 \end{code}
 
-### Free variables
-
 ### Substitution
 
-Build-in the invariant that `rho` covers all free variables in term,
-and don't pass y separately
-
 \begin{code}
-subst : ∀ (N : Term) → Map (free N) → Term
+subst : List Id → (Id → Term) → Term → Term
 subst ys ρ (` x)          =  ρ x
 subst ys ρ (`λ x ⇒ N)     =  `λ y ⇒ subst (y ∷ ys) (ρ , x ↦ ` y) N
   where
@@ -511,7 +501,6 @@ preservation (`λ ⊢N) ()
 preservation (⊢L · ⊢M) (ξ-⟹₁ L⟶L′)        =  preservation ⊢L L⟶L′ · ⊢M
 preservation (⊢V · ⊢M) (ξ-⟹₂ valV M⟶M′)   =  ⊢V · preservation ⊢M M⟶M′
 preservation ((`λ ⊢N) · ⊢W) (β-⟹ valW)      =  ⊢substitution ⊢N ⊢W
--}
 \end{code}