The commute-subst-rename lemma in the Substitution chapter quantifies over polymorphic renaming ρ : ∀{Γᵨ} → Rename Γᵨ (Γᵨ , ★) (i.e. the ρ itself quantifies over the context Γᵨ), but the parameter Γᵨ is only instantiated with Γᵨ = Γ and Γᵨ = Δ. Thus we can replace this with just two renamings ρ₁ : Rename Γ (Γ , ★) and ρ₂ : Rename Δ (Δ , ★). By this way, we can also avoid defining some what awkward ρ′. I think the resulting proof is more clean.
I also fixed the corresponding prose below the agda code. It seems that the equational reasoning part was just broken, for example in this line:
The
commute-subst-renamelemma in the Substitution chapter quantifies over polymorphic renamingρ : ∀{Γᵨ} → Rename Γᵨ (Γᵨ , ★)(i.e. theρitself quantifies over the contextΓᵨ), but the parameterΓᵨis only instantiated withΓᵨ = ΓandΓᵨ = Δ. Thus we can replace this with just two renamingsρ₁ : Rename Γ (Γ , ★)andρ₂ : Rename Δ (Δ , ★). By this way, we can also avoid defining some what awkwardρ′. I think the resulting proof is more clean.I also fixed the corresponding prose below the agda code. It seems that the equational reasoning part was just broken, for example in this line:
which should be
even if we keep using polymorphic renaming.