{-# 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 ]