module NCILL.Sequent where
open import Data.List
open import NCILL.Types
open import NCILL.Ctx
infix 4 _⊢_
data _⊢_ : Ctx → Ty → Set where
var : ∀ {A}
→ [ A ] ⊢ A
impl-R : ∀ {Γ A B}
→ A ∷ Γ ⊢ B
→ Γ ⊢ (A ⊸ B)
impl-L : ∀ {Γ} Δ₁ {Δ₂ A B C}
→ Γ ⊢ A → Δ₁ ++ B ∷ Δ₂ ⊢ C
→ Δ₁ ++ Γ ++ A ⊸ B ∷ Δ₂ ⊢ C
impl-Rʳ : ∀ {Γ A B}
→ Γ ++ [ A ] ⊢ B
→ Γ ⊢ (A ⊸ʳ B)
impl-Lʳ : ∀ {Γ} (Δ₁ : Ctx) → ∀ {Δ₂ A B C}
→ Γ ⊢ A → Δ₁ ++ B ∷ Δ₂ ⊢ C
→ Δ₁ ++ A ⊸ʳ B ∷ Γ ++ Δ₂ ⊢ C
times-R : ∀ {Γ Δ A B}
→ Γ ⊢ A → Δ ⊢ B
→ Γ ++ Δ ⊢ A ⊗ B
times-L : ∀ Δ₁ {Δ₂ A B C}
→ Δ₁ ++ A ∷ B ∷ Δ₂ ⊢ C
→ Δ₁ ++ A ⊗ B ∷ Δ₂ ⊢ C
plus-R₁ : ∀ {Γ A B}
→ Γ ⊢ A
→ Γ ⊢ A ⊕ B
plus-R₂ : ∀ {Γ A B}
→ Γ ⊢ B
→ Γ ⊢ A ⊕ B
plus-L : ∀ Δ₁ {Δ₂ A B C}
→ Δ₁ ++ A ∷ Δ₂ ⊢ C → Δ₁ ++ B ∷ Δ₂ ⊢ C
→ Δ₁ ++ A ⊕ B ∷ Δ₂ ⊢ C
with-R : ∀ {Γ A B}
→ Γ ⊢ A → Γ ⊢ B
→ Γ ⊢ A & B
with-L₁ : ∀ Δ₁ {Δ₂ A B C}
→ Δ₁ ++ A ∷ Δ₂ ⊢ C
→ Δ₁ ++ A & B ∷ Δ₂ ⊢ C
with-L₂ : ∀ Δ₁ {Δ₂ A B C}
→ Δ₁ ++ B ∷ Δ₂ ⊢ C
→ Δ₁ ++ A & B ∷ Δ₂ ⊢ C
unit-R :
[] ⊢ ♯1
unit-L : ∀ Δ₁ {Δ₂ A}
→ Δ₁ ++ Δ₂ ⊢ A
→ Δ₁ ++ ♯1 ∷ Δ₂ ⊢ A
zero-L : ∀ Δ₁ {Δ₂ A}
→ Δ₁ ++ ♯0 ∷ Δ₂ ⊢ A
top-R : ∀ {Γ}
→ Γ ⊢ ♯⊤
Sqnt : Ctx → Ty → Set
Sqnt Γ A = Γ ⊢ A
app : ∀ {Γ} Δ₁ {Δ₂ A B C}
→ Γ ⊢ A → Δ₁ ++ B ∷ Δ₂ ⊢ C
→ Δ₁ ++ A ⊸ʳ B ∷ Γ ++ Δ₂ ⊢ C
app = impl-Lʳ
lam : ∀ {Γ A B}
→ Γ ++ [ A ] ⊢ B
→ Γ ⊢ (A ⊸ʳ B)
lam = impl-Rʳ