Linear lambda calculus in Agda.

Linear.agda

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

module Linear where

open import Data.Bool
open import Data.List
open import Data.Product

Ctx : Set
Ctx = List Bool × List Bool

ε : Ctx
ε = [] , []

ext : Ctx → Ctx
ext (Γ , Γ′) = true ∷ Γ , false ∷ Γ′

data Var : Ctx → Set where
  zero : ∀ {Γ} → Var (true ∷ Γ , false ∷ Γ)
  suc : ∀ {b Γ Γ′} → Var (Γ , Γ′) → Var (b ∷ Γ , b ∷ Γ′)
  
data Term : Ctx → Set where
  ` : ∀ {Γ} → Var Γ → Term Γ
  ƛ : ∀ {Γ} → Term (ext Γ) → Term Γ
  _·_ : ∀ {Γ Γ′ Γ″} → Term (Γ , Γ′) → Term (Γ′ , Γ″) → Term (Γ , Γ″)

infixl 5 _·_

ex₁ : Term ε
ex₁ = ƛ (` zero)

ex₂ : Term ε
ex₂ = ƛ (ƛ (ƛ (` (suc (suc zero)) · ` zero · ` (suc zero))))

_⊆_ : Ctx → Ctx → Set
Γ ⊆ Δ = Var Γ → Var Δ

infix 4 _⊆_

ext-ρ : ∀ {Γ Δ} → Γ ⊆ Δ → ext Γ ⊆ ext Δ 
ext-ρ ρ zero = {!!}