@@ -60,9 +60,9 @@ record Lemmas₀ {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where
6060 lookup-map-weaken-↑⋆ zero x = refl
6161 lookup-map-weaken-↑⋆ (suc k) zero = refl
6262 lookup-map-weaken-↑⋆ (suc k) (suc x) {ρ} = begin
63- lookup (map weaken (map weaken ρ ↑⋆ k)) x ≡⟨ VecProp.lookup-map x weaken _ ⟩
63+ lookup (map weaken (map weaken ρ ↑⋆ k)) x ≡⟨ VecProp.lookup-map x weaken (map weaken ρ ↑⋆ k) ⟩
6464 weaken (lookup (map weaken ρ ↑⋆ k) x) ≡⟨ cong weaken (lookup-map-weaken-↑⋆ k x) ⟩
65- weaken (lookup ((ρ ↑) ↑⋆ k) (lift k suc x)) ≡⟨ sym $ VecProp.lookup-map (lift k suc x) _ _ ⟩
65+ weaken (lookup ((ρ ↑) ↑⋆ k) (lift k suc x)) ≡⟨ sym $ VecProp.lookup-map (lift k suc x) weaken ((ρ ↑) ↑⋆ k) ⟩
6666 lookup (map weaken ((ρ ↑) ↑⋆ k)) (lift k suc x) ∎
6767
6868record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
@@ -77,7 +77,7 @@ record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
7777 lookup ρ x ≡ var y →
7878 lookup (map weaken ρ) x ≡ var (suc y)
7979 lookup-map-weaken x {y} {ρ} hyp = begin
80- lookup (map weaken ρ) x ≡⟨ VecProp.lookup-map x _ _ ⟩
80+ lookup (map weaken ρ) x ≡⟨ VecProp.lookup-map x weaken ρ ⟩
8181 weaken (lookup ρ x) ≡⟨ cong weaken hyp ⟩
8282 weaken (var y) ≡⟨ weaken-var ⟩
8383 var (suc y) ∎
@@ -89,23 +89,23 @@ record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
8989 lookup-id (suc x) = lookup-wk x
9090
9191 lookup-wk : ∀ {n} (x : Fin n) → lookup wk x ≡ var (suc x)
92- lookup-wk x = lookup-map-weaken x (lookup-id x)
92+ lookup-wk x = lookup-map-weaken x {ρ = id} (lookup-id x)
9393
9494 lookup-↑⋆ : ∀ {m n} (f : Fin m → Fin n) {ρ : Sub T m n} →
9595 (∀ x → lookup ρ x ≡ var (f x)) →
9696 ∀ k x → lookup (ρ ↑⋆ k) x ≡ var (lift k f x)
97- lookup-↑⋆ f hyp zero x = hyp x
98- lookup-↑⋆ f hyp (suc k) zero = refl
99- lookup-↑⋆ f hyp (suc k) (suc x) =
100- lookup-map-weaken x (lookup-↑⋆ f hyp k x)
97+ lookup-↑⋆ f hyp zero x = hyp x
98+ lookup-↑⋆ f hyp (suc k) zero = refl
99+ lookup-↑⋆ f {ρ = ρ} hyp (suc k) (suc x) =
100+ lookup-map-weaken x {ρ = ρ ↑⋆ k} (lookup-↑⋆ f hyp k x)
101101
102102 lookup-lift-↑⋆ : ∀ {m n} (f : Fin n → Fin m) {ρ : Sub T m n} →
103103 (∀ x → lookup ρ (f x) ≡ var x) →
104104 ∀ k x → lookup (ρ ↑⋆ k) (lift k f x) ≡ var x
105- lookup-lift-↑⋆ f hyp zero x = hyp x
106- lookup-lift-↑⋆ f hyp (suc k) zero = refl
107- lookup-lift-↑⋆ f hyp (suc k) (suc x) =
108- lookup-map-weaken (lift k f x) (lookup-lift-↑⋆ f hyp k x)
105+ lookup-lift-↑⋆ f hyp zero x = hyp x
106+ lookup-lift-↑⋆ f hyp (suc k) zero = refl
107+ lookup-lift-↑⋆ f {ρ = ρ} hyp (suc k) (suc x) =
108+ lookup-map-weaken (lift k f x) {ρ = ρ ↑⋆ k} (lookup-lift-↑⋆ f hyp k x)
109109
110110 lookup-wk-↑⋆ : ∀ {n} k (x : Fin (k + n)) →
111111 lookup (wk ↑⋆ k) x ≡ var (lift k suc x)
@@ -145,30 +145,30 @@ record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
145145
146146 lookup-⊙ : ∀ {m n k} x {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} →
147147 lookup (ρ₁ ⊙ ρ₂) x ≡ lookup ρ₁ x / ρ₂
148- lookup-⊙ x = VecProp.lookup-map x _ _
148+ lookup-⊙ x {ρ₁} {ρ₂} = VecProp.lookup-map x ( λ t → t / ρ₂) ρ₁
149149
150150 lookup-⨀ : ∀ {m n} x (ρs : Subs T m n) →
151151 lookup (⨀ ρs) x ≡ var x /✶ ρs
152152 lookup-⨀ x ε = lookup-id x
153153 lookup-⨀ x (ρ ◅ ε) = sym var-/
154154 lookup-⨀ x (ρ ◅ (ρ′ ◅ ρs′)) = begin
155155 lookup (⨀ (ρ ◅ ρs)) x ≡⟨ refl ⟩
156- lookup (⨀ ρs ⊙ ρ) x ≡⟨ lookup-⊙ x ⟩
156+ lookup (⨀ ρs ⊙ ρ) x ≡⟨ lookup-⊙ x {ρ₁ = ⨀ (ρ′ ◅ ρs′)} ⟩
157157 lookup (⨀ ρs) x / ρ ≡⟨ cong₂ _/_ (lookup-⨀ x (ρ′ ◅ ρs′)) refl ⟩
158158 var x /✶ ρs / ρ ∎
159159 where ρs = ρ′ ◅ ρs′
160160
161161 id-⊙ : ∀ {m n} {ρ : Sub T m n} → id ⊙ ρ ≡ ρ
162162 id-⊙ {ρ = ρ} = extensionality λ x → begin
163- lookup (id ⊙ ρ) x ≡⟨ lookup-⊙ x ⟩
163+ lookup (id ⊙ ρ) x ≡⟨ lookup-⊙ x {ρ₁ = id} ⟩
164164 lookup id x / ρ ≡⟨ cong₂ _/_ (lookup-id x) refl ⟩
165165 var x / ρ ≡⟨ var-/ ⟩
166166 lookup ρ x ∎
167167
168168 lookup-wk-↑⋆-⊙ : ∀ {m n} k {x} {ρ : Sub T (k + suc m) n} →
169169 lookup (wk ↑⋆ k ⊙ ρ) x ≡ lookup ρ (lift k suc x)
170170 lookup-wk-↑⋆-⊙ k {x} {ρ} = begin
171- lookup (wk ↑⋆ k ⊙ ρ) x ≡⟨ lookup-⊙ x ⟩
171+ lookup (wk ↑⋆ k ⊙ ρ) x ≡⟨ lookup-⊙ x {ρ₁ = wk ↑⋆ k} ⟩
172172 lookup (wk ↑⋆ k) x / ρ ≡⟨ cong₂ _/_ (lookup-wk-↑⋆ k x) refl ⟩
173173 var (lift k suc x) / ρ ≡⟨ var-/ ⟩
174174 lookup ρ (lift k suc x) ∎
@@ -194,14 +194,14 @@ record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
194194 wk {n} ↑⋆ k ↑⋆ j ⊙ wk ↑⋆ j ≡
195195 wk ↑⋆ j ⊙ wk ↑⋆ suc k ↑⋆ j
196196 wk-↑⋆-⊙-wk k j = extensionality λ x → begin
197- lookup (wk ↑⋆ k ↑⋆ j ⊙ wk ↑⋆ j) x ≡⟨ lookup-⊙ x ⟩
197+ lookup (wk ↑⋆ k ↑⋆ j ⊙ wk ↑⋆ j) x ≡⟨ lookup-⊙ x {ρ₁ = wk ↑⋆ k ↑⋆ j} ⟩
198198 lookup (wk ↑⋆ k ↑⋆ j) x / wk ↑⋆ j ≡⟨ cong₂ _/_ (lookup-wk-↑⋆-↑⋆ k j x) refl ⟩
199199 var (lift j (lift k suc) x) / wk ↑⋆ j ≡⟨ var-/-wk-↑⋆ j (lift j (lift k suc) x) ⟩
200200 var (lift j suc (lift j (lift k suc) x)) ≡⟨ cong var (lift-commutes k j x) ⟩
201201 var (lift j (lift (suc k) suc) (lift j suc x)) ≡⟨ sym (lookup-wk-↑⋆-↑⋆ (suc k) j (lift j suc x)) ⟩
202202 lookup (wk ↑⋆ suc k ↑⋆ j) (lift j suc x) ≡⟨ sym var-/ ⟩
203203 var (lift j suc x) / wk ↑⋆ suc k ↑⋆ j ≡⟨ cong₂ _/_ (sym (lookup-wk-↑⋆ j x)) refl ⟩
204- lookup (wk ↑⋆ j) x / wk ↑⋆ suc k ↑⋆ j ≡⟨ sym (lookup-⊙ x) ⟩
204+ lookup (wk ↑⋆ j) x / wk ↑⋆ suc k ↑⋆ j ≡⟨ sym (lookup-⊙ x {ρ₁ = wk ↑⋆ j} ) ⟩
205205 lookup (wk ↑⋆ j ⊙ wk ↑⋆ suc k ↑⋆ j) x ∎
206206
207207 open Subst subst public hiding (simple; application)
@@ -341,8 +341,8 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
341341 var (suc x) / ρ ↑ ≡ var x / ρ / wk
342342 suc-/-↑ {ρ = ρ} x = begin
343343 var (suc x) / ρ ↑ ≡⟨ var-/ ⟩
344- lookup (map weaken ρ) x ≡⟨ cong (Fun.flip lookup x) map-weaken ⟩
345- lookup (ρ ⊙ wk) x ≡⟨ lookup-⊙ x ⟩
344+ lookup (map weaken ρ) x ≡⟨ cong (Fun.flip lookup x) ( map-weaken {ρ = ρ}) ⟩
345+ lookup (ρ ⊙ wk) x ≡⟨ lookup-⊙ x {ρ₁ = ρ} ⟩
346346 lookup ρ x / wk ≡⟨ cong₂ _/_ (sym var-/) refl ⟩
347347 var x / ρ / wk ∎
348348
0 commit comments