Lapin0t · December 16, 2021 23:14
diff --git a/test.agda b/test.agda
 module test where

 data ty : Set where
  unit : ty
  _⇒_ : ty → ty → ty

 data env : Set where
  ∅ : env
  _▸_ : env → ty → env

 data _∈_ (x : ty) : env → Set where
  top : ∀ {Γ} → x ∈ (Γ ▸ x)
  pop : ∀ {Γ y} → x ∈ Γ → x ∈ (Γ ▸ y)

 data tm (Γ : env) : ty → Set where
  var : ∀ {a} → a ∈ Γ → tm Γ a
  lam : ∀ {a b} → tm (Γ ▸ a) b → tm Γ (a ⇒ b)
  app : ∀ {a b} → tm Γ (a ⇒ b) → tm Γ a → tm Γ b
  ⋆ : tm Γ unit

 data val (Γ : env) : ty → Set where
  var : ∀ {a} → a ∈ Γ → val Γ a
  lam : ∀ {a b} → tm (Γ ▸ a) b → val Γ (a ⇒ b)
  ⋆ : val Γ unit

 data ctxₑ (Γ : env) (y : ty) : ty → Set where
  □ : ctxₑ Γ y y
  appₗ : ∀ {a b} → ctxₑ Γ y b → tm Γ a → ctxₑ Γ y (a ⇒ b)
  appᵣ : ∀ {a b} → ctxₑ Γ y b → val Γ (a ⇒ b) → ctxₑ Γ y a

 data tmₑ (Γ : env) (x : ty) : Set where
  tval : val Γ x → tmₑ Γ x
  tred : ∀ {a b} → ctxₑ Γ x b → val Γ (a ⇒ b) → val Γ a → tmₑ Γ x

 focus : ∀ {Γ x y} → ctxₑ Γ y x → tm Γ x → tmₑ Γ y
 focus-val : ∀ {Γ x y} → ctxₑ Γ y x → val Γ x → tmₑ Γ y

 focus E (var i)   = focus-val E (var i)
 focus E (lam a)   = focus-val E (lam a)
 focus E (app a b) = focus (appₗ E b) a
 focus E ⋆         = focus-val E ⋆

 focus-val □         v = tval v
 focus-val (appₗ E a) v = focus (appᵣ E v) a
 focus-val (appᵣ E u) v = tred E u v
	module test where

	data ty : Set where
	unit : ty
	_⇒_ : ty → ty → ty

	data env : Set where
	∅ : env
	_▸_ : env → ty → env

	data _∈_ (x : ty) : env → Set where
	top : ∀ {Γ} → x ∈ (Γ ▸ x)
	pop : ∀ {Γ y} → x ∈ Γ → x ∈ (Γ ▸ y)

	data tm (Γ : env) : ty → Set where
	var : ∀ {a} → a ∈ Γ → tm Γ a
	lam : ∀ {a b} → tm (Γ ▸ a) b → tm Γ (a ⇒ b)
	app : ∀ {a b} → tm Γ (a ⇒ b) → tm Γ a → tm Γ b
	⋆ : tm Γ unit

	data val (Γ : env) : ty → Set where
	var : ∀ {a} → a ∈ Γ → val Γ a
	lam : ∀ {a b} → tm (Γ ▸ a) b → val Γ (a ⇒ b)
	⋆ : val Γ unit

	data ctxₑ (Γ : env) (y : ty) : ty → Set where
	□ : ctxₑ Γ y y
	appₗ : ∀ {a b} → ctxₑ Γ y b → tm Γ a → ctxₑ Γ y (a ⇒ b)
	appᵣ : ∀ {a b} → ctxₑ Γ y b → val Γ (a ⇒ b) → ctxₑ Γ y a

	data tmₑ (Γ : env) (x : ty) : Set where
	tval : val Γ x → tmₑ Γ x
	tred : ∀ {a b} → ctxₑ Γ x b → val Γ (a ⇒ b) → val Γ a → tmₑ Γ x

	focus : ∀ {Γ x y} → ctxₑ Γ y x → tm Γ x → tmₑ Γ y
	focus-val : ∀ {Γ x y} → ctxₑ Γ y x → val Γ x → tmₑ Γ y

	focus E (var i) = focus-val E (var i)
	focus E (lam a) = focus-val E (lam a)
	focus E (app a b) = focus (appₗ E b) a
	focus E ⋆ = focus-val E ⋆

	focus-val □ v = tval v
	focus-val (appₗ E a) v = focus (appᵣ E v) a
	focus-val (appᵣ E u) v = tred E u v