{-# OPTIONS --without-K --safe #-}

module Unbox.Typ where

open import Lib
open import LibNonEmpty

infixr 5 _⟶_

-- types
data Typ : Set where
  B   : Typ
  _⟶_ : Typ  Typ  Typ
     : Typ  Typ

Ctx : Set
Ctx = List Typ

Ctxs : Set
Ctxs = List⁺ Ctx

variable
  S T U      : Typ
  Γ Γ′ Γ″    : Ctx
  Δ Δ′ Δ″    : Ctx
  Γs Γs′ Γs″ : List Ctx
  Δs Δs′ Δs″ : List Ctx
  Ψ Ψ′ Ψ″ Ψ‴ : Ctxs