{-# 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◦ #-}