```module Exam where
```

IMPORTANT For ease of marking, when modifying the given code please write

``````-- begin
-- end``````

## Imports

```import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _<_; _≤_; _≤?_; z≤n; s≤s)
open import Data.List using (List; []; _∷_; _++_)
open import Data.Product using (∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.String using (String; _≟_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (False; toWitnessFalse)
```

## Problem 1

```module Problem1 where

open import Function using (_∘_)
```

Remember to indent all code by two spaces.

## Problem 2

Remember to indent all code by two spaces.

```module Problem2 where
```

### Infix declarations

```  infix  4 _⊢_
infix  4 _∋_
infixl 5 _,_

infixr 7 _⇒_

infix  5 ƛ_
infix  5 μ_
infixl 7 _·_
infix  8 `suc_
infix  9 `_
infix  9 S_
```

### Types and contexts

```  data Type : Set where
_⇒_   : Type → Type → Type
`ℕ    : Type

data Context : Set where
∅   : Context
_,_ : Context → Type → Context
```

### Variables and the lookup judgment

```  data _∋_ : Context → Type → Set where

Z : ∀ {Γ A}
----------
→ Γ , A ∋ A

S_ : ∀ {Γ A B}
→ Γ ∋ A
---------
→ Γ , B ∋ A
```

### Terms and the typing judgment

```  data _⊢_ : Context → Type → Set where

`_ : ∀ {Γ} {A}
→ Γ ∋ A
------
→ Γ ⊢ A

ƛ_  :  ∀ {Γ} {A B}
→ Γ , A ⊢ B
----------
→ Γ ⊢ A ⇒ B

_·_ : ∀ {Γ} {A B}
→ Γ ⊢ A ⇒ B
→ Γ ⊢ A
----------
→ Γ ⊢ B

`zero : ∀ {Γ}
----------
→ Γ ⊢ `ℕ

`suc_ : ∀ {Γ}
→ Γ ⊢ `ℕ
-------
→ Γ ⊢ `ℕ

case : ∀ {Γ A}
→ Γ ⊢ `ℕ
→ Γ ⊢ A
→ Γ , `ℕ ⊢ A
-----------
→ Γ ⊢ A

μ_ : ∀ {Γ A}
→ Γ , A ⊢ A
----------
→ Γ ⊢ A
```

### Renaming

```  ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
-----------------------------------
→ (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
ext ρ Z      =  Z
ext ρ (S x)  =  S (ρ x)

rename : ∀ {Γ Δ}
→ (∀ {A} → Γ ∋ A → Δ ∋ A)
------------------------
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename ρ (` x)          =  ` (ρ x)
rename ρ (ƛ N)          =  ƛ (rename (ext ρ) N)
rename ρ (L · M)        =  (rename ρ L) · (rename ρ M)
rename ρ (`zero)        =  `zero
rename ρ (`suc M)       =  `suc (rename ρ M)
rename ρ (case L M N)   =  case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
rename ρ (μ N)          =  μ (rename (ext ρ) N)
```

### Simultaneous Substitution

```  exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A)
----------------------------------
→ (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
exts σ Z      =  ` Z
exts σ (S x)  =  rename S_ (σ x)

subst : ∀ {Γ Δ}
→ (∀ {A} → Γ ∋ A → Δ ⊢ A)
------------------------
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
subst σ (` k)          =  σ k
subst σ (ƛ N)          =  ƛ (subst (exts σ) N)
subst σ (L · M)        =  (subst σ L) · (subst σ M)
subst σ (`zero)        =  `zero
subst σ (`suc M)       =  `suc (subst σ M)
subst σ (case L M N)   =  case (subst σ L) (subst σ M) (subst (exts σ) N)
subst σ (μ N)          =  μ (subst (exts σ) N)
```

### Single and double substitution

```  _[_] : ∀ {Γ A B}
→ Γ , A ⊢ B
→ Γ ⊢ A
---------
→ Γ ⊢ B
_[_] {Γ} {A} {B} N V =  subst {Γ , A} {Γ} σ {B} N
where
σ : ∀ {B} → Γ , A ∋ B → Γ ⊢ B
σ Z      =  V
σ (S x)  =  ` x

_[_][_] : ∀ {Γ A B C}
→ Γ , A , B ⊢ C
→ Γ ⊢ A
→ Γ ⊢ B
---------
→ Γ ⊢ C
_[_][_] {Γ} {A} {B} {C} N V W =  subst {Γ , A , B} {Γ} σ {C} N
where
σ : ∀ {C} → Γ , A , B ∋ C → Γ ⊢ C
σ Z          =  W
σ (S Z)      =  V
σ (S (S x))  =  ` x
```

### Values

```  data Value : ∀ {Γ A} → Γ ⊢ A → Set where

V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
---------------------------
→ Value (ƛ N)

V-zero : ∀ {Γ}
-----------------
→ Value (`zero {Γ})

V-suc : ∀ {Γ} {V : Γ ⊢ `ℕ}
→ Value V
--------------
→ Value (`suc V)
```

### Reduction

```  infix 2 _—→_

data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where

ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
→ L —→ L′
-----------------
→ L · M —→ L′ · M

ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
→ Value V
→ M —→ M′
--------------
→ V · M —→ V · M′

β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
→ Value W
-------------------
→ (ƛ N) · W —→ N [ W ]

ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
→ M —→ M′
----------------
→ `suc M —→ `suc M′

ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
→ L —→ L′
--------------------------
→ case L M N —→ case L′ M N

β-zero :  ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
-------------------
→ case `zero M N —→ M

β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
→ Value V
-----------------------------
→ case (`suc V) M N —→ N [ V ]

β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
---------------
→ μ N —→ N [ μ N ]
```

### Reflexive and transitive closure

```  infix  2 _—↠_
infix  1 begin_
infixr 2 _—→⟨_⟩_
infix  3 _∎

data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where

_∎ : (M : Γ ⊢ A)
------
→ M —↠ M

step—→ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
→ M —↠ N
→ L —→ M
------
→ L —↠ N

pattern _—→⟨_⟩_ L L—→M M—↠N = step—→ L M—↠N L—→M

begin_ : ∀ {Γ A} {M N : Γ ⊢ A}
→ M —↠ N
------
→ M —↠ N
begin M—↠N = M—↠N
```

### Progress

```  data Progress {A} (M : ∅ ⊢ A) : Set where

step : ∀ {N : ∅ ⊢ A}
→ M —→ N
-------------
→ Progress M

done :
Value M
----------
→ Progress M

progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
progress (` ())
progress (ƛ N)                          =  done V-ƛ
progress (L · M) with progress L
...    | step L—→L′                     =  step (ξ-·₁ L—→L′)
...    | done V-ƛ with progress M
...        | step M—→M′                 =  step (ξ-·₂ V-ƛ M—→M′)
...        | done VM                    =  step (β-ƛ VM)
progress (`zero)                        =  done V-zero
progress (`suc M) with progress M
...    | step M—→M′                     =  step (ξ-suc M—→M′)
...    | done VM                        =  done (V-suc VM)
progress (case L M N) with progress L
...    | step L—→L′                     =  step (ξ-case L—→L′)
...    | done V-zero                    =  step (β-zero)
...    | done (V-suc VL)                =  step (β-suc VL)
progress (μ N)                          =  step (β-μ)
```

### Evaluation

```  record Gas : Set where
constructor gas
field
amount : ℕ

data Finished {Γ A} (N : Γ ⊢ A) : Set where

done :
Value N
----------
→ Finished N

out-of-gas :
----------
Finished N

data Steps : ∀ {A} → ∅ ⊢ A → Set where

steps : ∀ {A} {L N : ∅ ⊢ A}
→ L —↠ N
→ Finished N
----------
→ Steps L

eval : ∀ {A}
→ Gas
→ (L : ∅ ⊢ A)
-----------
→ Steps L
eval (gas zero)    L                     =  steps (L ∎) out-of-gas
eval (gas (suc m)) L with progress L
... | done VL                            =  steps (L ∎) (done VL)
... | step {M} L—→M with eval (gas m) M
...    | steps M—↠N fin                  =  steps (L —→⟨ L—→M ⟩ M—↠N) fin
```

### Example

Here is a term (in extrinsic style) to add two numbers.

``````plus = μ "plus" ⇒ ƛ "m" ⇒ ƛ n ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ ` "plus" · ` "m" · ` "n" ]``````

Here is a sample reduction demonstrating that two plus two is four.

```  pattern two = `suc `suc `zero
pattern plus = μ ƛ ƛ (case (` S Z) (` Z) (`suc (` S S S Z · ` Z · ` S Z)))

2+2 : ∅ ⊢ `ℕ
2+2 = plus · two · two

_ : 2+2 —↠ `suc `suc `suc `suc `zero
_ =
begin
plus · two · two
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
(ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z))) · two · two
—→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
(ƛ case two (` Z) (`suc (plus · ` Z · ` S Z))) · two
—→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
case two two (`suc (plus · ` Z · two))
—→⟨ β-suc (V-suc V-zero) ⟩
`suc (plus · `suc `zero · two)
—→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
`suc ((ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z)))
· `suc `zero · two)
—→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
`suc ((ƛ case (`suc `zero) (` Z) (`suc (plus · ` Z · ` S Z))) · two)
—→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
`suc (case (`suc `zero) (two) (`suc (plus · ` Z · two)))
—→⟨ ξ-suc (β-suc V-zero) ⟩
`suc (`suc (plus · `zero · two))
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
`suc (`suc ((ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z)))
· `zero · two))
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
`suc (`suc ((ƛ case `zero (` Z) (`suc (plus · ` Z · ` S Z))) · two))
—→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
`suc (`suc (case `zero (two) (`suc (plus · ` Z · two))))
—→⟨ ξ-suc (ξ-suc β-zero) ⟩
`suc (`suc (`suc (`suc `zero)))
∎
```

## Problem 3

Remember to indent all code by two spaces.

```module Problem3 where
```

### Syntax

```  infix   4  _∋_⦂_
infix   4  _⊢_↑_
infix   4  _⊢_↓_
infixl  5  _,_⦂_

infixr  7  _⇒_

infix   5  ƛ_⇒_
infix   5  μ_⇒_
infix   6  _↑
infix   6  _↓_
infixl  7  _·_
infix   8  `suc_
infix   9  `_
```

### Types

```  data Type : Set where
_⇒_   : Type → Type → Type
`ℕ    : Type
```

### Identifiers

```  Id : Set
Id = String
```

### Contexts

```  data Context : Set where
∅     : Context
_,_⦂_ : Context → Id → Type → Context
```

### Terms

```  data Term⁺ : Set
data Term⁻ : Set

data Term⁺ where
`_                        : Id → Term⁺
_·_                       : Term⁺ → Term⁻ → Term⁺
_↓_                       : Term⁻ → Type → Term⁺

data Term⁻ where
ƛ_⇒_                     : Id → Term⁻ → Term⁻
`zero                    : Term⁻
`suc_                    : Term⁻ → Term⁻
`case_[zero⇒_|suc_⇒_]    : Term⁺ → Term⁻ → Id → Term⁻ → Term⁻
μ_⇒_                     : Id → Term⁻ → Term⁻
_↑                       : Term⁺ → Term⁻
```

### Lookup

```  data _∋_⦂_ : Context → Id → Type → Set where

Z : ∀ {Γ x A}
--------------------
→ Γ , x ⦂ A ∋ x ⦂ A

S : ∀ {Γ x y A B}
→ x ≢ y
→ Γ ∋ x ⦂ A
-----------------
→ Γ , y ⦂ B ∋ x ⦂ A
```

### Bidirectional type checking

```  data _⊢_↑_ : Context → Term⁺ → Type → Set
data _⊢_↓_ : Context → Term⁻ → Type → Set

data _⊢_↑_ where

⊢` : ∀ {Γ A x}
→ Γ ∋ x ⦂ A
-----------
→ Γ ⊢ ` x ↑ A

_·_ : ∀ {Γ L M A B}
→ Γ ⊢ L ↑ A ⇒ B
→ Γ ⊢ M ↓ A
-------------
→ Γ ⊢ L · M ↑ B

⊢↓ : ∀ {Γ M A}
→ Γ ⊢ M ↓ A
---------------
→ Γ ⊢ (M ↓ A) ↑ A

data _⊢_↓_ where

⊢ƛ : ∀ {Γ x N A B}
→ Γ , x ⦂ A ⊢ N ↓ B
-------------------
→ Γ ⊢ ƛ x ⇒ N ↓ A ⇒ B

⊢zero : ∀ {Γ}
--------------
→ Γ ⊢ `zero ↓ `ℕ

⊢suc : ∀ {Γ M}
→ Γ ⊢ M ↓ `ℕ
---------------
→ Γ ⊢ `suc M ↓ `ℕ

⊢case : ∀ {Γ L M x N A}
→ Γ ⊢ L ↑ `ℕ
→ Γ ⊢ M ↓ A
→ Γ , x ⦂ `ℕ ⊢ N ↓ A
-------------------------------------
→ Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ↓ A

⊢μ : ∀ {Γ x N A}
→ Γ , x ⦂ A ⊢ N ↓ A
-----------------
→ Γ ⊢ μ x ⇒ N ↓ A

⊢↑ : ∀ {Γ M A B}
→ Γ ⊢ M ↑ A
→ A ≡ B
-------------
→ Γ ⊢ (M ↑) ↓ B
```

### Type equality

```  _≟Tp_ : (A B : Type) → Dec (A ≡ B)
`ℕ      ≟Tp `ℕ              =  yes refl
`ℕ      ≟Tp (A ⇒ B)         =  no λ()
(A ⇒ B) ≟Tp `ℕ              =  no λ()
(A ⇒ B) ≟Tp (A′ ⇒ B′)
with A ≟Tp A′ | B ≟Tp B′
...  | no A≢    | _         =  no λ{refl → A≢ refl}
...  | yes _    | no B≢     =  no λ{refl → B≢ refl}
...  | yes refl | yes refl  =  yes refl
```

### Prerequisites

```  dom≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′
dom≡ refl = refl

rng≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → B ≡ B′
rng≡ refl = refl

ℕ≢⇒ : ∀ {A B} → `ℕ ≢ A ⇒ B
ℕ≢⇒ ()
```

### Unique lookup

```  uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
uniq-∋ Z Z                 =  refl
uniq-∋ Z (S x≢y _)         =  ⊥-elim (x≢y refl)
uniq-∋ (S x≢y _) Z         =  ⊥-elim (x≢y refl)
uniq-∋ (S _ ∋x) (S _ ∋x′)  =  uniq-∋ ∋x ∋x′
```

### Unique synthesis

```  uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B
uniq-↑ (⊢` ∋x) (⊢` ∋x′)       =  uniq-∋ ∋x ∋x′
uniq-↑ (⊢L · ⊢M) (⊢L′ · ⊢M′)  =  rng≡ (uniq-↑ ⊢L ⊢L′)
uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′)       =  refl
```

## Lookup type of a variable in the context

```  ext∋ : ∀ {Γ B x y}
→ x ≢ y
→ ¬ (∃[ A ] Γ ∋ x ⦂ A)
----------------------------
→ ¬ (∃[ A ] Γ , y ⦂ B ∋ x ⦂ A)
ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
ext∋ _   ¬∃ ⟨ A , S _ ⊢x ⟩  =  ¬∃ ⟨ A , ⊢x ⟩

lookup :
∀ (Γ : Context) (x : Id)
-----------------------
→ Dec (∃[ A ] Γ ∋ x ⦂ A)
lookup ∅ x                        =  no  (λ ())
lookup (Γ , y ⦂ B) x with x ≟ y
... | yes refl                    =  yes ⟨ B , Z ⟩
... | no x≢y with lookup Γ x
...             | no  ¬∃          =  no  (ext∋ x≢y ¬∃)
...             | yes ⟨ A , ⊢x ⟩  =  yes ⟨ A , S x≢y ⊢x ⟩
```

### Promoting negations

```  ¬arg : ∀ {Γ A B L M}
→ Γ ⊢ L ↑ A ⇒ B
→ ¬ (Γ ⊢ M ↓ A)
--------------------------
→ ¬ (∃[ B′ ] Γ ⊢ L · M ↑ B′)
¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′

¬switch : ∀ {Γ M A B}
→ Γ ⊢ M ↑ A
→ A ≢ B
---------------
→ ¬ Γ ⊢ (M ↑) ↓ B
¬switch ⊢M A≢B (⊢↑ ⊢M′ A′≡B) rewrite uniq-↑ ⊢M ⊢M′ = A≢B A′≡B
```

## Synthesize and inherit types

```  synthesize : ∀ (Γ : Context) (M : Term⁺)
-----------------------
→ Dec (∃[ A ] Γ ⊢ M ↑ A )

inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
---------------
→ Dec (Γ ⊢ M ↓ A)

synthesize Γ (` x) with lookup Γ x
... | no  ¬∃              =  no  (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ })
... | yes ⟨ A , ∋x ⟩      =  yes ⟨ A , ⊢` ∋x ⟩
synthesize Γ (L · M) with synthesize Γ L
... | no  ¬∃              =  no  (λ{ ⟨ _ , ⊢L  · _  ⟩  →  ¬∃ ⟨ _ , ⊢L ⟩ })
... | yes ⟨ `ℕ ,    ⊢L ⟩  =  no  (λ{ ⟨ _ , ⊢L′ · _  ⟩  →  ℕ≢⇒ (uniq-↑ ⊢L ⊢L′) })
... | yes ⟨ A ⇒ B , ⊢L ⟩ with inherit Γ M A
...    | no  ¬⊢M          =  no  (¬arg ⊢L ¬⊢M)
...    | yes ⊢M           =  yes ⟨ B , ⊢L · ⊢M ⟩
synthesize Γ (M ↓ A) with inherit Γ M A
... | no  ¬⊢M             =  no  (λ{ ⟨ _ , ⊢↓ ⊢M ⟩  →  ¬⊢M ⊢M })
... | yes ⊢M              =  yes ⟨ A , ⊢↓ ⊢M ⟩

inherit Γ (ƛ x ⇒ N) `ℕ      =  no  (λ())
inherit Γ (ƛ x ⇒ N) (A ⇒ B) with inherit (Γ , x ⦂ A) N B
... | no ¬⊢N                =  no  (λ{ (⊢ƛ ⊢N)  →  ¬⊢N ⊢N })
... | yes ⊢N                =  yes (⊢ƛ ⊢N)
inherit Γ `zero `ℕ          =  yes ⊢zero
inherit Γ `zero (A ⇒ B)     =  no  (λ())
inherit Γ (`suc M) `ℕ with inherit Γ M `ℕ
... | no ¬⊢M                =  no  (λ{ (⊢suc ⊢M)  →  ¬⊢M ⊢M })
... | yes ⊢M                =  yes (⊢suc ⊢M)
inherit Γ (`suc M) (A ⇒ B)  =  no  (λ())
inherit Γ (`case L [zero⇒ M |suc x ⇒ N ]) A with synthesize Γ L
... | no ¬∃                 =  no  (λ{ (⊢case ⊢L  _ _) → ¬∃ ⟨ `ℕ , ⊢L ⟩})
... | yes ⟨ _ ⇒ _ , ⊢L ⟩    =  no  (λ{ (⊢case ⊢L′ _ _) → ℕ≢⇒ (uniq-↑ ⊢L′ ⊢L) })
... | yes ⟨ `ℕ ,    ⊢L ⟩ with inherit Γ M A
...    | no ¬⊢M             =  no  (λ{ (⊢case _ ⊢M _) → ¬⊢M ⊢M })
...    | yes ⊢M with inherit (Γ , x ⦂ `ℕ) N A
...       | no ¬⊢N          =  no  (λ{ (⊢case _ _ ⊢N) → ¬⊢N ⊢N })
...       | yes ⊢N          =  yes (⊢case ⊢L ⊢M ⊢N)
inherit Γ (μ x ⇒ N) A with inherit (Γ , x ⦂ A) N A
... | no ¬⊢N                =  no  (λ{ (⊢μ ⊢N) → ¬⊢N ⊢N })
... | yes ⊢N                =  yes (⊢μ ⊢N)
inherit Γ (M ↑) B with synthesize Γ M
... | no  ¬∃                =  no  (λ{ (⊢↑ ⊢M _) → ¬∃ ⟨ _ , ⊢M ⟩ })
... | yes ⟨ A , ⊢M ⟩ with A ≟Tp B
...   | no  A≢B             =  no  (¬switch ⊢M A≢B)
...   | yes A≡B             =  yes (⊢↑ ⊢M A≡B)
```

### Example

```  two : Term⁻
two = `suc (`suc `zero)

plus : Term⁺
plus = (μ "p" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
`case (` "m") [zero⇒ ` "n" ↑
|suc "m" ⇒ `suc (` "p" · (` "m" ↑) · (` "n" ↑) ↑) ])
↓ (`ℕ ⇒ `ℕ ⇒ `ℕ)

2+2 : Term⁺
2+2 = plus · two · two
```
A smart constructor, to make it easier to access a variable.
```  S′ : ∀ {Γ x y A B}
→ {x≢y : False (x ≟ y)}
→ Γ ∋ x ⦂ A
------------------
→ Γ , y ⦂ B ∋ x ⦂ A

S′ {x≢y = x≢y} x = S (toWitnessFalse x≢y) x
```
Here is the result of typing two plus two on naturals:
```  ⊢2+2 : ∅ ⊢ 2+2 ↑ `ℕ
⊢2+2 =
(⊢↓
(⊢μ
(⊢ƛ
(⊢ƛ
(⊢case (⊢` (S′ Z)) (⊢↑ (⊢` Z) refl)
(⊢suc
(⊢↑
(⊢`
(S′
(S′
(S′ Z)))
· ⊢↑ (⊢` Z) refl
· ⊢↑ (⊢` (S′ Z)) refl)
refl))))))
· ⊢suc (⊢suc ⊢zero)
· ⊢suc (⊢suc ⊢zero))
```
We confirm that synthesis on the relevant term returns natural as the type and the above derivation:
```  _ : synthesize ∅ 2+2 ≡ yes ⟨ `ℕ , ⊢2+2 ⟩
_ = refl
```