module Implicit.Language.Shift.Properties where
open import Implicit.Language.Base
open import Implicit.Language.Shift.Base
↑tm-total : ∀ (e : Term n m) (x)
→ ∃ λ e'
→ e ↑tm x ⇘ e'
↑tm-total (lit i) x = ⟨ lit i , ↑tm-lit ⟩
↑tm-total (` x₁) x = ⟨ ` punchIn x x₁ , ↑tm-var ⟩
↑tm-total (ƛ e) x = ⟨ ƛ ↑tm-total e (#S x) .proj₁ , ↑tm-ƛ (↑tm-total e (#S x) .proj₂) ⟩
↑tm-total (e · e₁) x = ⟨ ↑tm-total e x .proj₁ · ↑tm-total e₁ x .proj₁ ,
↑tm-app (↑tm-total e x .proj₂) (↑tm-total e₁ x .proj₂) ⟩
↑tm-total (e ⦂ A) x = ⟨ ↑tm-total e x .proj₁ ⦂ A , ↑tm-⦂ (↑tm-total e x .proj₂) ⟩
↑tm-total (Λ e) x = ⟨ Λ ↑tm-total e x .proj₁ , ↑tm-Λ (↑tm-total e x .proj₂) ⟩
↑tm-total (e ⓪ A) x = ⟨ ↑tm-total e x .proj₁ ⓪ A , ↑tm-⓪ (↑tm-total e x .proj₂) ⟩
↑tm-unique : e ↑tm k ⇘ e₁
→ e ↑tm k ⇘ e₂
→ e₁ ≡ e₂
↑tm-unique ↑tm-lit ↑tm-lit = refl
↑tm-unique ↑tm-var ↑tm-var = refl
↑tm-unique (↑tm-ƛ up1) (↑tm-ƛ up2) rewrite ↑tm-unique up1 up2 = refl
↑tm-unique (↑tm-app up1 up3) (↑tm-app up2 up4) rewrite ↑tm-unique up1 up2 | ↑tm-unique up3 up4 = refl
↑tm-unique (↑tm-⦂ up1) (↑tm-⦂ up2) rewrite ↑tm-unique up1 up2 = refl
↑tm-unique (↑tm-Λ up1) (↑tm-Λ up2) rewrite ↑tm-unique up1 up2 = refl
↑tm-unique (↑tm-⓪ up1) (↑tm-⓪ up2) rewrite ↑tm-unique up1 up2 = refl
↑ty-unique :
A ↑ty k ⇘ A₁
→ A ↑ty k ⇘ A₂
→ A₁ ≡ A₂
↑ty-unique ↑ty-int ↑ty-int = refl
↑ty-unique ↑ty-var ↑ty-var = refl
↑ty-unique (↑ty-arr up1 up3) (↑ty-arr up2 up4) rewrite ↑ty-unique up1 up2 | ↑ty-unique up3 up4 = refl
↑ty-unique (↑ty-∀ up1) (↑ty-∀ up2) rewrite ↑ty-unique up1 up2 = refl
↑ty-unique-inver' : A ↑ty k ⇘ T₁
→ B ↑ty k ⇘ T₂
→ T₁ ≡ T₂
→ A ≡ B
↑ty-unique-inver' ↑ty-int ↑ty-int eqT = refl
↑ty-unique-inver' {k = k} (↑ty-var {X = X}) (↑ty-var {X = Y}) eqT = cong ‶_ (punchIn-injective k X Y (‶-injective eqT))
↑ty-unique-inver' (↑ty-arr upA upA₁) (↑ty-arr upB upB₁) refl rewrite ↑ty-unique-inver' upA upB refl | ↑ty-unique-inver' upA₁ upB₁ refl = refl
↑ty-unique-inver' (↑ty-∀ upA) (↑ty-∀ upB) refl rewrite ↑ty-unique-inver' upA upB refl = refl
↑ty-unique-inver : A ↑ty k ⇘ T
→ B ↑ty k ⇘ T
→ A ≡ B
↑ty-unique-inver upA upB = ↑ty-unique-inver' upA upB refl
↑ty-total : ∀ (A : Type m) (k)
→ ∃ λ A'
→ A ↑ty k ⇘ A'
↑ty-total Int k = ⟨ Int , ↑ty-int ⟩
↑ty-total (‶ X) k = ⟨ ‶ punchIn k X , ↑ty-var ⟩
↑ty-total (A `→ A₁) k = ⟨ ↑ty-total A k .proj₁ `→ ↑ty-total A₁ k .proj₁ ,
↑ty-arr (↑ty-total A k .proj₂) (↑ty-total A₁ k .proj₂) ⟩
↑ty-total (`∀ A) k = ⟨ `∀ ↑ty-total A (#S k) .proj₁ , ↑ty-∀ (↑ty-total A (#S k) .proj₂)⟩
↑ty0-total : ∀ (A : Type m)
→ ∃ λ A'
→ ↑ty0 A ⇘ A'
↑ty0-total A = ↑ty-total A #0
↑ty-¬ε : A ↑ty k ⇘ A'
→ k ¬ε A'
↑ty-¬ε ↑ty-int = ¬ε-int
↑ty-¬ε {k = k} (↑ty-var {X = X}) = ¬ε-var (punchInᵢ≢i k X)
↑ty-¬ε (↑ty-arr upA upA₁) = ¬ε-arr (↑ty-¬ε upA) (↑ty-¬ε upA₁)
↑ty-¬ε (↑ty-∀ upA) = ¬ε-∀ (↑ty-¬ε upA)
↑ty-comm : k₁ #≤ k₂
→ A ↑ty k₁ ⇘ B
→ B ↑ty #S k₂ ⇘ C
→ A ↑ty k₂ ⇘ D
→ D ↑ty (inject₁ k₁) ⇘ C
↑ty-comm k₁≤k₂ ↑ty-int ↑ty-int ↑ty-int = ↑ty-int
↑ty-comm {k₁ = k₁} {k₂} k₁≤k₂ (↑ty-var {X = X}) ↑ty-var ↑ty-var
rewrite sym (punchIn-comm {x = X} {j = k₁} {k = k₂} k₁≤k₂) = ↑ty-var
↑ty-comm k₁≤k₂ (↑ty-arr up1 up4) (↑ty-arr up2 up5) (↑ty-arr up3 up6) =
↑ty-arr (↑ty-comm k₁≤k₂ up1 up2 up3) (↑ty-comm k₁≤k₂ up4 up5 up6)
↑ty-comm k₁≤k₂ (↑ty-∀ up1) (↑ty-∀ up2) (↑ty-∀ up3) = ↑ty-∀ (↑ty-comm (s≤s k₁≤k₂) up1 up2 up3)
private variable
A₀ Aₖ Aₖ₊₁ : Type m
↑ty-comm0 : ↑ty0 A ⇘ A₀
→ A₀ ↑ty #S k ⇘ Aₖ₊₁
→ A ↑ty k ⇘ Aₖ
→ ↑ty0 Aₖ ⇘ Aₖ₊₁
↑ty-comm0 up1 up2 up3 = ↑ty-comm {k₁ = #0} z≤n up1 up2 up3
↑ty-var-eq : Y ≡ punchIn k X
→ (‶ X) ↑ty k ⇘ ‶ Y
↑ty-var-eq refl = ↑ty-var
↑ty-var-inv-eq : (‶ X) ↑ty k ⇘ ‶ Y
→ Y ≡ punchIn k X
↑ty-var-inv-eq ↑ty-var = refl
↑ty-comm-v2 : k₁ #≤ k₂
→ B ↑ty #S k₂ ⇘ C
→ D ↑ty (inject₁ k₁) ⇘ C
→ A ↑ty k₂ ⇘ D
→ A ↑ty k₁ ⇘ B
↑ty-comm-v2 lt ↑ty-int ↑ty-int ↑ty-int = ↑ty-int
↑ty-comm-v2 {k₁ = k₁} {k₂} lt (↑ty-var {X = X}) up2 (↑ty-var {X = Y})
with eq1 ← ↑ty-var-inv-eq up2
with eq2 ← punchIn-comm {x = Y} {j = k₁} {k = k₂} lt
= ↑ty-var-eq (punchIn-injective (#S k₂) X (punchIn k₁ Y)(trans eq1 eq2))
↑ty-comm-v2 lt (↑ty-arr up1 up4) (↑ty-arr up2 up5) (↑ty-arr up3 up6) = ↑ty-arr (↑ty-comm-v2 lt up1 up2 up3) (↑ty-comm-v2 lt up4 up5 up6)
↑ty-comm-v2 lt (↑ty-∀ up1) (↑ty-∀ up2) (↑ty-∀ up3) = ↑ty-∀ (↑ty-comm-v2 (s≤s lt) up1 up2 up3)
↑ty-comm1 : A₀ ↑ty #S k ⇘ Aₖ₊₁
→ ↑ty0 Aₖ ⇘ Aₖ₊₁
→ A ↑ty k ⇘ Aₖ
→ ↑ty0 A ⇘ A₀
↑ty-comm1 up1 up2 up3 = ↑ty-comm-v2 z≤n up1 up2 up3
↑ty-comm' : k₁ #≤ k₂
→ A ↑ty k₂ ⇘ D
→ D ↑ty (inject₁ k₁) ⇘ C
→ A ↑ty k₁ ⇘ B
→ B ↑ty #S k₂ ⇘ C
↑ty-comm' k₁≤k₂ ↑ty-int ↑ty-int ↑ty-int = ↑ty-int
↑ty-comm' {k₁ = k₁} {k₂} k₁≤k₂ (↑ty-var {X = X}) ↑ty-var ↑ty-var
rewrite punchIn-comm {x = X} {j = k₁} {k = k₂} k₁≤k₂ = ↑ty-var
↑ty-comm' k₁≤k₂ (↑ty-arr up1 up4) (↑ty-arr up2 up5) (↑ty-arr up3 up6) =
↑ty-arr (↑ty-comm' k₁≤k₂ up1 up2 up3) (↑ty-comm' k₁≤k₂ up4 up5 up6)
↑ty-comm' k₁≤k₂ (↑ty-∀ up1) (↑ty-∀ up2) (↑ty-∀ up3) = ↑ty-∀ (↑ty-comm' (s≤s k₁≤k₂) up1 up2 up3)
↑ty-comm0' : A ↑ty k ⇘ Aₖ
→ ↑ty0 Aₖ ⇘ Aₖ₊₁
→ ↑ty0 A ⇘ A₀
→ A₀ ↑ty #S k ⇘ Aₖ₊₁
↑ty-comm0' up1 up2 up3 = ↑ty-comm' z≤n up1 up2 up3
↑tyᵉ-comm' : k₁ #≤ k₂
→ e₁ ↑tyᵉ k₂ ⇘ e₄
→ e₄ ↑tyᵉ (inject₁ k₁) ⇘ e₃
→ e₁ ↑tyᵉ k₁ ⇘ e₂
→ e₂ ↑tyᵉ #S k₂ ⇘ e₃
↑tyᵉ-comm' lt ↑tyᵉ-lit ↑tyᵉ-lit ↑tyᵉ-lit = ↑tyᵉ-lit
↑tyᵉ-comm' lt ↑tyᵉ-var ↑tyᵉ-var ↑tyᵉ-var = ↑tyᵉ-var
↑tyᵉ-comm' lt (↑tyᵉ-ƛ up1) (↑tyᵉ-ƛ up2) (↑tyᵉ-ƛ up3) = ↑tyᵉ-ƛ (↑tyᵉ-comm' lt up1 up2 up3)
↑tyᵉ-comm' lt (↑tyᵉ-app up1 up4) (↑tyᵉ-app up2 up5) (↑tyᵉ-app up3 up6) = ↑tyᵉ-app (↑tyᵉ-comm' lt up1 up2 up3) (↑tyᵉ-comm' lt up4 up5 up6)
↑tyᵉ-comm' lt (↑tyᵉ-⦂ up1 up) (↑tyᵉ-⦂ up2 up₁) (↑tyᵉ-⦂ up3 up₂) = ↑tyᵉ-⦂ (↑tyᵉ-comm' lt up1 up2 up3) (↑ty-comm' lt up up₁ up₂)
↑tyᵉ-comm' lt (↑tyᵉ-Λ up1) (↑tyᵉ-Λ up2) (↑tyᵉ-Λ up3) = ↑tyᵉ-Λ (↑tyᵉ-comm' (s≤s lt) up1 up2 up3)
↑tyᵉ-comm' lt (↑tyᵉ-⓪ up1 upA1) (↑tyᵉ-⓪ up2 upA2) (↑tyᵉ-⓪ up3 upA3) = ↑tyᵉ-⓪ (↑tyᵉ-comm' lt up1 up2 up3) (↑ty-comm' lt upA1 upA2 upA3)
↑tyᵉ-comm0' : ∀ {e : Term n m} {eₖ eₖ₊₁ e₀ k}
→ e ↑tyᵉ k ⇘ eₖ
→ ↑tyᵉ0 eₖ ⇘ eₖ₊₁
→ ↑tyᵉ0 e ⇘ e₀
→ e₀ ↑tyᵉ #S k ⇘ eₖ₊₁
↑tyᵉ-comm0' up1 up2 up3 = ↑tyᵉ-comm' z≤n up1 up2 up3
↑tm-comm' : k₁ #≤ k₂
→ e ↑tm k₂ ⇘ e₁
→ e₁ ↑tm (inject₁ k₁) ⇘ e₂
→ e ↑tm k₁ ⇘ e'
→ e' ↑tm #S k₂ ⇘ e₂
↑tm-comm' lt ↑tm-lit ↑tm-lit ↑tm-lit = ↑tm-lit
↑tm-comm' {k₁ = k₁} {k₂} lt(↑tm-var {x = x}) ↑tm-var ↑tm-var
rewrite punchIn-comm {x = x} {j = k₁} {k = k₂} lt = ↑tm-var
↑tm-comm' lt (↑tm-ƛ up1) (↑tm-ƛ up2) (↑tm-ƛ up3) = ↑tm-ƛ (↑tm-comm' (s≤s lt) up1 up2 up3)
↑tm-comm' lt (↑tm-app up1 up4) (↑tm-app up2 up5) (↑tm-app up3 up6) = ↑tm-app (↑tm-comm' lt up1 up2 up3) (↑tm-comm' lt up4 up5 up6)
↑tm-comm' lt (↑tm-⦂ up1) (↑tm-⦂ up2) (↑tm-⦂ up3) = ↑tm-⦂ (↑tm-comm' lt up1 up2 up3)
↑tm-comm' lt (↑tm-Λ up1) (↑tm-Λ up2) (↑tm-Λ up3) = ↑tm-Λ (↑tm-comm' lt up1 up2 up3)
↑tm-comm' lt (↑tm-⓪ up1) (↑tm-⓪ up2) (↑tm-⓪ up3) = ↑tm-⓪ (↑tm-comm' lt up1 up2 up3)
↑ty-punchOut : (¬p : k ≢ X)
→ ‶ punchOut ¬p ↑ty k ⇘ ‶ X
↑ty-punchOut ¬p = helper ¬p (sym (punchIn-punchOut ¬p))
where helper : (¬p : k ≢ X)
→ X ≡ punchIn k (punchOut ¬p)
→ ‶ punchOut ¬p ↑ty k ⇘ ‶ X
helper ¬p eq with punchOut ¬p
helper ¬p refl | Y = ↑ty-var
↑ty-surjective : k ¬ε A'
→ ∃[ A ](A ↑ty k ⇘ A')
↑ty-surjective ¬ε-int = ⟨ Int , ↑ty-int ⟩
↑ty-surjective (¬ε-var x) = ⟨ (‶ punchOut (≢-sym x)) , (↑ty-punchOut (≢-sym x)) ⟩
↑ty-surjective (¬ε-arr ¬inA' ¬inA'') = ⟨ ↑ty-surjective ¬inA' .proj₁ `→ ↑ty-surjective ¬inA'' .proj₁ ,
↑ty-arr (↑ty-surjective ¬inA' .proj₂)
(↑ty-surjective ¬inA'' .proj₂)
⟩
↑ty-surjective (¬ε-∀ ¬inA') = ⟨ `∀ ↑ty-surjective ¬inA' .proj₁ ,
↑ty-∀ (↑ty-surjective ¬inA' .proj₂) ⟩
↑ty-surjective⋆ : k ¬ε⋆ A'
→ k' #≤ k
→ ∃[ A ](A ↑ty k' ⇘ A')
↑ty-surjective⋆ ¬ε⋆-int lt = ⟨ Int , ↑ty-int ⟩
↑ty-surjective⋆ {k' = k'} (¬ε⋆-var {k' = k''} x) lt = ⟨ (‶ punchOut helper) , (↑ty-punchOut helper) ⟩
where helper : k' ≢ k''
helper = #≤-#<-≢ lt x
↑ty-surjective⋆ (¬ε⋆-arr ninA ninA₁) lt = ⟨ ↑ty-surjective⋆ ninA lt .proj₁ `→ ↑ty-surjective⋆ ninA₁ lt .proj₁
, ↑ty-arr (↑ty-surjective⋆ ninA lt .proj₂)
(↑ty-surjective⋆ ninA₁ lt .proj₂) ⟩
↑ty-surjective⋆ (¬ε⋆-∀ ninA) lt = ⟨ `∀ ↑ty-surjective⋆ ninA (s≤s lt) .proj₁ ,
↑ty-∀ (↑ty-surjective⋆ ninA (s≤s lt) .proj₂) ⟩
¬ε⋆-↑ty : k₁ ¬ε⋆ A
→ A ↑ty k₂ ⇘ A'
→ k₂ #≤ k₁
→ #S k₁ ¬ε⋆ A'
¬ε⋆-↑ty ¬ε⋆-int ↑ty-int lt = ¬ε⋆-int
¬ε⋆-↑ty (¬ε⋆-var x) ↑ty-var lt = ¬ε⋆-var (helper lt x)
where
helper : ∀ {k₁ : Fin m} {k₂ : Fin (1 + m)} {X}
→ k₂ #≤ k₁
→ k₁ #< X
→ #S k₁ #< punchIn k₂ X
helper {k₁ = #0} {k₂ = #0} {X = #S X} lt1 lt2 = s≤s lt2
helper {k₁ = #S k₁} {k₂ = #0} {X = X} lt1 lt2 = s≤s lt2
helper {k₁ = #S k₁} {k₂ = #S k₂} {X = #S X} (s≤s lt1) (s≤s lt2) = s≤s (helper lt1 lt2)
¬ε⋆-↑ty (¬ε⋆-arr ninA ninA₁) (↑ty-arr upA upA₁) lt = ¬ε⋆-arr (¬ε⋆-↑ty ninA upA lt) (¬ε⋆-↑ty ninA₁ upA₁ lt)
¬ε⋆-↑ty (¬ε⋆-∀ ninA) (↑ty-∀ upA) lt = ¬ε⋆-∀ (¬ε⋆-↑ty ninA upA (s≤s lt))
¬ε⋆-↑ty' : #S k₁ ¬ε⋆ A'
→ A ↑ty k₂ ⇘ A'
→ k₂ #≤ k₁
→ k₁ ¬ε⋆ A
¬ε⋆-↑ty' ¬ε⋆-int ↑ty-int lt = ¬ε⋆-int
¬ε⋆-↑ty' (¬ε⋆-var x) ↑ty-var lt = ¬ε⋆-var (helper x lt)
where helper : ∀ {k₁ : Fin m} {k₂ : Fin (1 + m)} {X}
→ #S k₁ #< punchIn k₂ X
→ k₂ #≤ k₁
→ k₁ #< X
helper {k₁ = #0} {k₂ = #0} {X = #0} (s≤s ()) lt2
helper {k₁ = #0} {k₂ = #0} {X = #S X} lt1 lt2 = s≤s z≤n
helper {k₁ = #S k₁} {k₂ = #0} {X = #0} (s≤s ()) lt2
helper {k₁ = #S k₁} {k₂ = #0} {X = #S X} (s≤s (s≤s lt1)) lt2 = s≤s lt1
helper {k₁ = #S k₁} {k₂ = #S k₂} {X = #S X} (s≤s lt1) (s≤s lt2) = s≤s (helper lt1 lt2)
¬ε⋆-↑ty' (¬ε⋆-arr ninA' ninA'') (↑ty-arr upA upA₁) lt = ¬ε⋆-arr (¬ε⋆-↑ty' ninA' upA lt) (¬ε⋆-↑ty' ninA'' upA₁ lt)
¬ε⋆-↑ty' (¬ε⋆-∀ ninA') (↑ty-∀ upA) lt = ¬ε⋆-∀ (¬ε⋆-↑ty' ninA' upA (s≤s lt))
¬ε⋆-↑ty'0 : #S k ¬ε⋆ A'
→ ↑ty0 A ⇘ A'
→ k ¬ε⋆ A
¬ε⋆-↑ty'0 ninA' upA = ¬ε⋆-↑ty' ninA' upA z≤n
¬ε-↑ty : k₁ ¬ε T
→ T ↑ty k₂ ⇘ T'
→ k₂ #≤ k₁
→ (#S k₁) ¬ε T'
¬ε-↑ty ¬ε-int ↑ty-int lt = ¬ε-int
¬ε-↑ty (¬ε-var x) ↑ty-var lt rewrite sym (punchIn-≤ lt) = ¬ε-var (punchIn-≢ x)
¬ε-↑ty (¬ε-arr ¬inT ¬inT₁) (↑ty-arr upT upT₁) lt = ¬ε-arr (¬ε-↑ty ¬inT upT lt) (¬ε-↑ty ¬inT₁ upT₁ lt)
¬ε-↑ty (¬ε-∀ ¬inT) (↑ty-∀ upT) lt = ¬ε-∀ (¬ε-↑ty ¬inT upT (s≤s lt))
¬ε-↑ty0 : k ¬ε T
→ ↑ty0 T ⇘ T'
→ #S k ¬ε T'
¬ε-↑ty0 ¬inT upT = ¬ε-↑ty ¬inT upT z≤n
¬ε-↑ty-≤ : (#S k₁) ¬ε T'
→ T ↑ty k₂ ⇘ T'
→ k₂ #≤ k₁
→ k₁ ¬ε T
¬ε-↑ty-≤ ¬ε-int ↑ty-int lt = ¬ε-int
¬ε-↑ty-≤ (¬ε-var x) ↑ty-var lt = ¬ε-var (helper lt x)
where helper : ∀ {m} {k₁ : Fin m} {k₂ X}
→ k₂ #≤ k₁
→ punchIn k₂ X ≢ #S k₁
→ X ≢ k₁
helper {k₁ = #0} {k₂ = #0} {X = #0} lt neq = λ z → neq refl
helper {k₁ = #0} {k₂ = #0} {X = #S X} lt neq = λ ()
helper {k₁ = #S k₁} {k₂ = #0} {X = #0} lt neq = λ ()
helper {k₁ = #S k₁} {k₂ = #0} {X = #S X} lt neq = ≢-pred neq
helper {k₁ = #S k₁} {k₂ = #S k₂} {X = #0} lt neq = λ ()
helper {k₁ = #S k₁} {k₂ = #S k₂} {X = #S X} (s≤s lt) neq = ≢-suc (helper lt (≢-pred neq))
¬ε-↑ty-≤ (¬ε-arr ninT' ninT'') (↑ty-arr upT upT₁) lt = ¬ε-arr (¬ε-↑ty-≤ ninT' upT lt) (¬ε-↑ty-≤ ninT'' upT₁ lt)
¬ε-↑ty-≤ (¬ε-∀ ninT') (↑ty-∀ upT) lt = ¬ε-∀ (¬ε-↑ty-≤ ninT' upT (s≤s lt))
¬ε-↑ty' : X ¬ε A
→ A ↑ty k ⇘ A'
→ X #< k
→ inject₁ X ¬ε A'
¬ε-↑ty' ¬ε-int ↑ty-int lt = ¬ε-int
¬ε-↑ty' (¬ε-var x) ↑ty-var lt = ¬ε-var (≢-sym (punchIn-inject-neq lt (≢-sym x)))
¬ε-↑ty' (¬ε-arr ninA ninA₁) (↑ty-arr up up₁) lt = ¬ε-arr (¬ε-↑ty' ninA up lt) (¬ε-↑ty' ninA₁ up₁ lt)
¬ε-↑ty' (¬ε-∀ ninA) (↑ty-∀ up) lt = ¬ε-∀ (¬ε-↑ty' ninA up (s≤s lt))
¬ε-↑ty0' : #0 ¬ε A
→ A ↑ty #S k ⇘ A'
→ #0 ¬ε A'
¬ε-↑ty0' ¬inA upA = ¬ε-↑ty' ¬inA upA (s≤s z≤n)
¬ε-↑ty'-inv : inject₁ X ¬ε A'
→ A ↑ty k ⇘ A'
→ X #< k
→ X ¬ε A
¬ε-↑ty'-inv ¬ε-int ↑ty-int lt = ¬ε-int
¬ε-↑ty'-inv (¬ε-var x) ↑ty-var lt = ¬ε-var λ where
refl → x (sym (punchIn-inject lt))
¬ε-↑ty'-inv (¬ε-arr ninA ninA₁) (↑ty-arr upA upA₁) lt = ¬ε-arr (¬ε-↑ty'-inv ninA upA lt) (¬ε-↑ty'-inv ninA₁ upA₁ lt)
¬ε-↑ty'-inv (¬ε-∀ ninA) (↑ty-∀ upA) lt = ¬ε-∀ (¬ε-↑ty'-inv ninA upA (s≤s lt))
¬ε-↑ty'-inv0 : #0 ¬ε A'
→ A ↑ty #S k ⇘ A'
→ #0 ¬ε A
¬ε-↑ty'-inv0 ninA upA = ¬ε-↑ty'-inv ninA upA (s≤s z≤n)
↑ty-¬ε-prv : X ¬ε A
→ A ↑ty k ⇘ A'
→ X #< k
→ inject₁ X ¬ε A'
↑ty-¬ε-prv ¬ε-int ↑ty-int lt = ¬ε-int
↑ty-¬ε-prv (¬ε-var x) ↑ty-var lt = ¬ε-var (≢-sym (punchIn-inject-neq lt (≢-sym x)))
↑ty-¬ε-prv (¬ε-arr ¬inA ¬inA₁) (↑ty-arr upA upA₁) lt = ¬ε-arr (↑ty-¬ε-prv ¬inA upA lt) (↑ty-¬ε-prv ¬inA₁ upA₁ lt)
↑ty-¬ε-prv (¬ε-∀ ¬inA) (↑ty-∀ upA) lt = ¬ε-∀ (↑ty-¬ε-prv ¬inA upA (s≤s lt))
↑tyᵉ-total : ∀ (e : Term n m) k
→ ∃ λ e'
→ e ↑tyᵉ k ⇘ e'
↑tyᵉ-total (lit i) k = ⟨ lit i , ↑tyᵉ-lit ⟩
↑tyᵉ-total (` x) k = ⟨ ` x , ↑tyᵉ-var ⟩
↑tyᵉ-total (ƛ e) k = ⟨ ƛ ↑tyᵉ-total e k .proj₁ , ↑tyᵉ-ƛ (↑tyᵉ-total e k .proj₂) ⟩
↑tyᵉ-total (e · e₁) k = ⟨ ↑tyᵉ-total e k .proj₁ · ↑tyᵉ-total e₁ k .proj₁ ,
↑tyᵉ-app (↑tyᵉ-total e k .proj₂) (↑tyᵉ-total e₁ k .proj₂) ⟩
↑tyᵉ-total (e ⦂ A) k with ↑tyᵉ-total e k | ↑ty-total A k
... | ⟨ e' , upe ⟩ | ⟨ A' , upA ⟩ = ⟨ e' ⦂ A' , ↑tyᵉ-⦂ upe upA ⟩
↑tyᵉ-total (Λ e) k = ⟨ Λ ↑tyᵉ-total e (#S k) .proj₁ ,
↑tyᵉ-Λ (↑tyᵉ-total e (#S k) .proj₂) ⟩
↑tyᵉ-total (e ⓪ A) k with ↑tyᵉ-total e k | ↑ty-total A k
... | ⟨ e' , upe ⟩ | ⟨ A' , upA ⟩ = ⟨ e' ⓪ A' , ↑tyᵉ-⓪ upe upA ⟩
↑tyᵉ0-total : ∀ (e : Term n m)
→ ∃ λ e'
→ ↑tyᵉ0 e ⇘ e'
↑tyᵉ0-total e = ↑tyᵉ-total e #0
↑tyᵉ-unique : e ↑tyᵉ k ⇘ e₁
→ e ↑tyᵉ k ⇘ e₂
→ e₁ ≡ e₂
↑tyᵉ-unique ↑tyᵉ-lit ↑tyᵉ-lit = refl
↑tyᵉ-unique ↑tyᵉ-var ↑tyᵉ-var = refl
↑tyᵉ-unique (↑tyᵉ-ƛ up1) (↑tyᵉ-ƛ up2) with refl ← ↑tyᵉ-unique up1 up2 = refl
↑tyᵉ-unique (↑tyᵉ-app up1 up3) (↑tyᵉ-app up2 up4)
with refl ← ↑tyᵉ-unique up1 up2
with refl ← ↑tyᵉ-unique up3 up4 = refl
↑tyᵉ-unique (↑tyᵉ-⦂ up1 up) (↑tyᵉ-⦂ up2 up₁)
with refl ← ↑tyᵉ-unique up1 up2
with refl ← ↑ty-unique up up₁ = refl
↑tyᵉ-unique (↑tyᵉ-Λ up1) (↑tyᵉ-Λ up2)
with refl ← ↑tyᵉ-unique up1 up2 = refl
↑tyᵉ-unique (↑tyᵉ-⓪ up1 upA1) (↑tyᵉ-⓪ up2 upA2)
with refl ← ↑tyᵉ-unique up1 up2
with refl ← ↑ty-unique upA1 upA2 = refl
↑tm-gc : GenericConsumer e
→ e ↑tm k ⇘ e'
→ GenericConsumer e'
↑tm-gc gc-i ↑tm-lit = gc-i
↑tm-gc gc-var ↑tm-var = gc-var
↑tm-gc gc-ann (↑tm-⦂ upe) = gc-ann
↑tm-gc gc-tlam (↑tm-Λ upe) = gc-tlam
↑tm-gc' : GenericConsumer e'
→ e ↑tm k ⇘ e'
→ GenericConsumer e
↑tm-gc' gc-i ↑tm-lit = gc-i
↑tm-gc' gc-var ↑tm-var = gc-var
↑tm-gc' gc-ann (↑tm-⦂ upe) = gc-ann
↑tm-gc' gc-tlam (↑tm-Λ upe) = gc-tlam
↑ty-gc' : GenericConsumer e'
→ e ↑tyᵉ k ⇘ e'
→ GenericConsumer e
↑ty-gc' gc-i ↑tyᵉ-lit = gc-i
↑ty-gc' gc-var ↑tyᵉ-var = gc-var
↑ty-gc' gc-ann (↑tyᵉ-⦂ up up₁) = gc-ann
↑ty-gc' gc-tlam (↑tyᵉ-Λ up) = gc-tlam
↑ty-var-inv-helper : ∀ {B : Type m} {k Y X}
→ B ↑ty k ⇘ ‶ Y
→ Y ≡ punchIn k X
→ B ≡ ‶ X
↑ty-var-inv-helper {B = B} {k = k} {Y = Y} {X = X} (↑ty-var {X = X'}) eq = cong ‶_ (punchIn-injective k X' X eq)
↑ty-var-inv : ∀ {m} {X Y : Fin m} {re k : Fin (1 + m)}
→ ‶ X ↑ty k ⇘ ‶ re
→ re ≡ punchIn k Y
→ X ≡ Y
↑ty-var-inv {X = X} {Y = Y} {k = k} ↑ty-var eq = punchIn-injective k X Y eq