{-# OPTIONS --allow-unsolved-metas #-}

module A201605.AltArtemov.Try3.Prov where

open import A201605.AltArtemov.Try3.True public renaming (ᵗ⌊_⌋ to ᵗ⌊_⌋ᵀ)


-- TODO: unfinished
data Prov (Γ : Cx) : ∀ {n} → Tm ᵍ⌊ Γ ⌋ n → Ty n → Set where
  var  : ∀ {n} {A : Ty n} (x : Var Γ A) →
           Prov Γ (VAR ⁱ⌊ x ⌋) A
  lam  : ∀ {n} {t : Tm (suc ᵍ⌊ Γ ⌋) n} {A B : Ty n} → Prov (Γ , A) t B →
           Prov Γ (LAM t) {!(A ⊃ B)!}
  app  : ∀ {n} {t₁ t₂ : Tm ᵍ⌊ Γ ⌋ n} {A B : Ty n} → Prov Γ t₁ {!A ⊃ B!} → Prov Γ t₂ A →
           Prov Γ (APP t₁ t₂) B
  pair : ∀ {n} {t₁ t₂ : Tm ᵍ⌊ Γ ⌋ n} {A B : Ty n} → Prov Γ t₁ A → Prov Γ t₂ B →
           Prov Γ (PAIR t₁ t₂) {!A ∧ B!}
  fst  : ∀ {n} {t : Tm ᵍ⌊ Γ ⌋ n} {A B : Ty n} → Prov Γ t {!A ∧ B!} →
           Prov Γ (FST t) A
  snd  : ∀ {n} {t : Tm ᵍ⌊ Γ ⌋ n} {A B : Ty n} → Prov Γ t {!A ∧ B!} →
           Prov Γ (SND t) B
  up   : ∀ {n} {t : Tm ᵍ⌊ Γ ⌋ (suc n)} {u : Tm  n} {A : Ty n} → Prov Γ t (u ∶ A) →
           Prov Γ (UP t) (! u ∶ u ∶ A)
  down : ∀ {n} {t : Tm ᵍ⌊ Γ ⌋ (suc n)} {u : Tm  n} {A : Ty n} → Prov Γ t (u ∶ A) →
           Prov Γ (DOWN t) A

ᵗ⌊_⌋ : ∀ {Γ n} {t : Tm ᵍ⌊ Γ ⌋ n} {A : Ty n} → Prov Γ t 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 ⌋

--true⇗ : ∀ {Γ n} {A : Ty n} (j : True Γ A) → Prov Γ ᵗ⌊ j ⌋ᵀ A
--true⇗ (var x)      = var x
--true⇗ (lam j)      = lam (true⇗ j)
--true⇗ (app j₁ j₂)  = app (true⇗ j₁) (true⇗ j₂)
--true⇗ (pair j₁ j₂) = pair (true⇗ j₁) (true⇗ j₂)
--true⇗ (fst j)      = fst (true⇗ j)
--true⇗ (snd j)      = snd (true⇗ j)
--true⇗ (up j)       = up (true⇗ j)
--true⇗ (down j)     = down (true⇗ j)
--
--true⇙ : ∀ {Γ n} {t : Tm ᵍ⌊ Γ ⌋ n} {A : Ty n} (j : Prov Γ t A) → True Γ A
--true⇙ (var x)      = var x
--true⇙ (lam j)      = lam (true⇙ j)
--true⇙ (app j₁ j₂)  = app (true⇙ j₁) (true⇙ j₂)
--true⇙ (pair j₁ j₂) = pair (true⇙ j₁) (true⇙ j₂)
--true⇙ (fst j)      = fst (true⇙ j)
--true⇙ (snd j)      = snd (true⇙ j)
--true⇙ (up j)       = up (true⇙ j)
--true⇙ (down j)     = down (true⇙ j)
--
--true⇗⇙-id : ∀ {Γ n} {A : Ty n} (j : True Γ A) → true⇙ (true⇗ j) ≡ j
--true⇗⇙-id (var x)      = refl
--true⇗⇙-id (lam j)      = cong lam (true⇗⇙-id j)
--true⇗⇙-id (app j₁ j₂)  = cong₂ app (true⇗⇙-id j₁) (true⇗⇙-id j₂)
--true⇗⇙-id (pair j₁ j₂) = cong₂ pair (true⇗⇙-id j₁) (true⇗⇙-id j₂)
--true⇗⇙-id (fst j)      = cong fst (true⇗⇙-id j)
--true⇗⇙-id (snd j)      = cong snd (true⇗⇙-id j)
--true⇗⇙-id (up j)       = cong up (true⇗⇙-id j)
--true⇗⇙-id (down j)     = cong down (true⇗⇙-id j)

-- TODO: unfinished
prov⇗ : ∀ {Γ n} {t : Tm ᵍ⌊ Γ ⌋ n} {A : Ty n} (j : Prov Γ t A) →
           Prov Γ (! ᵗ⌊ j ⌋) (t ∶ A)
prov⇗ (var x)      = {!var x!}
prov⇗ (lam j)      = {!!}
prov⇗ (app j₁ j₂)  = {!!}
prov⇗ (pair j₁ j₂) = {!!}
prov⇗ (fst j)      = fst {!prov⇗ j!}
prov⇗ (snd j)      = {!!}
prov⇗ (up j)       = {!!}
prov⇗ (down j)     = {!!}