{-# OPTIONS --safe --without-K #-} module ag-000N where open import MLTT.Spartan hiding (_⊔_; id) open import ag-000M using (Ty; _⇒_; Con; ◇; _▷_) variable Γ Δ Ξ : Con A B C : Ty
引入 Sort 區分 variable 跟 term 的情況
mutual data Sort : 𝓤₀ ̇ where V : Sort T>V : (s : Sort) → IsV s → Sort data IsV : Sort → 𝓤₀ ̇ where isV : IsV V pattern T = T>V V isV variable q r s : Sort
這樣就可以把 variables 跟 terms 定義到一起，用 s 區分
Γ ⊢[ s ] A 是 variable 還是 term
data _⊢[_]_ : Con → Sort → Ty → 𝓤₀ ̇ where here : Γ ▷ A ⊢[ V ] A there : Γ ⊢[ V ] A → (B : Ty) → Γ ▷ B ⊢[ V ] A `_ : Γ ⊢[ V ] A → Γ ⊢[ T ] A _·_ : Γ ⊢[ T ] A ⇒ B → Γ ⊢[ T ] A → Γ ⊢[ T ] B ƛ_ : Γ ▷ A ⊢[ T ] B → Γ ⊢[ T ] A ⇒ B variable x y z : Γ ⊢[ q ] A
substitution 現在定義成
data _⊩[_]_ : Con → Sort → Con → 𝓤₀ ̇ where ε : Γ ⊩[ q ] ◇ _,_ : Γ ⊩[ q ] Δ → Γ ⊢[ q ] A → Γ ⊩[ q ] Δ ▷ A variable xs ys zs : Δ ⊩[ q ] Γ
現在需要考慮 sort 之間的關係，這些 lemma 有助於簡化後面的證明
data _⊑_ : Sort → Sort → Set where rfl : s ⊑ s v⊑t : V ⊑ T _⊔_ : Sort → Sort → Sort V ⊔ r = r T ⊔ r = T
一些輔助用的 REWRITE [ag-000O]
一些輔助用的 REWRITE [ag-000O]
{-# OPTIONS --without-K --rewriting #-} module ag-000O where open import MLTT.Spartan hiding (_⊔_; id) open import ag-000M using (Ty; _⇒_; Con; ◇; _▷_) open import ag-000N {-# BUILTIN REWRITE _＝_ #-}
這邊的定義很繁瑣但只是單純攤開 V、T
就能證明，並不是很重要。重點在最後用 REWRITE
避免後續需要證明一些麻煩的情況
⊑t : s ⊑ T ⊑t {V} = v⊑t ⊑t {T} = rfl v⊑ : V ⊑ s v⊑ {V} = rfl v⊑ {T} = v⊑t ⊑q⊔ : q ⊑ (q ⊔ r) ⊑q⊔ {V}{V} = rfl ⊑q⊔ {V}{T} = v⊑t ⊑q⊔ {T}{V} = rfl ⊑q⊔ {T}{T} = rfl ⊔⊔ : q ⊔ (r ⊔ s) ＝ (q ⊔ r) ⊔ s ⊔⊔ {V}{V}{V} = refl ⊔⊔ {V}{V}{T} = refl ⊔⊔ {V}{T}{V} = refl ⊔⊔ {V}{T}{T} = refl ⊔⊔ {T}{V}{V} = refl ⊔⊔ {T}{V}{T} = refl ⊔⊔ {T}{T}{V} = refl ⊔⊔ {T}{T}{T} = refl ⊔v : q ⊔ V ＝ q ⊔v {V} = refl ⊔v {T} = refl ⊔t : q ⊔ T ＝ T ⊔t {V} = refl ⊔t {T} = refl ⊑⊔r : r ⊑ (q ⊔ r) ⊑⊔r {V}{V} = rfl ⊑⊔r {V}{T} = v⊑t ⊑⊔r {T}{V} = rfl ⊑⊔r {T}{T} = rfl ⊔-self : q ⊔ q ＝ q ⊔-self {V} = refl ⊔-self {T} = refl {-# REWRITE ⊔⊔ ⊔v ⊔t ⊔-self #-}
substitution 的組合 [ag-000P]
substitution 的組合 [ag-000P]
{-# OPTIONS --without-K --rewriting #-} module ag-000P where open import MLTT.Spartan hiding (_⊔_; id) open import ag-000M using (Ty; _⇒_; Con; ◇; _▷_) open import ag-000N open import ag-000O
這裡的目的是定義 ⊑ relation 對 term 的影響，以及定義
substitution 的結合 ◦
tm⊑ : q ⊑ s → Γ ⊢[ q ] A → Γ ⊢[ s ] A tm⊑ rfl x = x tm⊑ v⊑t i = ` i here[_] : (q : Sort) → Γ ▷ A ⊢[ q ] A here[ V ] = here here[ T ] = ` here mutual _[_] : Γ ⊢[ q ] A → Δ ⊩[ r ] Γ → Δ ⊢[ q ⊔ r ] A here [ xs , x ] = x there i _ [ xs , x ] = i [ xs ] (` i) [ xs ] = tm⊑ ⊑t (i [ xs ]) (t · u) [ xs ] = (t [ xs ]) · (u [ xs ]) (ƛ t) [ xs ] = ƛ (t [ xs ↑ _ ]) id-poly : (q : Sort) → Γ ⊩[ q ] Γ id-poly {Γ = ◇} q = ε id-poly {Γ = Γ ▷ A} q = id-poly q ↑ A id : Γ ⊩[ V ] Γ id = id-poly V {-# INLINE id #-} there[_] : (q : Sort) → Γ ⊢[ q ] B → (A : Ty) → Γ ▷ A ⊢[ q ] B there[ V ] i A = there i A there[ T ] t A = t [ id ⁺ A ] _⁺_ : Γ ⊩[ q ] Δ → (A : Ty) → Γ ▷ A ⊩[ q ] Δ ε ⁺ A = ε (ts , t) ⁺ A = (ts ⁺ A) , there[ _ ] t A _↑_ : Γ ⊩[ q ] Δ → (A : Ty) → Γ ▷ A ⊩[ q ] Δ ▷ A ts ↑ A = ts ⁺ A , here[ _ ] infixl 70 _⁺_ _◦_ : Γ ⊩[ q ] Ξ → Δ ⊩[ r ] Γ → Δ ⊩[ q ⊔ r ] Ξ ε ◦ ys = ε (xs , x) ◦ ys = (xs ◦ ys) , x [ ys ]
Proposition. The right identity law [ag-000Q]
Proposition. The right identity law [ag-000Q]
{-# OPTIONS --without-K --rewriting #-} module ag-000Q where open import MLTT.Spartan hiding (_⊔_; id) open import ag-000M using (Ty; _⇒_; Con; ◇; _▷_) open import ag-000N open import ag-000O open import ag-000P
⁺-nat[]v : (i : Γ ⊢[ V ] A) → (xs : Δ ⊩[ q ] Γ) → i [ xs ⁺ B ] ＝ there[ q ] (i [ xs ]) B ⁺-nat[]v here (xs , x) = refl ⁺-nat[]v (there j _) (xs , x) = ⁺-nat[]v j xs [id] : x [ id ] ＝ x [id] {x = here} = refl [id] {x = there i B} = (i [ id ⁺ B ]) ＝⟨ ⁺-nat[]v {q = V} i id ⟩ there (i [ id ]) B ＝⟨ ap (λ - → there - B) [id] ⟩ there i B ∎ [id] {x = ` i} = ap `_ [id] [id] {x = t · u} = ((t [ id ]) · (u [ id ])) ＝⟨ ap (t [ id ] ·_) [id] ⟩ ((t [ id ]) · u) ＝⟨ ap (_· u) [id] ⟩ (t · u) ∎ [id] {x = ƛ t} = ap ƛ_ [id] ◦id : xs ◦ id ＝ xs ◦id {xs = ε} = refl ◦id {xs = xs , x} = (xs ◦ id) , (x [ id ]) ＝⟨ ap ((xs ◦ id) ,_) [id] ⟩ (xs ◦ id) , x ＝⟨ ap (_, x) ◦id ⟩ xs , x ∎
Proposition. Left identity law 與 Associative law [ag-000R]
Proposition. Left identity law 與 Associative law [ag-000R]
{-# OPTIONS --allow-unsolved-metas --without-K --rewriting #-} module ag-000R where open import MLTT.Spartan hiding (_⊔_; id) open import ag-000M using (Ty; _⇒_; Con; ◇; _▷_) open import ag-000N open import ag-000O open import ag-000P open import ag-000Q
這兩個是 mutual 定義的，而且有一些 goals 我也看不出怎麼解了，暫時就先這樣 xd
tm[] : tm⊑ ⊑t (x [ xs ]) ＝ (tm⊑ ⊑t x) [ xs ] tm[] {x = here} = refl tm[] {x = there x B} = refl tm[] {x = ` x} = tm[] {x = x} tm[] {x = x · x₁} = refl tm[] {x = ƛ x} = refl zero[] : {q : Sort} {r : Sort} {Γ : Con} {Δ : Con} {A : Ty} {xs : Δ ⊩[ r ] Γ} {x : Δ ⊢[ r ] A} → here[ q ] [ xs , x ] ＝ tm⊑ (⊑⊔r {q = q}) x zero[] {q = V} {r = V} = refl zero[] {q = V} {r = T} = refl zero[] {q = T} {r = V} = refl zero[] {q = T} {r = T} = refl tm⊑zero : (q⊑r : q ⊑ r) → here[ r ] ＝ tm⊑ q⊑r here[ q ] tm⊑zero rfl = refl tm⊑zero v⊑t = refl {-# TERMINATING #-} mutual suc[] : (there[ s ] x _) [ ys , y ] ＝ x [ ys ] suc[] {s = V} = refl suc[] {s = T} {x = x} {ys = ys} {y = y} = there[ T ] x _ [ ys , y ] ＝⟨ refl ⟩ x [ id ⁺ _ ] [ ys , y ] ＝⟨ [◦] {x = x} ⁻¹ ⟩ x [ (id ⁺ _) ◦ (ys , y) ] ＝⟨ ap (x [_]) ⁺◦ ⟩ x [ id ◦ ys ] ＝⟨ ap (x [_]) id◦ ⟩ x [ ys ] ∎ ⁺◦ : xs ⁺ A ◦ (ys , x) ＝ xs ◦ ys ⁺◦ {xs = ε} = refl ⁺◦ {xs = ts , t} {A = A} {ys = ys} {x = x} = ((ts ⁺ A) ◦ (ys , x)) , (there[ _ ] t A [ ys , x ]) ＝⟨ ap (((ts ⁺ A) ◦ (ys , x)) ,_) (suc[] {x = t}) ⟩ ((ts ⁺ A) ◦ (ys , x)) , (t [ ys ]) ＝⟨ ap (_, (t [ ys ])) ⁺◦ ⟩ (ts ◦ ys) , (t [ ys ]) ∎ ⁺−nat◦ : {xs : Δ ⊩[ q ] Γ} → {ys : Ξ ⊩[ r ] Δ} → {A : Ty} → xs ◦ (ys ⁺ A) ＝ (xs ◦ ys) ⁺ A ⁺−nat◦ {xs = ε} = refl ⁺−nat◦ {q = q} {r = r} {xs = xs , x} {ys = ys} {A = A} = (xs ◦ (ys ⁺ A)) , (x [ ys ⁺ A ]) ＝⟨ ap ((xs ◦ (ys ⁺ A)) ,_) (⁺-nat[] {q = q} {B = A} {x = x} {xs = ys}) ⟩ (xs ◦ (ys ⁺ A)) , there[ _ ] (x [ ys ]) A ＝⟨ ap (_, there[ _ ] (x [ ys ]) A) ⁺−nat◦ ⟩ ((xs ◦ ys) ⁺ A) , there[ _ ] (x [ ys ]) A ∎ ⁺-nat[] : {q r : Sort} → {A B : Ty} → {x : Γ ⊢[ q ] A} → {xs : Δ ⊩[ r ] Γ} → x [ xs ⁺ B ] ＝ there[ q ⊔ r ] (x [ xs ]) B ⁺-nat[] {q = V} {x = i} {xs = xs} = ⁺-nat[]v i xs ⁺-nat[] {q = T} {B = B} {x = x} {xs = xs} = x [ xs ⁺ B ] ＝⟨ ap (λ - → x [ - ⁺ B ]) (◦id {xs = xs} ⁻¹) ⟩ x [ (xs ◦ id) ⁺ B ] ＝⟨ ap (x [_]) (⁺−nat◦ ⁻¹) ⟩ x [ xs ◦ (id ⁺ B) ] ＝⟨ [◦] {x = x} ⟩ x [ xs ] [ id ⁺ B ] ＝⟨ refl ⟩ there[ T ] (x [ xs ]) B ∎ ↑◦ : {r s : Sort} → {xs : Δ ⊩[ r ] Ξ} → {ys : Γ ⊩[ s ] Δ} → {A : Ty} → (xs ◦ ys) ↑ A ＝ (xs ↑ A) ◦ (ys ↑ A) ↑◦ {r = r} {s = s} {xs = xs} {ys = ys} {A = A} = (xs ◦ ys) ↑ A ＝⟨ refl ⟩ (xs ◦ ys) ⁺ A , here[ r ⊔ s ] ＝⟨ ap (λ - → - , here[ _ ]) (⁺−nat◦ ⁻¹) ⟩ xs ◦ (ys ⁺ A) , here[ r ⊔ s ] ＝⟨ ap (xs ◦ (ys ⁺ A) ,_) (tm⊑zero (⊑⊔r {r = s} {q = r})) ⟩ xs ◦ (ys ⁺ A) , tm⊑ (⊑⊔r {q = r}) here[ s ] ＝⟨ ap (xs ◦ (ys ⁺ A) ,_) (zero[] {q = r} {r = s} {A = A} {xs = ys ⁺ A} {x = here[ s ]} ⁻¹) ⟩ xs ◦ (ys ⁺ A) , (here[ r ] [ ys ↑ A ]) ＝⟨ ap (_, (here[ r ] [ ys ↑ A ])) (⁺◦ {xs = xs} {A = A} {ys = ys ⁺ A} {x = here[ s ]} ⁻¹) ⟩ ((xs ⁺ A) ◦ (ys ⁺ A , here[ s ])) , (here[ r ] [ ys ↑ A ]) ＝⟨ refl ⟩ (xs ↑ A) ◦ (ys ↑ A)∎ [◦] : x [ xs ◦ ys ] ＝ x [ xs ] [ ys ] [◦] {x = here} {xs = xs , x} = refl [◦] {x = there i B} {xs = xs , x} = [◦] {x = i} [◦] {x = ` x} {xs = xs} {ys = ys} = tm⊑ ⊑t (x [ xs ◦ ys ]) ＝⟨ ap (λ - → tm⊑ ⊑t -) ([◦] {x = x}) ⟩ tm⊑ ⊑t (x [ xs ] [ ys ]) ＝⟨ tm[] {x = x [ xs ]} ⟩ (tm⊑ ⊑t (x [ xs ]) [ ys ]) ∎ [◦] {x = t · u} {xs = xs} {ys = ys} = (t [ xs ◦ ys ]) · (u [ xs ◦ ys ]) ＝⟨ ap (_· (u [ xs ◦ ys ])) ([◦] {x = t}) ⟩ (t [ xs ] [ ys ]) · (u [ xs ◦ ys ]) ＝⟨ ap ((t [ xs ] [ ys ]) ·_) ([◦] {x = u}) ⟩ ((t [ xs ]) [ ys ]) · ((u [ xs ]) [ ys ]) ∎ [◦] {x = ƛ t} {xs = xs} {ys = ys} = ap ƛ_ (t [ (xs ◦ ys) ↑ _ ] ＝⟨ ap (t [_]) (↑◦ {xs = xs}) ⟩ t [ (xs ↑ _) ◦ (ys ↑ _) ] ＝⟨ [◦] {x = t} ⟩ (t [ xs ↑ _ ]) [ ys ↑ _ ] ∎) id◦' : Sort → id ◦ xs ＝ xs id◦' {xs = ε} q = refl id◦' {xs = xs , x} q = ap (_, x) (((id ⁺ _) ◦ (xs , x)) ＝⟨ ⁺◦ ⟩ id ◦ xs ＝⟨ id◦ ⟩ xs ∎) id◦ : id ◦ xs ＝ xs id◦ = id◦' V {-# INLINE id◦ #-}
到這裡已經證明了 contexts 與 substitutions 真的是一個範疇，而且這個範疇有 terminal object。第五節是把這邊的工作放進去 CwF-simple（constant presheaves 可以讓 CwF 適用於 simply typed calculus）裡，那個我暫時沒什麼興趣。