{-# OPTIONS --without-K --safe #-}
module NonCumulative.Statics.Ascribed.Properties where
open import Lib
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary using (PartialSetoid; IsPartialEquivalence)
import Relation.Binary.Reasoning.PartialSetoid as PS
open import NonCumulative.Statics.Ascribed.Full
import NonCumulative.Statics.Ascribed.Presup as Presup
import NonCumulative.Statics.Ascribed.Refl as Refl
import NonCumulative.Statics.Ascribed.Misc as Misc
import NonCumulative.Statics.Ascribed.PER as PER
import NonCumulative.Statics.Ascribed.CtxEquiv as CtxEquiv
import NonCumulative.Statics.Ascribed.Properties.Contexts as Ctxₚ
import NonCumulative.Statics.Ascribed.Properties.Subst as Subₚ
open Misc
using ( _[wk]*_)
public
⊢≈-refl : ⊢ Γ →
⊢ Γ ≈ Γ
⊢≈-refl ⊢Γ = (Refl.≈-Ctx-refl ⊢Γ)
⊢≈-trans : ⊢ Γ ≈ Γ′ → ⊢ Γ′ ≈ Γ″ → ⊢ Γ ≈ Γ″
⊢≈-trans ⊢Γ≈Γ′ ⊢Γ′≈Γ′′ = PER.⊢≈-trans ⊢Γ≈Γ′ ⊢Γ′≈Γ′′
[]-cong-Se‴ : ∀ {i} → Δ ⊢ T ∶[ 1 + i ] Se i → Γ ⊢s σ ≈ σ′ ∶ Δ → Γ ⊢ T [ σ ] ≈ T [ σ′ ] ∶[ 1 + i ] Se i
[]-cong-Se‴ ⊢T σ≈σ′ = Misc.[]-cong-Se″ ⊢T (proj₁ (proj₂ (Presup.presup-s-≈ σ≈σ′))) σ≈σ′
no-closed-Ne-gen : ∀ {i} →
Γ ⊢ t ∶[ i ] T →
Γ ≡ [] →
¬ (t ≡ Ne⇒Exp u)
no-closed-Ne-gen {_} {_} {_} {rec T z s u} {_} (N-E _ _ _ ⊢u) refl refl = no-closed-Ne-gen ⊢u refl refl
no-closed-Ne-gen {_} {_} {_} {u $ n} {_} (Λ-E _ _ ⊢u _ _) refl refl = no-closed-Ne-gen ⊢u refl refl
no-closed-Ne-gen {_} {_} {_} {unlift u} {_} (L-E _ _ ⊢u) refl refl = no-closed-Ne-gen ⊢u refl refl
no-closed-Ne-gen {_} {_} {_} {_} (conv ⊢u _) refl refl = no-closed-Ne-gen ⊢u refl refl
no-closed-Ne : ∀ {i} → ¬ ([] ⊢ Ne⇒Exp u ∶[ i ] T)
no-closed-Ne ⊢u = no-closed-Ne-gen ⊢u refl refl
⊢I-inv : Γ ⊢s I ∶ Δ → ⊢ Γ ≈ Δ
⊢I-inv (s-I ⊢Γ) = ⊢≈-refl ⊢Γ
⊢I-inv (s-conv ⊢I Δ′≈Δ) = ⊢≈-trans (⊢I-inv ⊢I) Δ′≈Δ
[I]-inv : ∀ { i } → Γ ⊢ t [ I ] ∶[ i ] T → Γ ⊢ t ∶[ i ] T
[I]-inv (t[σ] ⊢t[I] ⊢sI) with ⊢t ← CtxEquiv.ctxeq-tm (Ctxₚ.⊢≈-sym (⊢I-inv ⊢sI)) ⊢t[I] = conv ⊢t (≈-sym ([I] (proj₂ (Presup.presup-tm ⊢t))))
[I]-inv (conv ⊢t[I] S≈T) = conv ([I]-inv ⊢t[I]) S≈T
[I]-≈ˡ : ∀ {i} → Γ ⊢ t [ I ] ≈ s ∶[ i ] T [ I ] →
Γ ⊢ t ≈ s ∶[ i ] T
[I]-≈ˡ ≈s
with _ , ⊢t[I] , _ , ⊢T[I] ← Presup.presup-≈ ≈s = ≈-conv (≈-trans (≈-sym ([I] ⊢t)) ≈s) ([I] ⊢T)
where ⊢t = [I]-inv ⊢t[I]
⊢T = [I]-inv ⊢T[I]
[I]-≈ˡ-Se : ∀ {i} →
Γ ⊢ T [ I ] ≈ S ∶[ 1 + i ] Se i →
Γ ⊢ T ≈ S ∶[ 1 + i ] Se i
[I]-≈ˡ-Se ≈S
with _ , ⊢T[I] , _ ← Presup.presup-≈ ≈S = ≈-trans (≈-sym ([I] ⊢T)) ≈S
where ⊢T = [I]-inv ⊢T[I]
∘I-inv : Γ ⊢s σ ∘ I ∶ Δ → ∃ λ Δ′ → Γ ⊢s σ ∶ Δ′ × ⊢ Δ ≈ Δ′
∘I-inv (s-∘ ⊢I ⊢σ) = -, CtxEquiv.ctxeq-s (Ctxₚ.⊢≈-sym (⊢I-inv ⊢I)) ⊢σ , ⊢≈-refl (proj₂ (Presup.presup-s ⊢σ))
∘I-inv (s-conv ⊢σI Δ″≈Δ)
with Δ′ , ⊢σ , Δ″≈Δ′ ← ∘I-inv ⊢σI = -, ⊢σ , ⊢≈-trans (Ctxₚ.⊢≈-sym Δ″≈Δ) Δ″≈Δ′
∘I-inv′ : Γ ⊢s σ ∘ I ∶ Δ → Γ ⊢s σ ∶ Δ
∘I-inv′ ⊢σI
with _ , ⊢σ , Δ′≈Δ ← ∘I-inv ⊢σI = s-conv ⊢σ (Ctxₚ.⊢≈-sym Δ′≈Δ)
∷-cong″ : ∀ {i} → Γ ⊢ T ≈ T′ ∶[ 1 + i ] Se i → ⊢ (T ↙ i) ∷ Γ ≈ (T′ ↙ i) ∷ Γ
∷-cong″ T≈T′
with ⊢Γ , ⊢T , ⊢T′ , _ ← Presup.presup-≈ T≈T′ = Refl.∷-cong′ ⊢Γ ⊢T ⊢T′ T≈T′
[∘]-N : Δ ⊢ t ∶[ 0 ] N → Γ ⊢s σ ∶ Δ → Γ′ ⊢s τ ∶ Γ → Γ′ ⊢ t [ σ ] [ τ ] ≈ t [ σ ∘ τ ] ∶[ 0 ] N
[∘]-N ⊢t ⊢σ ⊢τ = ≈-conv (≈-sym ([∘] ⊢τ ⊢σ ⊢t)) (N-[] (s-∘ ⊢τ ⊢σ))
Exp≈-isPER : ∀ {i} → IsPartialEquivalence (Γ ⊢_≈_∶[ i ] T)
Exp≈-isPER {Γ} {T} = record
{ sym = ≈-sym
; trans = ≈-trans
}
Exp≈-PER : ∀ {i} → Ctx → Typ → PartialSetoid _ _
Exp≈-PER {i} Γ T = record
{ Carrier = Exp
; _≈_ = Γ ⊢_≈_∶[ i ] T
; isPartialEquivalence = Exp≈-isPER
}
module ER {i Γ T} = PS (Exp≈-PER {i} Γ T)
Substs≈-isPER : IsPartialEquivalence (Γ ⊢s_≈_∶ Δ)
Substs≈-isPER = record
{ sym = s-≈-sym
; trans = s-≈-trans
}
Substs≈-PER : Ctx → Ctx → PartialSetoid _ _
Substs≈-PER Γ Δ = record
{ Carrier = Subst
; _≈_ = Γ ⊢s_≈_∶ Δ
; isPartialEquivalence = Substs≈-isPER
}
module SR {Γ Δ} = PS (Substs≈-PER Γ Δ)
q-cong : ∀ {i} → Γ ⊢s σ ≈ σ′ ∶ Δ → Δ ⊢ T ∶[ 1 + i ] Se i → (T [ σ ] ↙ i) ∷ Γ ⊢s q (T ↙ i) σ ≈ q (T ↙ i) σ′ ∶ (T ↙ i) ∷ Δ
q-cong {_} {σ} {σ′} {_} {T} σ≈σ′ ⊢T
with ⊢Γ , ⊢σ , _ ← Presup.presup-s-≈ σ≈σ′ = ,-cong (∘-cong (wk-≈ ⊢TσΓ) σ≈σ′) ⊢T (Refl.≈-refl ⊢T) (Refl.≈-refl (conv (vlookup ⊢TσΓ here) (Misc.[∘]-Se ⊢T ⊢σ (s-wk ⊢TσΓ))))
where open ER
⊢Tσ = Misc.t[σ]-Se ⊢T ⊢σ
⊢TσΓ = ⊢∷ ⊢Γ ⊢Tσ
[]-q-∘-, : ∀ {i j} → (S ↙ i) ∷ Γ ⊢ T ∶[ 1 + j ] Se j → Δ ⊢s σ ∶ Γ → Δ′ ⊢s τ ∶ Δ → Δ′ ⊢ t ∶[ i ] S [ σ ] [ τ ] →
Δ′ ⊢ T [ (σ ∘ τ) , t ∶ (S ↙ i) ] ≈ T [ q (S ↙ i) σ ] [ τ , t ∶ (sub S σ ↙ i) ] ∶[ 1 + j ] Se j
[]-q-∘-, {S} {T = T} {σ = σ} {τ = τ} {t = t} {i = i} {j} ⊢T ⊢σ ⊢τ ⊢t
with ⊢∷ ⊢Γ ⊢S ← proj₁ (Presup.presup-tm ⊢T)
| ⊢Δ′ , ⊢Δ ← Presup.presup-s ⊢τ = begin
T [ (σ ∘ τ) , t ∶ (S ↙ i) ] ≈⟨ []-cong-Se‴ ⊢T
(,-cong (s-≈-trans (∘-cong (s-≈-sym (p-, ⊢τ ⊢Sσ ⊢t)) (Refl.s-≈-refl ⊢σ))
(s-≈-sym (∘-assoc ⊢σ
(s-wk ⊢SσΔ)
(s-, ⊢τ ⊢Sσ ⊢t)))) ⊢S (Refl.≈-refl ⊢S) (≈-conv (≈-sym ([,]-v-ze ⊢τ ⊢Sσ ⊢t)) (Misc.[∘]-Se ⊢S ⊢σ ⊢τ) )) ⟩
T [ (σ ∘ wk ∘ τ , t ∶ (sub S σ ↙ i)) , v 0 [ τ , t ∶ (sub S σ ↙ i) ] ∶ (S ↙ i) ] ≈˘⟨ []-cong-Se‴ ⊢T
(,-∘ (s-∘ (s-wk ⊢SσΔ) ⊢σ) ⊢S (conv (vlookup ⊢SσΔ here) (Misc.[∘]-Se ⊢S ⊢σ (s-wk ⊢SσΔ))) (s-, ⊢τ ⊢Sσ ⊢t)) ⟩
T [ q (S ↙ i) σ ∘ (τ , t ∶ (sub S σ ↙ i)) ] ≈˘⟨ Misc.[∘]-Se ⊢T ⊢qσ ⊢τ,t ⟩
T [ q (S ↙ i) σ ] [ τ , t ∶ (sub S σ ↙ i) ] ∎
where open ER
⊢qσ = Misc.⊢q ⊢Δ ⊢σ ⊢S
⊢Sσ = Misc.t[σ]-Se ⊢S ⊢σ
⊢τ,t = s-, ⊢τ ⊢Sσ ⊢t
⊢SσΔ = ⊢∷ ⊢Δ ⊢Sσ
[]-q-∘-,′ : ∀ {i j} → (S ↙ j) ∷ Γ ⊢ T ∶[ 1 + i ] Se i → Δ ⊢s σ ∶ Γ → Δ ⊢ t ∶[ j ] S [ σ ] → Δ ⊢ T [ σ , t ∶ (S ↙ j) ] ≈ T [ q (S ↙ j) σ ] [| t ∶ (sub S σ ↙ j) ] ∶[ 1 + i ] Se i
[]-q-∘-,′ ⊢T ⊢σ ⊢t
with ⊢∷ ⊢Γ ⊢S ← proj₁ (Presup.presup-tm ⊢T)
| ⊢Δ , ⊢Γ ← Presup.presup-s ⊢σ = ≈-trans ([]-cong-Se‴ ⊢T (,-cong (s-≈-sym (∘-I ⊢σ)) ⊢S (Refl.≈-refl ⊢S) (Refl.≈-refl ⊢t)))
([]-q-∘-, ⊢T ⊢σ (s-I ⊢Δ) (conv ⊢t (≈-sym ([I] ⊢Sσ))))
where ⊢qσ = Misc.⊢q ⊢Δ ⊢σ ⊢S
⊢Sσ = Misc.t[σ]-Se ⊢S ⊢σ
[]-,-∘ : ∀ {i j} → (T ↙ i) ∷ Γ ⊢ S ∶[ 1 + j ] Se j → Δ ⊢s σ ∶ Γ → Δ ⊢ t ∶[ i ] T [ σ ] → Δ′ ⊢s τ ∶ Δ → Δ′ ⊢ S [ σ , t ∶ T ↙ i ] [ τ ] ≈ S [ (σ ∘ τ) , t [ τ ] ∶ T ↙ i ] ∶[ 1 + j ] Se j
[]-,-∘ {T} {S = S} {σ = σ} {t} {τ = τ} {i = i} {j} ⊢S ⊢σ ⊢t ⊢τ
with ⊢∷ ⊢Γ ⊢T ← proj₁ (Presup.presup-tm ⊢S) = begin
S [ σ , t ∶ T ↙ i ] [ τ ] ≈⟨ Misc.[∘]-Se ⊢S ⊢σ,t ⊢τ ⟩
S [ σ , t ∶ T ↙ i ∘ τ ] ≈⟨ []-cong-Se‴ ⊢S (,-∘ ⊢σ ⊢T ⊢t ⊢τ) ⟩
S [ (σ ∘ τ) , t [ τ ] ∶ T ↙ i ] ∎
where
open ER
⊢σ,t = s-, ⊢σ ⊢T ⊢t
I,∘≈, : ∀ {i} → Δ ⊢s σ ∶ Γ → Γ ⊢ T ∶[ 1 + i ] Se i → Γ ⊢ t ∶[ i ] T → Δ ⊢s (I , t ∶ T ↙ i) ∘ σ ≈ σ , t [ σ ] ∶ T ↙ i ∶ (T ↙ i) ∷ Γ
I,∘≈, ⊢σ ⊢T ⊢t = Subₚ.[I,t]∘σ≈σ,t[σ] (⊢∷ (proj₁ (Presup.presup-tm ⊢t)) ⊢T) ⊢σ ⊢t
[]-I,-∘ : ∀ {i j} → (T ↙ i) ∷ Γ ⊢ S ∶[ 1 + j ] Se j → Δ ⊢s σ ∶ Γ → Γ ⊢ t ∶[ i ] T → Δ ⊢ S [| t ∶ T ↙ i ] [ σ ] ≈ S [ σ , t [ σ ] ∶ T ↙ i ] ∶[ 1 + j ] Se j
[]-I,-∘ {T = T} {S = S} {σ = σ} {t = t} {i = i} {j = j} ⊢S ⊢σ ⊢t
with ⊢∷ ⊢Γ ⊢T ← proj₁ (Presup.presup-tm ⊢S) = begin
S [| t ∶ T ↙ i ] [ σ ] ≈⟨ Misc.[∘]-Se ⊢S ⊢I,t ⊢σ ⟩
S [ (I , t ∶ T ↙ i) ∘ σ ] ≈⟨ []-cong-Se‴ ⊢S (I,∘≈, ⊢σ ⊢T ⊢t) ⟩
S [ σ , t [ σ ] ∶ T ↙ i ]
∎
where open ER
⊢I,t = Misc.⊢I,t ⊢Γ ⊢T ⊢t
[]-I,ze-∘ : ∀ {i} → (N ↙ 0) ∷ Γ ⊢ S ∶[ 1 + i ] Se i → Δ ⊢s σ ∶ Γ → Δ ⊢ S [| ze ∶ N ↙ 0 ] [ σ ] ≈ S [ σ , ze ∶ N ↙ 0 ] ∶[ 1 + i ] Se i
[]-I,ze-∘ {_} {S} {_} {σ} ⊢S ⊢σ
with ⊢∷ ⊢Γ ⊢T ← proj₁ (Presup.presup-tm ⊢S) =
begin
S [| ze ∶ N ↙ 0 ] [ σ ] ≈⟨ Misc.[∘]-Se ⊢S I,t ⊢σ ⟩
S [ (I , ze ∶ N ↙ 0 ) ∘ σ ] ≈⟨ []-cong-Se‴ ⊢S (Subₚ.[I,ze]∘σ≈σ,ze ⊢Γ ⊢σ) ⟩
S [ σ , ze ∶ N ↙ 0 ] ∎
where open ER
I,t = Misc.⊢I,t ⊢Γ (N-wf ⊢Γ) (ze-I ⊢Γ)
p-∘ : ∀ {i} → Γ ⊢s σ ∶ (T ↙ i) ∷ Δ →
Γ′ ⊢s τ ∶ Γ →
Γ′ ⊢s p (σ ∘ τ) ≈ p σ ∘ τ ∶ Δ
p-∘ ⊢σ ⊢τ = s-≈-sym (∘-assoc (s-wk (proj₂ (Presup.presup-s ⊢σ))) ⊢σ ⊢τ)
module _ {i} {j : ℕ} (⊢σ : Γ ⊢s σ ∶ Δ)
(⊢T : Δ ⊢ T ∶[ 1 + i ] Se i)
(⊢τ : Δ′ ⊢s τ ∶ Γ)
(⊢t : Δ′ ⊢ t ∶[ i ] T [ σ ] [ τ ]) where
private
⊢Γ = proj₁ (Presup.presup-s ⊢σ)
⊢Tσ = Misc.t[σ]-Se ⊢T ⊢σ
⊢TσΓ = ⊢∷ ⊢Γ ⊢Tσ
⊢wk = s-wk ⊢TσΓ
⊢σwk = s-∘ ⊢wk ⊢σ
⊢qσ = Misc.⊢q ⊢Γ ⊢σ ⊢T
⊢τ,t = s-, ⊢τ ⊢Tσ ⊢t
eq = begin
σ ∘ wk ∘ (τ , t ∶ T [ σ ] ↙ i) ≈⟨ ∘-assoc ⊢σ ⊢wk ⊢τ,t ⟩
σ ∘ (wk ∘ (τ , t ∶ T [ σ ] ↙ i)) ≈⟨ ∘-cong (p-, ⊢τ ⊢Tσ ⊢t) (Refl.s-≈-refl ⊢σ) ⟩
σ ∘ τ ∎
where open SR
q∘,≈∘, : Δ′ ⊢s q (T ↙ i) σ ∘ (τ , t ∶ T [ σ ] ↙ i) ≈ (σ ∘ τ) , t ∶ T ↙ i ∶ (T ↙ i) ∷ Δ
q∘,≈∘, = begin
q (T ↙ i) σ ∘ (τ , t ∶ T [ σ ] ↙ i) ≈⟨ ,-∘ ⊢σwk ⊢T (conv (vlookup ⊢TσΓ here) (Misc.[∘]-Se ⊢T ⊢σ ⊢wk)) ⊢τ,t ⟩
(σ ∘ wk ∘ (τ , t ∶ T [ σ ] ↙ i)) , v 0 [ τ , t ∶ T [ σ ] ↙ i ] ∶ T ↙ i ≈⟨ ,-cong eq ⊢T (Refl.≈-refl ⊢T) (≈-conv ([,]-v-ze ⊢τ ⊢Tσ ⊢t)
( ≈-trans (Misc.[∘]-Se ⊢T ⊢σ ⊢τ) (≈-sym ([]-cong-Se‴ ⊢T eq)) )) ⟩
(σ ∘ τ) , t ∶ T ↙ i
∎
where open SR
[]-q-, : (T ↙ i) ∷ Δ ⊢ s ∶[ j ] S →
Δ′ ⊢ s [ q (T ↙ i) σ ] [ τ , t ∶ T [ σ ] ↙ i ] ≈ s [ (σ ∘ τ) , t ∶ T ↙ i ] ∶[ j ] S [ (σ ∘ τ) , t ∶ T ↙ i ]
[]-q-, {s} ⊢s
with _ , ⊢S ← Presup.presup-tm ⊢s = begin
s [ q (T ↙ i) σ ] [ τ , t ∶ T [ σ ] ↙ i ] ≈˘⟨ ≈-conv ([∘] ⊢τ,t ⊢qσ ⊢s) ([]-cong-Se‴ ⊢S q∘,≈∘,) ⟩
s [ (q (T ↙ i) σ) ∘ ( τ , t ∶ T [ σ ] ↙ i) ] ≈⟨ ≈-conv ([]-cong (Refl.≈-refl ⊢s) q∘,≈∘,) ([]-cong-Se‴ ⊢S q∘,≈∘,) ⟩
s [ (σ ∘ τ) , t ∶ T ↙ i ]
∎
where open ER
module _ (⊢σ : Δ ⊢s σ ∶ Γ) (⊢τ : Δ′ ⊢s τ ∶ Δ) where
private
⊢Δ = proj₁ (Presup.presup-s ⊢σ)
⊢Γ = proj₂ (Presup.presup-s ⊢σ)
⊢Δ′ = proj₁ (Presup.presup-s ⊢τ)
⊢τσ = s-∘ ⊢τ ⊢σ
q∘q : ∀ {i} → Γ ⊢ T ∶[ 1 + i ] Se i → (T [ σ ∘ τ ] ↙ i) ∷ Δ′ ⊢s q (T ↙ i) σ ∘ q ( T [ σ ] ↙ i ) τ ≈ q (T ↙ i) (σ ∘ τ) ∶ (T ↙ i) ∷ Γ
q∘q {T} {i} ⊢T = begin
q (T ↙ i) σ ∘ q ( T [ σ ] ↙ i ) τ ≈⟨ q∘,≈∘, {j = 0} ⊢σ ⊢T (s-∘ ⊢wk ⊢τ) ⊢v0 ⟩
(σ ∘ (τ ∘ wk)) , v 0 ∶ T ↙ i ≈⟨ ,-cong (s-≈-sym στwk≈) ⊢T (Refl.≈-refl ⊢T)
(Refl.≈-refl (conv (vlookup ⊢Δ′T[στ] here)
T[στ]wk≈T[στwk])) ⟩
q (T ↙ i) (σ ∘ τ)
∎
where
open SR
Δ′⊢T[στ] = Misc.t[σ]-Se ⊢T ⊢τσ
⊢Δ′T[στ] = ⊢∷ ⊢Δ′ Δ′⊢T[στ]
⊢wk = s-wk ⊢Δ′T[στ]
στwk≈ = ∘-assoc ⊢σ ⊢τ ⊢wk
T[στ]wk≈T[στwk] = ≈-trans (Misc.[∘]-Se ⊢T ⊢τσ ⊢wk) ([]-cong-Se‴ ⊢T στwk≈)
⊢v0 = conv (vlookup ⊢Δ′T[στ] here)
(≈-trans T[στ]wk≈T[στwk] (≈-sym (Misc.[∘]-Se ⊢T ⊢σ (s-∘ ⊢wk ⊢τ))))
q∘q-N : N₀ ∷ Δ′ ⊢s q N₀ σ ∘ q N₀ τ ≈ q N₀ (σ ∘ τ) ∶ N₀ ∷ Γ
q∘q-N = begin
q N₀ σ ∘ q N₀ τ ≈⟨ ∘-cong (,-cong (Refl.s-≈-refl ⊢τwk) Δ⊢N ≈N (Refl.≈-refl (conv (vlookup ⊢NΔ′ here) (≈-trans (N-[] ⊢wk′) (≈-sym (N-[] ⊢τwk))))))
(Refl.s-≈-refl (s-, ⊢σwk Γ⊢N (conv (vlookup ⊢NΔ here) (≈-trans (N-[] ⊢wk) (≈-sym (N-[] ⊢σwk)))))) ⟩
q N₀ σ ∘ q (N [ σ ] ↙ 0) τ ≈⟨ s-≈-conv (CtxEquiv.ctxeq-s-≈ (∷-cong″ (N-[] ⊢τσ)) (q∘q Γ⊢N)) (⊢≈-refl (⊢∷ ⊢Γ Γ⊢N)) ⟩
q N₀ (σ ∘ τ)
∎
where
open SR
Γ⊢N = N-wf ⊢Γ
Δ⊢N = N-wf ⊢Δ
≈N = ≈-sym (N-[] ⊢σ)
⊢NΔ = ⊢∷ ⊢Δ (N-wf ⊢Δ)
⊢NΔ′ = ⊢∷ ⊢Δ′ (N-wf ⊢Δ′)
⊢wk = s-wk ⊢NΔ
⊢wk′ = s-wk ⊢NΔ′
⊢σwk = s-∘ ⊢wk ⊢σ
⊢τwk = s-∘ ⊢wk′ ⊢τ
module NatTyping {i} (⊢T : (N ↙ 0) ∷ Γ ⊢ T ∶[ 1 + i ] Se i) (⊢σ : Δ ⊢s σ ∶ Γ) where
⊢Δ = proj₁ (Presup.presup-s ⊢σ)
⊢Γ = proj₂ (Presup.presup-s ⊢σ)
⊢qσ = Misc.⊢q-N ⊢Δ ⊢Γ ⊢σ
Γ⊢N = N-wf ⊢Γ
Δ⊢N = N-wf ⊢Δ
⊢qqσ = Misc.⊢q (⊢∷ ⊢Δ Δ⊢N) ⊢qσ ⊢T
⊢Tqσ = Misc.t[σ]-Se ⊢T ⊢qσ
⊢NΓ = ⊢∷ ⊢Γ Γ⊢N
⊢TNΓ = ⊢∷ ⊢NΓ ⊢T
⊢NΔ = ⊢∷ ⊢Δ Δ⊢N
⊢TqσNΔ = ⊢∷ ⊢NΔ ⊢Tqσ
⊢wk = s-wk ⊢NΓ
⊢wk′ = s-wk ⊢TNΓ
⊢wkwk = s-∘ ⊢wk′ ⊢wk