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

{-# 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  _⁺_

_◦_ : Γ ⊩[ q ] Ξ → Δ ⊩[ r ] Γ → Δ ⊩[ q ⊔ r ] Ξ
ε ◦ ys = ε
(xs , x) ◦ ys = (xs ◦ ys) , x [ ys ]

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

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