diff --git a/Language/Equivalence.agda b/Language/Equivalence.agda
new file mode 100644
index 0000000..43cedaa
--- /dev/null
+++ b/Language/Equivalence.agda
@@ -0,0 +1,154 @@
+{-# OPTIONS --guardedness #-}
+module Language.Equivalence where
+
+open import Language.Nested using () renaming
+    ( Instruction to Instructionᵃ; Program to Programᵃ; Env to Envᵃ
+    ; pushint to pushintᵃ; pushbool to pushboolᵃ; add to addᵃ
+    ; loop to loopᵃ; break to breakᵃ
+    ; Triple to Tripleᵃ
+    ; _⇒_ to _⇒ᵃ_; _⇒*_ to _⇒*ᵃ_
+    ; pushint-eval to pushint-evalᵃ; pushbool-eval to pushbool-evalᵃ; add-eval to add-evalᵃ
+    ; break-evalᵗ to break-evalᵗᵃ; break-evalᶠ to break-evalᶠᵃ; empty-eval to empty-evalᵃ
+    ; loop-eval⁰ to loop-eval⁰ᵃ; loop-evalⁿ to loop-evalⁿᵃ
+    ; doneᵉ to doneᵉᵃ; _thenᵉ_ to _thenᵉᵃ_
+    )
+open import Language.Flat
+    using
+        (_⇒ₓ_; pushint-skip; pushbool-skip; add-skip; break-skip; loop-skip; end-skip
+        )
+    renaming
+        ( Instruction to Instructionᵇ; Program to Programᵇ; Env to Envᵇ
+        ; pushint to pushintᵇ; pushbool to pushboolᵇ; add to addᵇ
+        ; loop to loopᵇ; break to breakᵇ; end to endᵇ
+        ; Triple to Tripleᵇ
+        ; _⇒_ to _⇒ᵇ_; _⇒*_ to _⇒*ᵇ_
+        ; pushint-eval to pushint-evalᵇ; pushbool-eval to pushbool-evalᵇ; add-eval to add-evalᵇ
+        ; break-evalᵗ to break-evalᵗᵇ; break-evalᶠ to break-evalᶠᵇ; end-eval to end-evalᵇ
+        ; loop-eval⁰ to loop-eval⁰ᵇ; loop-evalⁿ to loop-evalⁿᵇ
+        ; doneᵉ to doneᵉᵇ; _thenᵉ_ to _thenᵉᵇ_
+        )
+open import Language.Values using
+    ( Value; int; bool
+    ; ValueType; tint; tbool
+    ; ⟦_⟧ˢ; ⟦⟧ˢ-empty; ⟦⟧ˢ-int; ⟦⟧ˢ-bool
+    ; s; s'; s''
+    ; st; st'; st''
+    ; b; b₁; b₂
+    ; z; z₁; z₂
+    )
+
+open import Data.List using (List; _∷_; []; length; foldr; _++_)
+open import Data.List.Properties using (++-assoc)
+open import Data.Product using (Σ; _×_; _,_)
+open import Data.Nat using (ℕ)
+open import Data.Unit using (⊤; tt)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
+
+variable
+    n n' : ℕ
+
+    iᵃ : Instructionᵃ
+    isᵃ isᵃ' isᵃ'' : Programᵃ
+    Sᵃ Sᵃ' Sᵃ'' : Envᵃ
+
+    iᵇ : Instructionᵇ
+    isᵇ isᵇ' isᵇ'' : Programᵇ
+    Sᵇ Sᵇ' Sᵇ'' : Envᵇ
+
+
+interleaved mutual
+    ⟦_⟧ⁱ : Instructionᵃ → List Instructionᵇ
+    ⟦_⟧ⁱˢ : List Instructionᵃ → List Instructionᵇ
+
+    ⟦ pushintᵃ z ⟧ⁱ = pushintᵇ z ∷ []
+    ⟦ pushboolᵃ b ⟧ⁱ = pushboolᵇ b ∷ []
+    ⟦ addᵃ ⟧ⁱ = addᵇ ∷ []
+    ⟦ loopᵃ n is ⟧ⁱ = loopᵇ n ∷ (⟦ is ⟧ⁱˢ ++ endᵇ ∷ [])
+    ⟦ breakᵃ ⟧ⁱ = breakᵇ ∷ []
+
+    ⟦ [] ⟧ⁱˢ = []
+    ⟦ i ∷ is ⟧ⁱˢ = ⟦ i ⟧ⁱ ++ ⟦ is ⟧ⁱˢ
+
+-- Translation always leaves well-balanced programs
+interleaved mutual
+    lemma₁  : isᵇ ⇒ₓ isᵇ' → (⟦ iᵃ ⟧ⁱ ++ isᵇ) ⇒ₓ isᵇ'
+    lemma₁' : isᵇ ⇒ₓ isᵇ' → (⟦ isᵃ ⟧ⁱˢ ++ isᵇ) ⇒ₓ isᵇ'
+    lemma₂  : (⟦ isᵃ ⟧ⁱˢ ++ endᵇ ∷ isᵇ) ⇒ₓ isᵇ
+
+    lemma₁ {iᵃ = pushintᵃ z} = pushint-skip
+    lemma₁ {iᵃ = pushboolᵃ z} = pushbool-skip
+    lemma₁ {iᵃ = addᵃ} = add-skip
+    lemma₁ {iᵃ = breakᵃ} = break-skip
+    lemma₁ {isᵇ = isᵇ} {iᵃ = loopᵃ n is}
+        rewrite ++-assoc ⟦ is ⟧ⁱˢ (endᵇ ∷ []) isᵇ =
+        loop-skip (lemma₂ {isᵃ = is} {isᵇ = isᵇ})
+
+    lemma₁' {isᵃ = []} isᵇ⇒ₓisᵇ' = isᵇ⇒ₓisᵇ'
+    lemma₁' {isᵇ = isᵇ} {isᵃ = iᵃ ∷ isᵃ} isᵇ⇒ₓisᵇ'
+        rewrite ++-assoc ⟦ iᵃ ⟧ⁱ ⟦ isᵃ ⟧ⁱˢ isᵇ =
+        lemma₁ {iᵃ = iᵃ} (lemma₁' {isᵃ = isᵃ} isᵇ⇒ₓisᵇ')
+
+    lemma₂ {isᵃ = isᵃ} = lemma₁' {isᵃ = isᵃ} end-skip
+
+-- In flat semantics, we drop the top continuation and seek forward until we find
+-- an 'end'. In nested semantics, we drop the current instructions and use the
+-- bit of the top continuation after the 'while'. We need to be able to reconcile
+-- the two.
+data ⟦_⟧ᵀ=_ : Programᵃ × Envᵃ → Programᵇ × Envᵇ → Set where
+    ⟦⟧ᵀ-empty : ⟦ isᵃ , [] ⟧ᵀ= (⟦ isᵃ ⟧ⁱˢ , [])
+    ⟦⟧ᵀ-step : ⟦ isᵃ'' , Sᵃ ⟧ᵀ= (isᵇ , Sᵇ) →
+               ⟦ isᵃ , ((loopᵃ n isᵃ' ∷ isᵃ'') ∷ Sᵃ) ⟧ᵀ= ((⟦ isᵃ ⟧ⁱˢ ++ endᵇ ∷ []) ++ isᵇ , (⟦ loopᵃ n isᵃ' ⟧ⁱ ++ isᵇ) ∷ Sᵇ)
+
+
+step-equivalence : (s , isᵃ , Sᵃ) ⇒ᵃ (s' , isᵃ' , Sᵃ') →
+                   ⟦ isᵃ , Sᵃ ⟧ᵀ= (isᵇ , Sᵇ) →
+                   Σ (Programᵇ × Envᵇ) (λ { (isᵇ' , Sᵇ') → (s , isᵇ , Sᵇ) ⇒ᵇ (s' , isᵇ' , Sᵇ') ×
+                                                           ⟦ isᵃ' , Sᵃ' ⟧ᵀ= (isᵇ' , Sᵇ') })
+step-equivalence pushint-evalᵃ ⟦⟧ᵀ-empty = ((_ , _) , pushint-evalᵇ , ⟦⟧ᵀ-empty)
+step-equivalence pushint-evalᵃ (⟦⟧ᵀ-step next) = ((_ , _) , pushint-evalᵇ  , ⟦⟧ᵀ-step next)
+step-equivalence pushbool-evalᵃ ⟦⟧ᵀ-empty = ((_ , _) , pushbool-evalᵇ , ⟦⟧ᵀ-empty)
+step-equivalence pushbool-evalᵃ (⟦⟧ᵀ-step next) = ((_ , _) , pushbool-evalᵇ , ⟦⟧ᵀ-step next)
+step-equivalence add-evalᵃ ⟦⟧ᵀ-empty = ((_ , _) , add-evalᵇ , ⟦⟧ᵀ-empty)
+step-equivalence add-evalᵃ (⟦⟧ᵀ-step next) = ((_ , _) , add-evalᵇ , ⟦⟧ᵀ-step next)
+step-equivalence {isᵃ = loopᵃ n isˡ ∷ isᵃ} loop-eval⁰ᵃ ⟦⟧ᵀ-empty
+    rewrite ++-assoc ⟦ isˡ ⟧ⁱˢ (endᵇ ∷ []) ⟦ isᵃ ⟧ⁱˢ
+    = ((_ , _) , loop-eval⁰ᵇ (lemma₁' {isᵃ = isˡ} end-skip) , ⟦⟧ᵀ-empty)
+step-equivalence {isᵃ = loopᵃ n isˡ ∷ isᵃ} loop-eval⁰ᵃ (⟦⟧ᵀ-step {isᵇ = isᵇ} rec)
+    rewrite ++-assoc ⟦ isˡ ⟧ⁱˢ (endᵇ ∷ []) ⟦ isᵃ ⟧ⁱˢ
+    rewrite ++-assoc ⟦ isˡ ⟧ⁱˢ (endᵇ ∷ ⟦ isᵃ ⟧ⁱˢ) (endᵇ ∷ [])
+    rewrite ++-assoc ⟦ isˡ ⟧ⁱˢ (endᵇ ∷ ⟦ isᵃ ⟧ⁱˢ ++ endᵇ ∷ []) isᵇ
+    = ((_ , _) , loop-eval⁰ᵇ (lemma₁' {isᵃ = isˡ} end-skip) , (⟦⟧ᵀ-step rec))
+step-equivalence {isᵃ = loopᵃ n isˡ ∷ isᵃ} loop-evalⁿᵃ ⟦⟧ᵀ-empty
+    = ((_ , _) , loop-evalⁿᵇ , ⟦⟧ᵀ-step ⟦⟧ᵀ-empty)
+step-equivalence {isᵃ = loopᵃ n isˡ ∷ isᵃ} loop-evalⁿᵃ (⟦⟧ᵀ-step {isᵇ = isᵇ} rec)
+    rewrite ++-assoc (⟦ isˡ ⟧ⁱˢ ++ endᵇ ∷ []) ⟦ isᵃ ⟧ⁱˢ (endᵇ ∷ [])
+    rewrite ++-assoc ⟦ isˡ ⟧ⁱˢ (endᵇ ∷ []) (⟦ isᵃ ⟧ⁱˢ ++ endᵇ ∷ [])
+    rewrite sym (++-assoc ⟦ isˡ ⟧ⁱˢ (endᵇ ∷ []) (⟦ isᵃ ⟧ⁱˢ ++ endᵇ ∷ []))
+    rewrite ++-assoc (⟦ isˡ ⟧ⁱˢ ++ endᵇ ∷ []) (⟦ isᵃ ⟧ⁱˢ ++ endᵇ ∷ []) isᵇ
+    = (_ , loop-evalⁿᵇ , ⟦⟧ᵀ-step (⟦⟧ᵀ-step rec))
+step-equivalence break-evalᶠᵃ (⟦⟧ᵀ-step next) = ((_ , _) , break-evalᶠᵇ , ⟦⟧ᵀ-step next)
+step-equivalence {isᵃ = breakᵃ ∷ isᵃ} {Sᵃ = (loopᵃ n isˡ ∷ isᵃ') ∷ Sᵃ} break-evalᵗᵃ (⟦⟧ᵀ-step {isᵇ = isᵇ} next)
+    rewrite ++-assoc ⟦ isᵃ ⟧ⁱˢ (endᵇ ∷ []) isᵇ
+    = ((_ , _) , break-evalᵗᵇ (lemma₁' {isᵃ = isᵃ} end-skip) , next)
+step-equivalence empty-evalᵃ (⟦⟧ᵀ-step ⟦⟧ᵀ-empty)
+    = ((_ , _) , end-evalᵇ , ⟦⟧ᵀ-empty)
+step-equivalence {Sᵃ = (loopᵃ n isˡ ∷ isᵃ') ∷ Sᵃ} empty-evalᵃ (⟦⟧ᵀ-step (⟦⟧ᵀ-step {isᵇ = isᵇ} next))
+    rewrite sym (++-assoc (loopᵇ n ∷ ⟦ isˡ ⟧ⁱˢ ++ endᵇ ∷ []) (⟦ isᵃ' ⟧ⁱˢ ++ endᵇ ∷ []) isᵇ)
+    rewrite sym (++-assoc (⟦ isˡ ⟧ⁱˢ ++ endᵇ ∷ []) (⟦ isᵃ' ⟧ⁱˢ) (endᵇ ∷ []))
+    = ((_ , _) , end-evalᵇ , ⟦⟧ᵀ-step next)
+
+equivalence : (s , isᵃ , Sᵃ) ⇒*ᵃ (s' , isᵃ' , Sᵃ') →
+              ⟦ isᵃ , Sᵃ ⟧ᵀ= (isᵇ , Sᵇ) →
+              Σ (Programᵇ × Envᵇ) (λ { (isᵇ' , Sᵇ') → (s , isᵇ , Sᵇ) ⇒*ᵇ (s' , isᵇ' , Sᵇ') ×
+                                                           ⟦ isᵃ' , Sᵃ' ⟧ᵀ= (isᵇ' , Sᵇ') })
+equivalence doneᵉᵃ trans@(⟦⟧ᵀ-empty) = (_ , (doneᵉᵇ , trans))
+equivalence (isᵃ⇒isᵃ' thenᵉᵃ rest) trans =
+    let (_ , isᵇ⇒isᵇ' , trans') = step-equivalence isᵃ⇒isᵃ' trans in
+    let (_ , isᵇ'⇒*isᵇ'' , trans'') = equivalence rest trans' in
+    (_ , isᵇ⇒isᵇ' thenᵉᵇ isᵇ'⇒*isᵇ'' , trans'')
+
+equivalence' : (s , isᵃ , []) ⇒*ᵃ (s' , [] , []) →
+               (s , ⟦ isᵃ ⟧ⁱˢ , []) ⇒*ᵇ (s' , [] , [])
+equivalence' eval with
+    (_ , isᵃ⇒| , ⟦⟧ᵀ-empty) ←  equivalence eval ⟦⟧ᵀ-empty = isᵃ⇒|