{-# OPTIONS --safe #-}
module CtxTyp.Context where

open import Data.Nat.Base using (ℕ; suc; zero; _≥‴_; _≤‴_; ≤‴-refl; ≤‴-step)

data Type (n : ℕ) : Set

open import Data.StagedTree Type renaming (StagedForest to Context; StagedTree to ContextItem) public

variable
  A B A′ B′ : Type n
  Γ Δ Γ′ Δ′ : Context n
  Γ₁ Γ₂ Γ₃ : Context n

infixl 5 _,_^_
pattern _,_^_ Γ A n = Γ ,[ ∅ ⊢ A ^ ≤‴-refl {m = n} ]

-- Type
infixr 7 [_⊢_]⇒_
infixr 8 _▷_
data Type n where
  [_⊢_]⇒_ : (Δ : Context (suc n)) → (A : Type n) → (B : Type n) → Type n
  _▷_ : (Δ : Context (suc n)) → (A : Type n) → Type n
  `Bool : Type n
  ◯ : (A : Type (suc n)) → Type n

infixr 7 _⇒_
pattern _⇒_ A B = [ ∅ ⊢ A ]⇒ B