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