substitution 的組合

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

substitution 的組合 [ag-000P]