LCube.agda

import Function
open import Data.Unit.Base hiding (_≤_)
open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.List as L
open import Data.List.Any
open import Data.Fin hiding (_≤_; _<_; _+_)
open import Data.Nat
open import Data.Nat.Properties
open Membership-≡
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary

distinct : ∀{A} → List A → Set
distinct xs = ∀{x y} → (px : x ∈ xs) → (py : y ∈ xs) → x ≡ y → index px ≡ index py

data Idt : Set where
  idt : ℕ → Idt

unidt : Idt → ℕ
unidt = (λ x → Function.case x of λ { (idt n) → n })

record PTS : Set₁ where
  constructor λₚ_,_,_
  field
    sorts : Set
    axioms : List (sorts × sorts)
    rules : List (sorts × sorts × sorts)

  -- pseudo-terms
  data PTerm : Set where
    var : Idt → PTerm
    const : sorts → PTerm
    app : PTerm → PTerm → PTerm
    abs : PTerm → (Idt → PTerm) → PTerm
    prod : PTerm → (Idt → PTerm) → PTerm

  syntax abs A (λ x → B) = λ[ x ∶ A ] B
  syntax prod A (λ x → B) = Π[ x ∶ A ] B

  Context : Set
  Context = List (Idt × PTerm)

  isfresh : Idt → Context → Set
  isfresh x Γ = ∀{t} → (x , t) ∉ Γ

  data _⊢_∶_ : Context → PTerm → PTerm → Set where
    jaxioms : ∀{c s} → (c , s) ∈ axioms → [] ⊢ const c ∶ const s
    jstart : ∀{Γ A s x} → isfresh x Γ → Γ ⊢ A ∶ const s → ((x , A) ∷ Γ) ⊢ var x ∶ A
    jweak : ∀{Γ A B C s x} → isfresh x Γ → Γ ⊢ A ∶ B → Γ ⊢ C ∶ const s → ((x , C) ∷ Γ) ⊢ A ∶ B
    jprod : ∀{Γ A B s₁ s₂ s₃ x} → (s₁ , s₂ , s₃) ∈ rules → Γ ⊢ A ∶ const s₁ → ((x , A) ∷ Γ) ⊢ B ∶ const s₂ → Γ ⊢ (Π[ x ∶ A ] B) ∶ const s₃
    japp : ∀{Γ F a A} {B : PTerm → PTerm} → Γ ⊢ F ∶ (Π[ x ∶ A ] (B (var x))) → Γ ⊢ a ∶ A → Γ ⊢ app F a ∶ (B a)
    jabs : ∀{Γ A B x b s} → ((x , A) ∷ Γ) ⊢ b ∶ B → Γ ⊢ (Π[ x ∶ A ] B) ∶ const s → Γ ⊢ (λ[ x ∶ A ] b) ∶ (Π[ x ∶ A ] B)
    jconv : ∀{Γ A B B' s} → Γ ⊢ A ∶ B → Γ ⊢ B' ∶ const s → B ≡ B' → Γ ⊢ A ∶ B'
open PTS

r2 : ∀{X : Set} → X × X → X × X × X
r2 (a , b) = (a , b , b)

isfull : PTS → Set
isfull (λₚ S , A , R) = ∀(s₁ s₂ : S) → r2 (s₁ , s₂) ∈ R

module λ-cube where
  ⋆ : Fin 2
  ⋆ = zero

  □ : Fin 2
  □ = suc zero

  PTS-extend : (P : PTS) → sorts P × sorts P → PTS
  PTS-extend (λₚ S , A , R) q = λₚ S , A , (r2 q ∷ R)

  λ→ : PTS
  λ→ = λₚ (Fin 2) , [(⋆ , □)] , (r2 (⋆ , ⋆) ∷ [])

  λ2 : PTS
  λ2 = PTS-extend λ→ (□ , ⋆)

  λP : PTS
  λP = PTS-extend λ→ (⋆ , □)

  λ⍹ : PTS
  λ⍹ = PTS-extend λ→ (□ , □)

  λP2 : PTS
  λP2 = PTS-extend λP (□ , ⋆)

  λ⍵ : PTS
  λ⍵ = PTS-extend λ⍹ (□ , ⋆)

  λP⍹ : PTS
  λP⍹ = PTS-extend λP (□ , □)

  λC : PTS
  λC = PTS-extend λP⍹ (□ , ⋆)

PTS-judge : (P : PTS) → Context P → PTerm P → PTerm P → Set
PTS-judge P Γ x A = _⊢_∶_ P Γ x A

syntax PTS-judge P Γ x A = Γ ⊢[ P ] x ∶ A

PTS-judge-triple : (P : PTS) → Context P → PTerm P → PTerm P → PTerm P → Set
PTS-judge-triple P Γ A B C = (Γ ⊢[ P ] A ∶ B) × (Γ ⊢[ P ] B ∶ C)

syntax PTS-judge-triple P Γ A B C = Γ ⊢[ P ] A ∶ B ∶ C

module Definitions (L : PTS) where
  [_]-legal : Context L → Set
  [ Γ ]-legal = ∃ λ P → ∃ λ Q → Γ ⊢[ L ] P ∶ Q

  ctx-legal-witness : ∀{Γ P Q} → Γ ⊢[ L ] P ∶ Q → [ Γ ]-legal
  ctx-legal-witness {Γ} {P} {Q} dr = P , Q , dr

  [_]-term : Context L → PTerm L → Set
  [ Γ ]-term A = ∃ λ B → (Γ ⊢[ L ] A ∶ B) × (Γ ⊢[ L ] B ∶ A)

  [_]-type : Context L → PTerm L → Set
  [ Γ ]-type A = ∃ λ s → Γ ⊢[ L ] A ∶ const s

  [_]-type-of-sort-[_] : Context L → sorts L → PTerm L → Set
  [ Γ ]-type-of-sort-[ s ] A = Γ ⊢[ L ] A ∶ const s

  [_]-element : Context L → PTerm L → Set
  [ Γ ]-element A = ∃ λ B → ∃ λ s → Γ ⊢[ L ] A ∶ B ∶ const s

  [_]-element-of-type-[_]-of-sort-[_] : Context L → PTerm L → sorts L → PTerm L → Set
  [ Γ ]-element-of-type-[ B ]-of-sort-[ s ] A = Γ ⊢[ L ] A ∶ B ∶ const s

  legal : PTerm L → Set
  legal A = ∃ λ Γ → ∃ λ B → (Γ ⊢[ L ] A ∶ B) ⊎ (Γ ⊢[ L ] B ∶ A)

  _↾_ : Context L → ℕ → Context L
  Γ ↾ i = take i Γ

  _≤ₛ_ : Context L → Context L → Set
  Γ ≤ₛ Δ = ∃ λ j → (j ≤ length Δ) × (Γ ≡ Δ ↾ j)

  judge-all : Context L → Context L → Set
  judge-all Γ [] = ⊤
  judge-all Γ ((uₙ , Bₙ) ∷ Δ) = (Γ ⊢[ L ] var uₙ ∶ Bₙ) × judge-all Γ Δ

  legal-cons : ∀{Γ x A s} → Γ ⊢[ L ] A ∶ const s → isfresh L x Γ → [ Γ ]-legal → [ (x , A) ∷ Γ ]-legal
  legal-cons dr f g = (proj₁ g) , (proj₁ (proj₂ g) , jweak f (proj₂ (proj₂ g)) dr)

  judge-all-cons-f : ∀{Γ Δ A B s} → isfresh L A Γ → Γ ⊢[ L ] B ∶ const s → judge-all Γ Δ → judge-all ((A , B) ∷ Γ) Δ
  judge-all-cons-f {Δ = []} f dr j = tt
  judge-all-cons-f {Δ = (C , D) ∷ Δ} f dr j = jweak f (proj₁ j) dr , judge-all-cons-f f dr (proj₂ j)

  judge-all-cons : ∀{Γ Δ A B s} → isfresh L A Γ → Γ ⊢[ L ] B ∶ const s → judge-all Γ Δ → judge-all ((A , B) ∷ Γ) ((A , B) ∷ Δ)
  judge-all-cons {Δ = Δ} f dr j = (jstart f dr) , judge-all-cons-f f dr j

module coherence (L : PTS) where
  open Definitions L

  legal-type : ∀{Γ x A} → [((x , A) ∷ Γ)]-legal → [ Γ ]-type A
  legal-type {Γ} {x} {A} le = lem (proj₂ (proj₂ le)) where
    lem : ∀{Γ x A P Q} → (x , A) ∷ Γ ⊢[ L ] P ∶ Q → [ Γ ]-type A
    lem (jstart {s = s} x₂ dr) = s , dr
    lem (jweak {s = s} x₂ dr dr₁) = s , dr₁
    lem (jprod x₃ dr dr₁) = lem dr
    lem (japp dr dr₁) = lem dr₁
    lem (jabs dr dr₁) = lem dr₁
    lem (jconv dr dr₁ x₂) = lem dr₁

  legal-fresh : ∀{Γ x A} → [((x , A) ∷ Γ)]-legal → isfresh L x Γ
  legal-fresh le = ctx-cons-fresh (proj₂ (proj₂ le)) where
    ctx-cons-fresh : ∀{Γ x A P Q} → (x , A) ∷ Γ ⊢[ L ] P ∶ Q → isfresh L x Γ
    ctx-cons-fresh (jstart x₁ le₁) = x₁
    ctx-cons-fresh (jweak x₁ le₁ le₂) = x₁
    ctx-cons-fresh (jprod x₂ le₁ le₂) = ctx-cons-fresh le₁
    ctx-cons-fresh (japp le₁ le₂) = ctx-cons-fresh le₂
    ctx-cons-fresh (jabs le₁ le₂) = ctx-cons-fresh le₂
    ctx-cons-fresh (jconv le₁ le₂ x₁) = ctx-cons-fresh le₂

{-
  constf : PTerm L → Set
  constf (const _) = ⊤
  constf _ = ⊥

  type-con : ∀{Γ P Q} → ¬ (constf Q) →
    (Γ ⊢[ L ] P ∶ Q) →
    ∃ λ s → (Γ ⊢[ L ] Q ∶ const s)
  type-con nq (jaxioms _) = {!!}
  type-con nq (jstart {s = s} x₁ dr) = s , jweak x₁ dr dr
  type-con nq (jweak {s = s} x₁ dr dr₁) = let (s' , dr') = type-con nq dr in s' , jweak x₁ dr' dr₁
  type-con nq (jprod x₁ dr dr₁) = ⊥-elim (nq tt)
  type-con nq (japp dr dr₁) = {! !}
  type-con nq (jabs dr dr₁) = {!!}
  type-con nq (jconv dr dr₁ x) = {!!}
-}

{-
  prod-legal : ∀{Γ F A B} →
    (Γ ⊢[ L ] F ∶ (Π[ x ∶ A ] B)) →
    ∃ λ s →
    (Γ ⊢[ L ] (Π[ x ∶ A ] B) ∶ const s)
  prod-legal {(x , C) ∷ Γ} {app F₂ a} {A} {B a} (jweak _ _ _) = {!!}
  prod-legal {Γ} {F} {A} {B} dr = {!!}
-}

{-
  nvar-prod : ∀{Γ F s A} {B : PTerm L → PTerm L} →
    (Γ ⊢[ L ] (Π[ x ∶ A ] (B (var x))) ∶ const s) →
    (Γ ⊢[ L ] F ∶ (Π[ x ∶ A ] (B (var x)))) →
    ∃ λ y → isfresh L y Γ × (Γ ⊢[ L ] F ∶ (Π[ y ∶ A ] (B (var y))))
-}
data sig (A : Set) (B : A → Set) : Set where
  exist : ∀ (x : A) → B x → sig A B

p1 : ∀{A B} → sig A B → A
p1 (exist x px) = x

module α-trans (L : PTS) where
  map-resp-∉ : ∀{A B : Set} {f : A → B} {ys : List A} {y} → f y ∉ L.map f ys → y ∉ ys
  map-resp-∉ {ys = []} fy-∉ ()
  map-resp-∉ {ys = y ∷ ys} {.y} fy-∉ (here refl) = fy-∉ (here refl)
  map-resp-∉ {ys = x ∷ ys} fy-∉ (there x₁) = map-resp-∉ {ys = ys} (λ fy-∈-ys → fy-∉ (there fy-∈-ys)) x₁

  nvar : (xs : List Idt) → ∃ λ y → y ∉ xs
  nvar xs = (idt (suc (sum ys))) , map-resp-∉ {f = unidt} v-ub-∉ where
    ys = L.map unidt xs

    v-ub : ∀{y ys} → y ∈ ys → y ≤ sum ys
    v-ub (here {w} {xs} px) rewrite px = m≤m+n w (sum xs)
    v-ub {y} .{x ∷ xs} (there {x} {xs} x₁) = begin
      y ≤⟨ n≤m+n x y ⟩
      x + y ≤⟨ (DecTotalOrder.refl decTotalOrder) {x = x} +-mono v-ub {y = y} {xs} x₁ ⟩
      x + sum xs ≡⟨ refl ⟩
      sum (x ∷ xs) ∎
      where open ≤-Reasoning

    v-ub-≢ : ∀{y : ℕ} {ys} → y ∈ ys → y ≢ suc (sum ys)
    v-ub-≢ y-in y-eq rewrite y-eq = 1+n≰n (v-ub y-in)

    v-ub-∉ : ∀{ys : List ℕ} → suc (sum ys) ∉ ys
    v-ub-∉ = λ y-in → v-ub-≢ y-in refl

  fvar : (Γ : Context L) → ∃ λ x → isfresh L x Γ
  fvar Γ = proj₁ (nvar vars) , (λ xt-∈ → map-resp-∉ (proj₂ (nvar vars)) xt-∈) where
    vars = L.map proj₁ Γ

  nvar-prod : ∀{Γ F s A} {B : PTerm L → PTerm L} →
    (Γ ⊢[ L ] (Π[ x ∶ A ] (B (var x))) ∶ const s) →
    (Γ ⊢[ L ] F ∶ (Π[ x ∶ A ] (B (var x)))) →
    ∃ λ y → isfresh L y Γ × (Γ ⊢[ L ] F ∶ (Π[ y ∶ A ] (B (var y))))
  nvar-prod {Γ} p dr = proj₁ (fvar Γ) , (proj₂ (fvar Γ)) , (jconv dr p refl)

{-
  trl : ∀{Γ Δ A B} → [ Γ ]-legal → [ Δ ]-legal → judge-all Γ Δ → Δ ⊢[ L ] A ∶ B → Γ ⊢[ L ] A ∶ B
  trl g d tt (jaxioms x) = proj₁ (stl {x = idt zero} {proj₁ d} g) x
  trl g d j (jstart x₁ dr) = proj₁ j
  trl {Δ = (x , C) ∷ Δ} g d j (jweak {s = s} x₁ dr dr₁) = trl (var x , C , proj₁ j) (C , const s , dr₁) (proj₂ j) dr
  trl {Γ} {Δ} g d j (jprod {A = A} {x = x} x₁ dr dr₁) = jprod x₁ (proj₂ A-wf) (trl Γ⁺-legal (ctx-legal-witness dr₁) j' dr₁)
-}

  α-induction : ∀{P : ∀{Γ A B} → Γ ⊢[ L ] A ∶ B → Set} →
    -- axioms
    (∀{c s} → (p : (c , s) ∈ axioms L) → P (jaxioms p)) →
    -- start
    (∀{Γ x A s} → (xf : isfresh L x Γ) → (dr : Γ ⊢[ L ] A ∶ const s) → P (jstart xf dr)) →
    -- weakening
    (∀{Γ A B C x s} → (xf : isfresh L x Γ) → (dr : Γ ⊢[ L ] A ∶ B) → (dr₂ : Γ ⊢[ L ] C ∶ const s) → P (jweak xf dr dr₂)) →
    -- product
    (∀{Γ A B x s₁ s₂ s₃} → (xf : isfresh L x Γ) → (r : (s₁ , s₂ , s₃) ∈ rules L) → (dr : Γ ⊢[ L ] A ∶ const s₁) → (dr₂ : (x , A) ∷ Γ ⊢[ L ] B ∶ const s₂) → P (jprod r dr dr₂)) →
    -- application
    (∀{Γ F A} {B : PTerm L → PTerm L} {a} → (dr : Γ ⊢[ L ] F ∶ (Π[ x ∶ A ] B (var x))) → (dr₂ : Γ ⊢[ L ] a ∶ A) → P (japp {B = B} dr dr₂)) →
    -- abstraction
    (∀{Γ A B s x b} → (dr : (x , A) ∷ Γ ⊢[ L ] b ∶ B) → (dr₂ : Γ ⊢[ L ] (Π[ x ∶ A ] B) ∶ const s) → P (jabs dr dr₂)) →
    -- conversion
    (∀{Γ A B B' s} → (dr : Γ ⊢[ L ] A ∶ B) → (dr₂ : Γ ⊢[ L ] B' ∶ const s) → (eq : B ≡ B') → P (jconv dr dr₂ eq)) →
    ∀{Γ A B} (g : Γ ⊢[ L ] A ∶ B) → P g
  α-induction paxioms pstart pweak pprod papp pabs pconv g with g
  ... | jaxioms x = paxioms x
  ... | jstart x₁ g' = pstart x₁ g'
  ... | jweak x₁ g' g'' = pweak x₁ g' g''
  ... | jprod {Γ = Γ} x₁ g' g'' = {!!}
  ... | japp g' g'' = papp g' g''
  ... | jabs g' g'' = pabs g' g''
  ... | jconv g' g'' x = pconv g' g'' x

{-
  

  α-induction : ∀{P : Set → Set} →
    -- axioms
    (∀{c s} → (c , s) ∈ axioms L → P ([] ⊢[ L ] const c ∶ const s)) →
    -- start
    (∀{Γ x A s} → P (Γ ⊢[ L ] A ∶ const s) → P ((x , A) ∷ Γ ⊢[ L ] var x ∶ A)) →
    -- weakening
    (∀{Γ A B C x s} → P (Γ ⊢[ L ] A ∶ B) → P (Γ ⊢[ L ] C ∶ const s) → P ((x , C) ∷ Γ ⊢[ L ] A ∶ B)) →
    -- product
    (∀{Γ A B x s₁ s₂ s₃} → P (Γ ⊢[ L ] A ∶ const s₁) → P ((x , A) ∷ Γ ⊢[ L ] B ∶ const s₂) → P (Γ ⊢[ L ] (Π[ x ∶ A ] B) ∶ const s₃)) →
    -- application
    (∀{Γ F a A} {B : PTerm L → PTerm L} → P (Γ ⊢[ L ] F ∶ (Π[ x ∶ A ] B (var x)) → P (Γ ⊢[ L ] a ∶ A) → P (Γ ⊢[ L ] app F a ∶ B a))) →
    -- abstraction
    (∀{Γ A} {B : PTerm L → PTerm L} {b x s} → P ((x , A) ∷ Γ ⊢[ L ] b ∶ B (var x)) → P (Γ ⊢[ L ] (Π[ x ∶ A ] B (var x)) ∶ const s) → P (Γ ⊢[ L ] (λ[ x ∶ A ] b) ∶ (Π[ x ∶ A ] B (var x)))) →
    -- conversion
    (∀{Γ A B B' s} → P (Γ ⊢[ L ] A ∶ B) → P (Γ ⊢[ L ] B' ∶ const s) → B ≡ B' → P (Γ ⊢[ L ] A ∶ B')) →
    ∀{Γ A B} → Γ ⊢[ L ] A ∶ B → P (Γ ⊢[ L ] A ∶ B)
  α-induction pax pst pwk ppr pap pab pcv (jaxioms x) = pax x
  α-induction pax pst pwk ppr pap pab pcv (jstart x₁ dr) = pst {! dr!}
  α-induction pax pst pwk ppr pap pab pcv (jweak x₁ dr dr₁) = {! pwk!}
  α-induction pax pst pwk ppr pap pab pcv (jprod x₁ dr dr₁) = {! ppr!}
  α-induction pax pst pwk ppr pap pab pcv (japp dr dr₁) = {! pap!}
  α-induction pax pst pwk ppr pap pab pcv (jabs dr dr₁) = pab {! dr!} {! dr!}
  α-induction pax pst pwk ppr pap pab pcv (jconv dr dr₁ x) = {! jconv!}
-}

module In-PTS (L : PTS) where
  open Definitions L
  open α-trans L

  -- Free variable lemma for PTS's
--  fvl-1 : ∀{Γ} → (g : [ Γ ]-legal) → distinct Γ
--  fvl-1 = _

  -- Start lemma for PTS's
  stl : ∀{Γ c s x A} → [ Γ ]-legal → ((c , s) ∈ axioms L → Γ ⊢[ L ] const c ∶ const s) × ((x , A) ∈ Γ → Γ ⊢[ L ] var x ∶ A)
  stl {Γ} {c} {s} g = (λ t → stl-1 t (proj₂ (proj₂ g))) , (λ t → stl-2 t (proj₂ (proj₂ g)))
    where
      P = proj₁ g
      Q = proj₁ (proj₂ g)

      stl-1 : ∀{Γ P Q} → (c , s) ∈ axioms L → Γ ⊢[ L ] P ∶ Q → Γ ⊢[ L ] const c ∶ const s
      stl-1 cs-in (jaxioms cs2-in) = jaxioms cs-in
      stl-1 cs-in (jstart x₁ dr) = jweak x₁ (stl-1 cs-in dr) dr
      stl-1 cs-in (jweak x₁ dr dr₁) = jweak x₁ (stl-1 cs-in dr₁) dr₁
      stl-1 cs-in (jprod x₁ dr dr₁) = stl-1 cs-in dr
      stl-1 cs-in (japp dr dr₁) = stl-1 cs-in dr₁
      stl-1 cs-in (jabs dr dr₁) = stl-1 cs-in dr₁
      stl-1 cs-in (jconv dr dr₁ x) = stl-1 cs-in dr₁

      stl-2 : ∀{Γ x A P Q} → (x , A) ∈ Γ → Γ ⊢[ L ] P ∶ Q → Γ ⊢[ L ] var x ∶ A
      stl-2 () (jaxioms x₁)
      stl-2 (here refl) (jstart x₂ d) = jstart x₂ d
      stl-2 (there xA-in) (jstart x₂ d) = jweak x₂ (stl-2 xA-in d) d
      stl-2 (here refl) (jweak x₂ d d₁) = jstart x₂ d₁
      stl-2 (there xA-in) (jweak x₂ d d₁) = jweak x₂ (stl-2 xA-in d₁) d₁
      stl-2 xA-in (jprod x₂ d d₁) = stl-2 xA-in d
      stl-2 xA-in (japp d d₁) = stl-2 xA-in d₁
      stl-2 xA-in (jabs d d₁) = stl-2 xA-in d₁
      stl-2 xA-in (jconv d d₁ x₁) = stl-2 xA-in d₁

  -- Transitivity lemma for PTS's
  trl : ∀{Γ Δ A B} → [ Γ ]-legal → [ Δ ]-legal → judge-all Γ Δ → Δ ⊢[ L ] A ∶ B → Γ ⊢[ L ] A ∶ B
  trl g d tt (jaxioms x) = proj₁ (stl {x = idt zero} {proj₁ d} g) x
  trl g d j (jstart x₁ dr) = proj₁ j
  trl {Δ = (x , C) ∷ Δ} g d j (jweak {s = s} x₁ dr dr₁) = trl (var x , C , proj₁ j) (C , const s , dr₁) (proj₂ j) dr
  trl {Γ} {Δ} g d j (jprod {A = A} {x = x} x₁ dr dr₁) = jprod x₁ (proj₂ A-wf) (trl Γ⁺-legal (ctx-legal-witness dr₁) j' dr₁)
    where
      A-wf : [ Γ ]-type A
      A-wf = _ , (trl g d j dr)

      Γ⁺-legal : [((x , A) ∷ Γ)]-legal
      Γ⁺-legal = var x , A , {!!} --jstart {! proj₂ A-wf!} (proj₂ A-wf)
        where

      j' : judge-all ((x , A) ∷ Γ) ((x , A) ∷ Δ)
      j' = judge-all-cons ({! dr₁!}) (proj₂ A-wf) j

{-
  nvar-prod : ∀{Γ F s A} {B : PTerm L → PTerm L} →
    (Γ ⊢[ L ] (Π[ x ∶ A ] (B (var x))) ∶ const s) →
    (Γ ⊢[ L ] F ∶ (Π[ x ∶ A ] (B (var x)))) →
    ∃ λ y → isfresh L y Γ × (Γ ⊢[ L ] F ∶ (Π[ y ∶ A ] (B (var y))))

-}


{-
  legal-coherent-fresh : ∀{Γ x A} → [((x , A) ∷ Γ)]-legal → isfresh L x Γ

  legal-cons : ∀{Γ x A s} → Γ ⊢[ L ] A ∶ const s → isfresh L x Γ → [ Γ ]-legal → [ (x , A) ∷ Γ ]-legal
  legal-cons dr f g = (proj₁ g) , (proj₁ (proj₂ g) , jweak f (proj₂ (proj₂ g)) dr)

-}

  --jprod {x = x} x₁ (trl g d j dr) (trl (proj₁ g , (proj₁ (proj₂ g)) , jweak {!!} (proj₂ (proj₂ g)) {! !}) {!!} ((jstart {!!} {!!}) , {!!}) dr₁)
  trl g d j (japp {a} {A = A} dr dr₁) = {!!}
  trl g d j (jabs dr dr₁) = {!!}
  trl g d j (jconv dr dr₁ x) = {!!}
--   stl : ∀{Γ c s x A} → [ Γ ]-legal → ((c , s) ∈ axioms L → Γ ⊢[ L ] const c ∶ const s) × ((x , A) ∈ Γ → Γ ⊢[ L ] var x ∶ A)

{-
  data _⊢_∶_ : Context → PTerm → PTerm → Set where
    jaxioms : ∀{c s} → (c , s) ∈ axioms  → [] ⊢ const c ∶ const s
    jstart : ∀{Γ A s x} → isfresh x Γ → Γ ⊢ A ∶ const s → ((x , A) ∷ Γ) ⊢ var x ∶ A
    jweak : ∀{Γ A B C s x} → isfresh x Γ → Γ ⊢ A ∶ B → Γ ⊢ C ∶ const s → ((x , C) ∷ Γ) ⊢ A ∶ B
    jprod : ∀{Γ A B s₁ s₂ s₃ x} → (s₁ , s₂ , s₃) ∈ rules → Γ ⊢ A ∶ const s₁ → ((x , A) ∷ Γ) ⊢ B ∶ const s₂ → Γ ⊢ (Π[ x ∶ A ] B) ∶ const s₃
    japp : ∀{Γ F A a} {x : Idt} {B : PTerm → PTerm} → Γ ⊢ F ∶ (Π[ x ∶ A ] (B (var x))) → Γ ⊢ a ∶ A → Γ ⊢ app F a ∶ (B a)
    jabs : ∀{Γ A B x b s} → ((x , A) ∷ Γ) ⊢ b ∶ B → Γ ⊢ (Π[ x ∶ A ] B) ∶ const s → Γ ⊢ (λ[ x ∶ A ] b) ∶ (Π[ x ∶ A ] B)
    jconv : ∀{Γ A B B' s} → Γ ⊢ A ∶ B → Γ ⊢ B' ∶ const s → B ≡ B' → Γ ⊢ A ∶ B'
open PTS

-}