{-# OPTIONS
  --without-K
  --prop
  --rewriting
  --confluence-check
  --hidden-argument-puns
#-}

module TT.SSC.Lift where

open import TT.Lib
open import TT.SSC.Syntax
open import TT.SSC.Path
open import TT.SSC.Tel
open import TT.SSC.AlphaNorm

private variable
  i : ℕ
  Γ Δ : Con
  A B : Ty Γ i
  a b : Tm Γ A
  Ω : Tel Γ

module _
  (γ*₀ γ*₁ : Sub* Δ Γ) (γ*₀₁ᵀ : ∀ {i} {A : Ty Γ i} → A [ γ*₀ ]ᵀ* ≡ A [ γ*₁ ]ᵀ*)
  where
  []ᵀ→⁺^ᵀᵛ :
    (Ω-γ*₀₁ : Ω [ γ*₀ ]ᵀˡ* ≡ Ω [ γ*₁ ]ᵀˡ*) → Var (Γ ++ Ω) A a →
    A [ γ*₀ ⁺^* ]ᵀ* ≡[ ap-Ty (ap-++ Ω-γ*₀₁) ] A [ γ*₁ ⁺^* ]ᵀ*
  []ᵀ→⁺^ᵀᵛ {Ω = ◇} ◇-γ*₀₁ aᵛ = dep γ*₀₁ᵀ
  []ᵀ→⁺^ᵀᵛ {Ω = Ω ▹ A} Ω▹A-γ*₀₁ vz =
    dep (p-⁺ᵀ* (γ*₀ ⁺^*)) ∙ᵈ
    apᵈ-[]ᵀ
      (ap-++ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁))
      (▹ᵀˡ-inj-A Ω▹A-γ*₀₁)
      (ap-▹ (ap-++ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁)) (▹ᵀˡ-inj-A Ω▹A-γ*₀₁))
      (apᵈ-p (ap-++ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁)) (▹ᵀˡ-inj-A Ω▹A-γ*₀₁)) ∙ᵈ
    dep (sym (p-⁺ᵀ* (γ*₁ ⁺^*)))
  []ᵀ→⁺^ᵀᵛ {Ω = Ω ▹ A} Ω▹A-γ*₀₁ (vs bᵛ) =
    dep (p-⁺ᵀ* (γ*₀ ⁺^*)) ∙ᵈ
    apᵈ-[]ᵀ
      (ap-++ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁))
      ([]ᵀ→⁺^ᵀᵛ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁) bᵛ)
      (ap-▹ (ap-++ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁)) (▹ᵀˡ-inj-A Ω▹A-γ*₀₁))
      (apᵈ-p (ap-++ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁)) (▹ᵀˡ-inj-A Ω▹A-γ*₀₁)) ∙ᵈ
    dep (sym (p-⁺ᵀ* (γ*₁ ⁺^*)))

module []ᵛ→⁺^
  (γ*₀ γ*₁ : Sub* Δ Γ)
  (γ*₀₁ᵀ : ∀ {i} {A : Ty Γ i} → A [ γ*₀ ]ᵀ* ≡ A [ γ*₁ ]ᵀ*)
  (γ*₀₁ᵛ :
    ∀ {i} {A : Ty Γ i} {a}
    (aᵛ : Var Γ A a) → a [ γ*₀ ]ᵗ* ≡[ ap-Tm γ*₀₁ᵀ ] a [ γ*₁ ]ᵗ*)
  where
  private
    []ᵛ→⁺^ᵛ₀ :
      ∀ {A : Ty (Γ ++ Ω) i} {a}
      (Ω-γ*₀₁ : Ω [ γ*₀ ]ᵀˡ* ≡ Ω [ γ*₁ ]ᵀˡ*) (aᵛ : Var (Γ ++ Ω) A a) →
      a [ γ*₀ ⁺^* ]ᵗ*
        ≡[ ap-Tm₂ (ap-++ Ω-γ*₀₁) ([]ᵀ→⁺^ᵀᵛ γ*₀ γ*₁ γ*₀₁ᵀ Ω-γ*₀₁ aᵛ) ]
      a [ γ*₁ ⁺^* ]ᵗ*
    []ᵛ→⁺^ᵛ₀ {Ω = ◇} ◇-γ*₀₁ aᵛ = γ*₀₁ᵛ aᵛ
    []ᵛ→⁺^ᵛ₀ {Ω = Ω ▹ A} Ω▹A-γ*₀₁ vz =
      q-⁺* (γ*₀ ⁺^*) ∙ᵈ
      apᵈ-q (ap-++ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁)) (▹ᵀˡ-inj-A Ω▹A-γ*₀₁) ∙ᵈ
      symᵈ (q-⁺* (γ*₁ ⁺^*))
    []ᵛ→⁺^ᵛ₀ {Ω = Ω ▹ A} Ω▹A-γ*₀₁ (vs bᵛ) =
      p-⁺ᵗ* (γ*₀ ⁺^*) ∙ᵈ
      apᵈ-[]ᵗ₅
        (ap-++ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁))
        ([]ᵀ→⁺^ᵀᵛ γ*₀ γ*₁ γ*₀₁ᵀ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁) bᵛ)
        ([]ᵛ→⁺^ᵛ₀ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁) bᵛ)
        (ap-▹ (ap-++ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁)) (▹ᵀˡ-inj-A Ω▹A-γ*₀₁))
        (apᵈ-p (ap-++ (▹ᵀˡ-inj-Ω Ω▹A-γ*₀₁)) (▹ᵀˡ-inj-A Ω▹A-γ*₀₁)) ∙ᵈ
      symᵈ (p-⁺ᵗ* (γ*₁ ⁺^*))

    []ᵛ→⁺^ᵀ₀ :
      (Ω-γ*₀₁ : Ω [ γ*₀ ]ᵀˡ* ≡ Ω [ γ*₁ ]ᵀˡ*) → NTy (Γ ++ Ω) i A →
      A [ γ*₀ ⁺^* ]ᵀ* ≡[ ap-Ty (ap-++ Ω-γ*₀₁) ] A [ γ*₁ ⁺^* ]ᵀ*
    []ᵛ→⁺^ᵀᵗ₀ :
      (Ω-γ*₀₁ : Ω [ γ*₀ ]ᵀˡ* ≡ Ω [ γ*₁ ]ᵀˡ*) → NTm (Γ ++ Ω) A a →
      A [ γ*₀ ⁺^* ]ᵀ* ≡[ ap-Ty (ap-++ Ω-γ*₀₁) ] A [ γ*₁ ⁺^* ]ᵀ*
    []ᵛ→⁺^ᵗ₀ :
      ∀ {A : Ty (Γ ++ Ω) i} {a}
      (Ω-γ*₀₁ : Ω [ γ*₀ ]ᵀˡ* ≡ Ω [ γ*₁ ]ᵀˡ*) (aᴺ : NTm (Γ ++ Ω) A a) →
      a [ γ*₀ ⁺^* ]ᵗ* ≡[ ap-Tm₂ (ap-++ Ω-γ*₀₁) ([]ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ aᴺ) ]
      a [ γ*₁ ⁺^* ]ᵗ*

    []ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ (Uᴺ i) =
      dep (U-[]* (γ*₀ ⁺^*)) ∙ᵈ
      apᵈ-U (ap-++ Ω-γ*₀₁) ∙ᵈ
      dep (sym (U-[]* (γ*₁ ⁺^*)))
    []ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ (Elᴺ αᴺ) =
      dep (El-[]* (γ*₀ ⁺^*)) ∙ᵈ
      apᵈ-El (ap-++ Ω-γ*₀₁) (splitlr ([]ᵛ→⁺^ᵗ₀ Ω-γ*₀₁ αᴺ)) ∙ᵈ
      dep (sym (El-[]* (γ*₁ ⁺^*)))
    []ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ (Liftᴺ Aᴺ) =
      dep (Lift-[]* (γ*₀ ⁺^*)) ∙ᵈ
      apᵈ-Lift (ap-++ Ω-γ*₀₁) ([]ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ Aᴺ) ∙ᵈ
      dep (sym (Lift-[]* (γ*₁ ⁺^*)))
    []ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ (Πᴺ Aᴺ Bᴺ) =
      dep (Π-[]* (γ*₀ ⁺^*)) ∙ᵈ
      apᵈ-Π
        (ap-++ Ω-γ*₀₁)
        ([]ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ Aᴺ)
        ([]ᵛ→⁺^ᵀ₀ (ap-▹ᵀˡ Ω-γ*₀₁ ([]ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ Aᴺ)) Bᴺ) ∙ᵈ
      dep (sym (Π-[]* (γ*₁ ⁺^*)))

    []ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ (var aᵛ) = []ᵀ→⁺^ᵀᵛ γ*₀ γ*₁ γ*₀₁ᵀ Ω-γ*₀₁ aᵛ
    []ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ (cᴺ Aᴺ) =
      dep (U-[]* (γ*₀ ⁺^*)) ∙ᵈ
      apᵈ-U (ap-++ Ω-γ*₀₁) ∙ᵈ
      dep (sym (U-[]* (γ*₁ ⁺^*)))

    []ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ (lowerᴺ Aᴺ aᴺ) = []ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ Aᴺ
    []ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ (liftᴺ _ aᴺ) =
      dep (Lift-[]* (γ*₀ ⁺^*)) ∙ᵈ
      apᵈ-Lift (ap-++ Ω-γ*₀₁) ([]ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ aᴺ) ∙ᵈ
      dep (sym (Lift-[]* (γ*₁ ⁺^*)))

    []ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ (appᴺ _ Bᴺ fᴺ aᴺ) =
      dep (⟨⟩-[]ᵀ* (γ*₀ ⁺^*)) ∙ᵈ
      apᵈ-[]ᵀ
        (ap-▹ (ap-++ Ω-γ*₀₁) ([]ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ aᴺ))
        ([]ᵛ→⁺^ᵀ₀ (ap-▹ᵀˡ Ω-γ*₀₁ ([]ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ aᴺ)) Bᴺ)
        (ap-++ Ω-γ*₀₁)
        (apᵈ-⟨⟩₃ (ap-++ Ω-γ*₀₁) ([]ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ aᴺ) ([]ᵛ→⁺^ᵗ₀ Ω-γ*₀₁ aᴺ)) ∙ᵈ
      dep (sym (⟨⟩-[]ᵀ* (γ*₁ ⁺^*)))
    []ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ (lamᴺ Aᴺ _ bᴺ) =
      dep (Π-[]* (γ*₀ ⁺^*)) ∙ᵈ
      apᵈ-Π
        (ap-++ Ω-γ*₀₁)
        ([]ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ Aᴺ)
        ([]ᵛ→⁺^ᵀᵗ₀ (ap-▹ᵀˡ Ω-γ*₀₁ ([]ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ Aᴺ)) bᴺ) ∙ᵈ
      dep (sym (Π-[]* (γ*₁ ⁺^*)))

    []ᵛ→⁺^ᵗ₀ Ω-γ*₀₁ (var aᵛ) = []ᵛ→⁺^ᵛ₀ Ω-γ*₀₁ aᵛ
    []ᵛ→⁺^ᵗ₀ Ω-γ*₀₁ (cᴺ Aᴺ) =
      c-[]* (γ*₀ ⁺^*) ∙ᵈ
      apᵈ-c (ap-++ Ω-γ*₀₁) ([]ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ Aᴺ) ∙ᵈ
      symᵈ (c-[]* (γ*₁ ⁺^*))

    []ᵛ→⁺^ᵗ₀ Ω-γ*₀₁ (lowerᴺ Aᴺ aᴺ) =
      dep (lower-[]* (γ*₀ ⁺^*)) ∙ᵈ
      apᵈ-lower
        (ap-++ Ω-γ*₀₁)
        ([]ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ Aᴺ)
        (splitlr ([]ᵛ→⁺^ᵗ₀ Ω-γ*₀₁ aᴺ)) ∙ᵈ
      dep (sym (lower-[]* (γ*₁ ⁺^*)))
    []ᵛ→⁺^ᵗ₀ Ω-γ*₀₁ (liftᴺ _ aᴺ) =
      lift-[]* (γ*₀ ⁺^*) ∙ᵈ
      apᵈ-lift (ap-++ Ω-γ*₀₁) ([]ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ aᴺ) ([]ᵛ→⁺^ᵗ₀ Ω-γ*₀₁ aᴺ) ∙ᵈ
      symᵈ (lift-[]* (γ*₁ ⁺^*))

    []ᵛ→⁺^ᵗ₀ Ω-γ*₀₁ (appᴺ _ Bᴺ fᴺ aᴺ) =
      app-[]* (γ*₀ ⁺^*) ∙ᵈ
      apᵈ-app
        (ap-++ Ω-γ*₀₁)
        ([]ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ aᴺ)
        ([]ᵛ→⁺^ᵀ₀ (ap-▹ᵀˡ Ω-γ*₀₁ ([]ᵛ→⁺^ᵀᵗ₀ Ω-γ*₀₁ aᴺ)) Bᴺ)
        (splitlr ([]ᵛ→⁺^ᵗ₀ Ω-γ*₀₁ fᴺ))
        ([]ᵛ→⁺^ᵗ₀ Ω-γ*₀₁ aᴺ) ∙ᵈ
      symᵈ (app-[]* (γ*₁ ⁺^*))
    []ᵛ→⁺^ᵗ₀ Ω-γ*₀₁ (lamᴺ Aᴺ _ bᴺ) =
      lam-[]* (γ*₀ ⁺^*) ∙ᵈ
      apᵈ-lam₄
        (ap-++ Ω-γ*₀₁)
        ([]ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ Aᴺ)
        ([]ᵛ→⁺^ᵀᵗ₀ (ap-▹ᵀˡ Ω-γ*₀₁ ([]ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ Aᴺ)) bᴺ)
        ([]ᵛ→⁺^ᵗ₀ (ap-▹ᵀˡ Ω-γ*₀₁ ([]ᵛ→⁺^ᵀ₀ Ω-γ*₀₁ Aᴺ)) bᴺ) ∙ᵈ
      symᵈ (lam-[]* (γ*₁ ⁺^*))

  []ᵛ→[]ᵀˡ : Ω [ γ*₀ ]ᵀˡ* ≡ Ω [ γ*₁ ]ᵀˡ*
  []ᵛ→[]ᵀˡ {Ω = ◇} = refl
  []ᵛ→[]ᵀˡ {Ω = Ω ▹ A} = ap-▹ᵀˡ []ᵛ→[]ᵀˡ ([]ᵛ→⁺^ᵀ₀ []ᵛ→[]ᵀˡ (normᵀ A))

  []ᵛ→⁺^ᵀ :
    (Ω : Tel Γ) {A : Ty (Γ ++ Ω) i} →
    A [ γ*₀ ⁺^* ]ᵀ* ≡[ ap-Ty (ap-++ []ᵛ→[]ᵀˡ) ] A [ γ*₁ ⁺^* ]ᵀ*
  []ᵛ→⁺^ᵀ Ω {A} = []ᵛ→⁺^ᵀ₀ []ᵛ→[]ᵀˡ (normᵀ A)

  []ᵛ→⁺^ᵗ :
    (Ω : Tel Γ) {A : Ty (Γ ++ Ω) i} {a : Tm (Γ ++ Ω) A} →
    a [ γ*₀ ⁺^* ]ᵗ* ≡[ ap-Tm₂ (ap-++ []ᵛ→[]ᵀˡ) ([]ᵛ→⁺^ᵀ Ω) ] a [ γ*₁ ⁺^* ]ᵗ*
  []ᵛ→⁺^ᵗ Ω {a} = []ᵛ→⁺^ᵗ₀ []ᵛ→[]ᵀˡ (normᵗ a)

open []ᵛ→⁺^ public

module _ {a : Tm Γ A} {γ : Sub Δ Γ} where
  ⟨⟩-[]ᵛ :
    Var (Γ ▹ A) B b →
    b [ ⟨ a ⟩ ]ᵗ [ γ ]ᵗ ≡[ ap-Tm ⟨⟩-[]ᵀ ] b [ γ ⁺ ]ᵗ [ ⟨ a [ γ ]ᵗ ⟩ ]ᵗ
  ⟨⟩-[]ᵛ vz =
    apᵈ-[]ᵗ p-⟨⟩ᵀ q-⟨⟩ ∙ᵈ symᵈ q-⟨⟩ ∙ᵈ apᵈ-[]ᵗ (sym p-⁺ᵀ) (symᵈ q-⁺)
  ⟨⟩-[]ᵛ (vs cᵛ) =
    apᵈ-[]ᵗ p-⟨⟩ᵀ p-⟨⟩ᵗ ∙ᵈ symᵈ p-⟨⟩ᵗ ∙ᵈ apᵈ-[]ᵗ (sym p-⁺ᵀ) (symᵈ p-⁺ᵗ)

  open []ᵛ→⁺^ (⌜ ⟨ a ⟩ ⌝ ∘ ⌜ γ ⌝) (⌜ γ ⁺ ⌝ ∘ ⌜ ⟨ a [ γ ]ᵗ ⟩ ⌝) ⟨⟩-[]ᵀ ⟨⟩-[]ᵛ
    public using ()
    renaming ([]ᵛ→[]ᵀˡ to ⟨⟩-[]ᵀˡ; []ᵛ→⁺^ᵀ to ⟨⟩-[]ᵀ-⁺^; []ᵛ→⁺^ᵗ to ⟨⟩-[]ᵗ-⁺^)

⟨⟩-[]ᵗ* :
  (γ* : Sub* Δ Γ) →
  b [ ⟨ a ⟩ ]ᵗ [ γ* ]ᵗ* ≡[ ap-Tm (⟨⟩-[]ᵀ* γ*) ]
  b [ γ* ⁺* ]ᵗ* [ ⟨ a [ γ* ]ᵗ* ⟩ ]ᵗ
⟨⟩-[]ᵗ* ⌜ γ ⌝ = ⟨⟩-[]ᵗ-⁺^ ◇
⟨⟩-[]ᵗ* (γ* ∘ δ*) = apᵈ-[]ᵗ* (⟨⟩-[]ᵀ* γ*) (⟨⟩-[]ᵗ* γ*) δ* ∙ᵈ ⟨⟩-[]ᵗ* δ*
⟨⟩-[]ᵗ* id = reflᵈ

module _ {A : Ty Γ i} where
  ▹-ηᵛ : Var (Γ ▹ A) B b → b ≡[ ap-Tm ▹-ηᵀ ] b [ p ⁺ ]ᵗ [ ⟨ q ⟩ ]ᵗ
  ▹-ηᵛ vz = symᵈ q-⟨⟩ ∙ᵈ apᵈ-[]ᵗ (sym p-⁺ᵀ) (symᵈ q-⁺)
  ▹-ηᵛ (vs cᵛ) = symᵈ p-⟨⟩ᵗ ∙ᵈ apᵈ-[]ᵗ (sym p-⁺ᵀ) (symᵈ p-⁺ᵗ)

  open []ᵛ→⁺^ id (⌜ p ⁺ ⌝ ∘ ⌜ ⟨ q ⟩ ⌝) ▹-ηᵀ ▹-ηᵛ public using ()
    renaming ([]ᵛ→[]ᵀˡ to ▹-ηᵀˡ; []ᵛ→⁺^ᵀ to ▹-ηᵀ-⁺^; []ᵛ→⁺^ᵗ to ▹-ηᵗ-⁺^)