module A201605.AltArtemov.Try1.True where

open import A201605.AltArtemov.Try1.Var public


data True (Γ : Cx) : ∀ {n} → Ty n → Set where
  var  : ∀ {n} {A : Ty n} → Var Γ A → True Γ A
  lam  : ∀ {n} {A B : Ty n} → True (Γ , A) B → True Γ (A ⊃ B)
  app  : ∀ {n} {A B : Ty n} → True Γ (A ⊃ B) → True Γ A → True Γ B
  pair : ∀ {n} {A B : Ty n} → True Γ A → True Γ B → True Γ (A ∧ B)
  fst  : ∀ {n} {A B : Ty n} → True Γ (A ∧ B) → True Γ A
  snd  : ∀ {n} {A B : Ty n} → True Γ (A ∧ B) → True Γ B
  up   : ∀ {n} {t : Tm  n} {A : Ty n} → True Γ (t ∶ A) → True Γ (! t ∶ t ∶ A)
  down : ∀ {n} {t : Tm  n} {A : Ty n} → True Γ (t ∶ A) → True Γ A

ᵗ⌊_⌋ : ∀ {Γ n} {A : Ty n} → True Γ A → Tm ᵍ⌊ Γ ⌋ n
ᵗ⌊ var x ⌋      = VAR ⁱ⌊ x ⌋
ᵗ⌊ lam j ⌋      = LAM ᵗ⌊ j ⌋
ᵗ⌊ app j₁ j₂ ⌋  = APP ᵗ⌊ j₁ ⌋ ᵗ⌊ j₂ ⌋
ᵗ⌊ pair j₁ j₂ ⌋ = PAIR ᵗ⌊ j₁ ⌋ ᵗ⌊ j₂ ⌋
ᵗ⌊ fst j ⌋      = FST ᵗ⌊ j ⌋
ᵗ⌊ snd j ⌋      = SND ᵗ⌊ j ⌋
ᵗ⌊ up j ⌋       = UP (! ᵗ⌊ j ⌋)
ᵗ⌊ down j ⌋     = DOWN (¡ ᵗ⌊ j ⌋)

ren-true : ∀ {Γ Γ′ n} {A : Ty n} → Γ′ ⊇ Γ → True Γ A → True Γ′ A
ren-true η (var x)      = var (ren-var η x)
ren-true η (lam j)      = lam (ren-true (lift η) j)
ren-true η (app j₁ j₂)  = app (ren-true η j₁) (ren-true η j₂)
ren-true η (pair j₁ j₂) = pair (ren-true η j₁) (ren-true η j₂)
ren-true η (fst j)      = fst (ren-true η j)
ren-true η (snd j)      = snd (ren-true η j)
ren-true η (up j)       = up (ren-true η j)
ren-true η (down j)     = down (ren-true η j)

wk-true : ∀ {Γ n n′} {A : Ty n} {C : Ty n′} → True Γ C → True (Γ , A) C
wk-true = ren-true ⊇wk

wk*-true : ∀ {Γ n} {C : Ty n} → True ∅ C → True Γ C
wk*-true = ren-true ⊇to

ren-true-id : ∀ {Γ n} {A : Ty n} (j : True Γ A) → ren-true ⊇id j ≡ j
ren-true-id (var x)      = cong var (ren-var-id x)
ren-true-id (lam j)      = cong lam (ren-true-id j)
ren-true-id (app j₁ j₂)  = cong₂ app (ren-true-id j₁) (ren-true-id j₂)
ren-true-id (pair j₁ j₂) = cong₂ pair (ren-true-id j₁) (ren-true-id j₂)
ren-true-id (fst j)      = cong fst (ren-true-id j)
ren-true-id (snd j)      = cong snd (ren-true-id j)
ren-true-id (up j)       = cong up (ren-true-id j)
ren-true-id (down j)     = cong down (ren-true-id j)

ren-true-● : ∀ {Γ Γ′ Γ″ n} {A : Ty n} (η′ : Γ″ ⊇ Γ′) (η : Γ′ ⊇ Γ) (j : True Γ A) →
               ren-true η′ (ren-true η j) ≡ ren-true (η′ ● η) j
ren-true-● η′ η (var x)      = cong var (ren-var-● η′ η x)
ren-true-● η′ η (lam j)      = cong lam (ren-true-● (lift η′) (lift η) j)
ren-true-● η′ η (app j₁ j₂)  = cong₂ app (ren-true-● η′ η j₁) (ren-true-● η′ η j₂)
ren-true-● η′ η (pair j₁ j₂) = cong₂ pair (ren-true-● η′ η j₁) (ren-true-● η′ η j₂)
ren-true-● η′ η (fst j)      = cong fst (ren-true-● η′ η j)
ren-true-● η′ η (snd j)      = cong snd (ren-true-● η′ η j)
ren-true-● η′ η (up j)       = cong up (ren-true-● η′ η j)
ren-true-● η′ η (down j)     = cong down (ren-true-● η′ η j)

v₀ : ∀ {Γ n} {A : Ty n} → True (Γ , A) A
v₀ = var x₀

v₁ : ∀ {Γ n n′} {A : Ty n} {B : Ty n′} → True ((Γ , A) , B) A
v₁ = var x₁

v₂ : ∀ {Γ n n′ n″} {A : Ty n} {B : Ty n′} {C : Ty n″} → True (((Γ , A) , B) , C) A
v₂ = var x₂

I : ∀ {Γ n} {A : Ty n} → True Γ (A ⊃ A)
I = lam v₀

K : ∀ {Γ n} {A B : Ty n} → True Γ (A ⊃ B ⊃ A)
K = lam (lam v₁)

S : ∀ {Γ n} {A B C : Ty n} → True Γ ((A ⊃ B ⊃ C) ⊃ (A ⊃ B) ⊃ A ⊃ C)
S = lam (lam (lam
      (app (app v₂ v₀)
           (app v₁ v₀))))