module CoDeBruijn where

open import Agda.Builtin.Nat using (Nat; zero; suc; _+_)

ℕ = Nat
variable k l : ℕ

-- A binary sequence of length k containing l 1s
data Filter : (k l : ℕ) → Set where
  done :              Filter      0       0
  yes  : Filter k l → Filter (suc k) (suc l)
  no   : Filter k l → Filter (suc k)      l

data Term : ℕ → Set where
  var  : Term 1
  app  : Term k → Term l → Term (k + l)
  -- Each variable filtered out by the sequence is bound here
  lam  : Filter k l → Term k → Term l

-- λ0
identity : Term 0
identity = lam (no done) var

-- λλ1
const : Term 0
const = lam (no done) (lam (yes done) var)

-- λλλ201
flip : Term 0
flip = 
  lam (no done) (
    lam (no (yes done)) (
      lam (yes (no (yes done))) (
        app (app var var) var
      )
    )
  )