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

open import Data.Nat.Base using (ℕ; suc; zero; _≥‴_; _≤‴_; ≤‴-refl; ≤‴-step)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂; trans; sym)
open import Relation.Nullary.Negation.Core using (¬_)


variable
  n m n′ m′ n″ m″ : ℕ
  m≥n m′≥n : m ≥‴ n

≤‴-trans : n′ ≤‴ n → n ≤‴ m → n′ ≤‴ m
≤‴-trans ≤‴-refl n≤m  = n≤m
≤‴-trans (≤‴-step sn′≤m) n≤m = ≤‴-step (≤‴-trans sn′≤m n≤m)

data Type : (n : ℕ) → Set where
  ◯ : Type (suc n) → Type n
  `Bool : Type n
  _⇒_ : Type n → Type n → Type n

variable
  A B A′ B′ : Type n

-- Context
data Context : Set where
  ∅ : Context
  _,_ : (Γ : Context) → (A : Type m) → Context

infixl 5 _,_^_
pattern _,_^_ Γ A m = _,_ {m = m} Γ A 

variable
  Γ Δ Γ′ Δ′ : Context
  Γ₁ Γ₂ Γ₃ : Context

-- Membership
infix 4 Contains
syntax Contains {m = m} Γ A = Γ ∋ A ^ m
data Contains : Context → Type m → Set where
  Z : Γ , A ^ m ∋ A ^ m
  S : (x : Γ ∋ A ^ m) → Γ , A′ ^ m′ ∋ A ^ m

Rename : Context → Context → Set
Rename Γ Γ′ = ∀ {m} {A} → Γ ∋ A ^ m → Γ′ ∋ A ^ m