copumpkin · June 12, 2018 20:42
diff --git a/STLC.agda b/STLC.agda
 module STLC where

 -- Simple substitution à la Conor, as described in http://strictlypositive.org/ren-sub.pdf

 id : {A : Set} → A → A
 id x = x

 data Type : Set where
  *   : Type
  _⇒_ : (S T : Type) → Type

 data Context : Set where
  ε   : Context
  _,_ : (Γ : Context) (S : Type) → Context

 data _∋_ : Context → Type → Set where
  here  : ∀ {Γ S} → (Γ , S) ∋ S
  there : ∀ {Γ S T} (i : Γ ∋ S) → (Γ , T) ∋ S

 data Term : Context → Type → Set where
  var : ∀ {Γ S} (v : Γ ∋ S) → Term Γ S
  lam : ∀ {Γ S T} (t : Term (Γ , S) T) → Term Γ (S ⇒ T)
  app : ∀ {Γ S T} (f : Term Γ (S ⇒ T)) (x : Term Γ S) → Term Γ T

 record Kit (_◆_ : Context → Type → Set) : Set where
  constructor kit
  field
    variable : ∀ {Γ T}   → Γ ∋ T → Γ ◆ T
    term     : ∀ {Γ T}   → Γ ◆ T → Term Γ T
    weaken   : ∀ {Γ S T} → Γ ◆ T → (Γ , S) ◆ T

 open Kit

 lift : ∀ {Γ Δ S T _◆_} → Kit _◆_ → (∀ {X} → Γ ∋ X → Δ ◆ X) → (Γ , S) ∋ T → (Δ , S) ◆ T
 lift K τ here      = variable K here
 lift K τ (there v) = weaken K (τ v)

 traverse : ∀ {Γ Δ T _◆_} → Kit _◆_ → (∀ {X} → Γ ∋ X → Δ ◆ X) → Term Γ T → Term Δ T
 traverse K τ (var v)   = term K (τ v)
 traverse K τ (lam t)   = lam (traverse K (lift K τ) t)
 traverse K τ (app f x) = app (traverse K τ f) (traverse K τ x)


 rename : ∀ {Γ Δ T} → (∀ {X} → Γ ∋ X → Δ ∋ X) → Term Γ T → Term Δ T
 rename p t = traverse (kit id var there) p t

 subst : ∀ {Γ Δ T} → (∀ {X} → Γ ∋ X → Term Δ X) → Term Γ T → Term Δ T
 subst σ t = traverse (kit var id (rename there)) σ t

 subst₁ : ∀ {Γ S T} → Term Γ S → Term (Γ , S) T → Term Γ T
 subst₁ {Γ} {S} t = subst f
  where
  f : ∀ {X} → (Γ , S) ∋ X → Term Γ X
  f here = t
  f (there x) = var x


 data Env : Context → Set where
  ε   : Env ε
  _,_ : ∀ {Γ T} (xs : Env Γ) (x : Term Γ T) → Env (Γ , T)

 -- World's slowest full substitution
 subst′ : ∀ {Γ T} → Env Γ → Term Γ T → Term ε T
 subst′ ε t = t
 subst′ (xs , x) t = subst′ xs (subst₁ x t)
	module STLC where

	-- Simple substitution à la Conor, as described in http://strictlypositive.org/ren-sub.pdf

	id : {A : Set} → A → A
	id x = x

	data Type : Set where
	* : Type
	_⇒_ : (S T : Type) → Type

	data Context : Set where
	ε : Context
	_,_ : (Γ : Context) (S : Type) → Context

	data _∋_ : Context → Type → Set where
	here : ∀ {Γ S} → (Γ , S) ∋ S
	there : ∀ {Γ S T} (i : Γ ∋ S) → (Γ , T) ∋ S

	data Term : Context → Type → Set where
	var : ∀ {Γ S} (v : Γ ∋ S) → Term Γ S
	lam : ∀ {Γ S T} (t : Term (Γ , S) T) → Term Γ (S ⇒ T)
	app : ∀ {Γ S T} (f : Term Γ (S ⇒ T)) (x : Term Γ S) → Term Γ T

	record Kit (_◆_ : Context → Type → Set) : Set where
	constructor kit
	field
	variable : ∀ {Γ T} → Γ ∋ T → Γ ◆ T
	term : ∀ {Γ T} → Γ ◆ T → Term Γ T
	weaken : ∀ {Γ S T} → Γ ◆ T → (Γ , S) ◆ T

	open Kit

	lift : ∀ {Γ Δ S T _◆_} → Kit _◆_ → (∀ {X} → Γ ∋ X → Δ ◆ X) → (Γ , S) ∋ T → (Δ , S) ◆ T
	lift K τ here = variable K here
	lift K τ (there v) = weaken K (τ v)

	traverse : ∀ {Γ Δ T _◆_} → Kit _◆_ → (∀ {X} → Γ ∋ X → Δ ◆ X) → Term Γ T → Term Δ T
	traverse K τ (var v) = term K (τ v)
	traverse K τ (lam t) = lam (traverse K (lift K τ) t)
	traverse K τ (app f x) = app (traverse K τ f) (traverse K τ x)


	rename : ∀ {Γ Δ T} → (∀ {X} → Γ ∋ X → Δ ∋ X) → Term Γ T → Term Δ T
	rename p t = traverse (kit id var there) p t

	subst : ∀ {Γ Δ T} → (∀ {X} → Γ ∋ X → Term Δ X) → Term Γ T → Term Δ T
	subst σ t = traverse (kit var id (rename there)) σ t

	subst₁ : ∀ {Γ S T} → Term Γ S → Term (Γ , S) T → Term Γ T
	subst₁ {Γ} {S} t = subst f
	where
	f : ∀ {X} → (Γ , S) ∋ X → Term Γ X
	f here = t
	f (there x) = var x


	data Env : Context → Set where
	ε : Env ε
	_,_ : ∀ {Γ T} (xs : Env Γ) (x : Term Γ T) → Env (Γ , T)

	-- World's slowest full substitution
	subst′ : ∀ {Γ T} → Env Γ → Term Γ T → Term ε T
	subst′ ε t = t
	subst′ (xs , x) t = subst′ xs (subst₁ x t)