From c0da332b88c233cba9fad63c5ffac39195af292b Mon Sep 17 00:00:00 2001
From: 0xd34df00d <0xd34df00d@gmail.com>
Date: Sat, 23 Jan 2021 12:20:50 -0600
Subject: [PATCH] Update anchors

---
 agda/Surface/Theorems/SubstTyping.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/agda/Surface/Theorems/SubstTyping.agda b/agda/Surface/Theorems/SubstTyping.agda
index 0112ee63..04f42514 100644
--- a/agda/Surface/Theorems/SubstTyping.agda
+++ b/agda/Surface/Theorems/SubstTyping.agda
@@ -89,6 +89,7 @@ var-later-in-Γ-remains {k = suc k} {ι = suc ι} ε (∈-suc {τ = τ} refl τ
                 | weaken-ε-suc-k k ε
                 = refl
 
+-- Referred to as typing-substitution in the paper
 mutual
   sub-Γok : ∀ {k} {Γ : Ctx ℓ} {Γ,σ,Δ : Ctx (suc k + ℓ)}
           → Γ ⊢ ε ⦂ σ
@@ -100,7 +101,6 @@ mutual
   sub-Γok {k = suc _} εδ (prefix-cons Γ-prefix-Γ,σ,Δ) σ-∈ (TCTX-Bind Γ,σ,Δok τδ)
       = TCTX-Bind (sub-Γok εδ Γ-prefix-Γ,σ,Δ (∈-chop (∈-sucify σ-∈)) Γ,σ,Δok) (sub-Γ⊢τ εδ Γ-prefix-Γ,σ,Δ (∈-chop (∈-sucify σ-∈)) τδ)
 
-  -- Referred to as sub-TWF in the paper
   sub-Γ⊢τ : ∀ {k} {Γ : Ctx ℓ} {Γ,σ,Δ : Ctx (suc k + ℓ)} {τ : SType (suc k + ℓ)}
           → Γ ⊢ ε ⦂ σ
           → Γ prefix-at suc k of Γ,σ,Δ