diff --git a/agda/02-dependent/Indexed.lagda.rst b/agda/02-dependent/Indexed.lagda.rst
index 8989b9b89e456bbc00170110e29746acf590fc2a..501aad8c0125ea15465252a9f7958bf00dafe431 100644
--- a/agda/02-dependent/Indexed.lagda.rst
+++ b/agda/02-dependent/Indexed.lagda.rst
@@ -132,232 +132,6 @@ of the string ``s`` to be printed. Careful, the formats ``%.s`` or
``%.cs`` are non-sensical: this should impact either parsing or
interpretation.
-************************************************
-Mostly correct-by-construction compiler
-************************************************
-
-..
- ::
-
- module Compiler where
-
- infixr 5 _∙_
- infixr 5 _#_
-
-Using dependent types (in particular, inductive families), we can bake
-our invariants in the datatypes we manipulate and make sure that they
-are preserved as we process them. The advantage is twofold:
-
- - build *initial* models of a domain of interest (syntax!)
- - total denotational semantics in Agda itself (interpreter!)
-
-We illustrate this approach with another Classic, a draft of James
-McKinna & Joel Wright entitled `A type-correct, stack-safe, provably
-correct, expression compiler`_. As suggested by the title, we are
-going to implement a correct-by-construction compiler from a language
-of expressions to a stack machine.
-
---------------------------------
-Type-safe representation
---------------------------------
-
-Because Agda's type system is extremely rich, we can in fact *absorb*
-the type discipline of expressions in Agda. In programming terms, we
-define a datatype ``exp`` that represents only well-typed expressions::
-
- data typ : Set where
- nat bool : typ
-
- sem : typ → Set
- sem nat = â„•
- sem bool = Bool
-
- data exp : typ → Set where
- val : ∀ {T} → (v : sem T) → exp T
- plus : (e₠e₂ : exp nat) → exp nat
- ifte : ∀ {T} → (c : exp bool)(e₠e₂ : exp T) → exp T
-
-We define the semantics of this language by interpretation within
-Agda::
-
- eval : ∀ {T} → exp T → sem T
- eval (val v) = v
- eval (plus eâ‚ eâ‚‚) = eval eâ‚ + eval eâ‚‚
- eval (ifte c eâ‚ eâ‚‚) = if eval c then eval eâ‚ else eval eâ‚‚
-
-If we were pedantic, we would call this a *denotational*
-semantics.
-
-Note that we crucially rely on the fact that ``sem`` computes at the
-type level to ensure that, for example, the ``if_then_else_`` is
-performed on a Boolean and not a natural number. This is called a
-*tagless* interpreter. In a non-dependent setting, values would have
-carried a tag (discriminating them based on their type) and the
-evaluator would have to deal with type errors dynamically::
-
- module Tagged where
-
- data value : Set where
- isNat : (n : ℕ) → value
- isBool : (b : Bool) → value
-
- data exp' : Set where
- val : (v : value) → exp'
- plus : (e₠e₂ : exp') → exp'
- ifte : (c e₠e₂ : exp') → exp'
-
- eval' : exp' → Maybe value
- eval' (val v) = just v
- eval' (plus eâ‚ eâ‚‚)
- with eval' eâ‚ | eval' eâ‚‚
- ... | just (isNat nâ‚)
- | just (isNat nâ‚‚) = just (isNat (nâ‚ + nâ‚‚))
- ... | _ | _ = nothing
- eval' (ifte c eâ‚ eâ‚‚)
- with eval' c | eval' eâ‚ | eval' eâ‚‚
- ... | just (isBool b) | vâ‚ | vâ‚‚ = if b then vâ‚ else vâ‚‚
- ... | _ | _ | _ = nothing
-
-**Exercise (difficulty: 1)** The above implementation is needlessly
-verbose, use the Maybe monad to abstract away error handling.
-
-The moral of this implementation is that we failed to encode our
-invariant in the datatype ``exp'`` and paid the price in the
-implementation of ``eval'``.
-
---------------------------------
-Stack machine
---------------------------------
-
-Our stack machine will interpret a fixed set of opcodes, transforming
-input stack to output stack. A stack will contain values,
-ie. Booleans or integers. We can therefore describe well-typed stacks
-by identifying the type of each elements::
-
- stack-typ = List typ
-
- data stack : stack-typ → Set where
- ε : stack []
- _∙_ : ∀ {T σ} → sem T → stack σ → stack (T ∷ σ)
-
-
-In particular, a non-empty stack allows us to peek at the top element
-and to take its tail::
-
- top : ∀ {T σ} → stack (T ∷ σ) → sem T
- top (t ∙ _) = t
-
- tail : ∀ {T σ} → stack (T ∷ σ) → stack σ
- tail (_ ∙ s) = s
-
-Using an inductive family, we can once again garantee that
-instructions are only applied onto well-formed and well-typed stacks::
-
- data code : stack-typ → stack-typ → Set where
- skip : ∀ {σ} → code σ σ
- _#_ : ∀ {σ₠σ₂ σ₃} → (c₠: code σ₠σ₂)(c₂ : code σ₂ σ₃) → code σ₠σ₃
- PUSH : ∀ {T σ} → (v : sem T) → code σ (T ∷ σ)
- ADD : ∀ {σ} → code (nat ∷ nat ∷ σ) (nat ∷ σ)
- IFTE : ∀ {σ₠σ₂} → (câ‚ câ‚‚ : code σ₠σ₂) → code (bool ∷ σâ‚) σ₂
-
-As a result, we can implement a (total) interpreter for our stack
-machine::
-
- exec : ∀ {σ-i σ-f} → code σ-i σ-f → stack σ-i → stack σ-f
- exec skip s = s
- exec (câ‚ # câ‚‚) s = exec câ‚‚ (exec câ‚ s)
- exec (PUSH v) s = v ∙ s
- exec ADD (x₠∙ x₂ ∙ s) = x₠+ x₂ ∙ s
- exec (IFTE c₠c₂) (true ∙ s) = exec c₠s
- exec (IFTE c₠c₂) (false ∙ s) = exec c₂ s
-
-**Exercise (difficulty: 1)** Implement a simply-typed version of
-``code`` and update ``exec`` to work (partially) from list of tagged
-values to list of tagged values.
-
---------------------------------
-Compilation
---------------------------------
-
-The compiler from expressions to stack machine code is then
-straightforward, the types making sure that we cannot generate
-non-sensical opcodes::
-
- compile : ∀ {T σ} → exp T → code σ (T ∷ σ)
- compile (val v) = PUSH v
- compile (plus eâ‚ eâ‚‚) = compile eâ‚‚ # compile eâ‚ # ADD
- compile (ifte c eâ‚ eâ‚‚) = compile c # IFTE (compile eâ‚) (compile eâ‚‚)
-
-**Exercise (difficulty: 1)** Implement the (same) compiler on the
-simply-typed representation of expressions ``exp'``.
-
-Note that this does not guarantee that we preserve the semantics!
-
-**Exercise (difficulty: 4)** We could address that remark by indexing
-expressions (``exp``) not only by their type but also by their
-denotation (a natural number):
-
-.. code-block:: guess
-
- expSem : (T : typ) → ⟦ T ⟧ → Set
-
-Similarly, the stack machine opcodes could be indexed by their
-denotation (a stack):
-
-.. code-block:: guess
-
- codeSem : (σ : stack-typ) → stack σ → Set
-
-As a result, a type-safe ``compile`` function from ``expSem`` to
-``codeSem`` could ensure semantics-preservation by
-construction. Implement these source and target languages and the
-correct-by-construction compiler.
-
-
---------------------------------
-Correctness
---------------------------------
-
-The correctness proof amounts to showing that the interpreter for
-expressions agrees with the result of executing the stack
-machine. Having baked the typing discipline in our input expressions
-and output machine codes, we can focus on proving only the meaningful
-cases::
-
- correctness : forall {T σ} → (e : exp T)(s : stack σ) → exec (compile e) s ≡ eval e ∙ s
- correctness (val v) s = refl
- correctness (plus eâ‚ eâ‚‚) s
- rewrite correctness eâ‚‚ s
- | correctness e₠(eval e₂ ∙ s) = refl
- correctness (ifte c eâ‚ eâ‚‚) s
- rewrite correctness c s
- with eval c
- ... | true rewrite correctness eâ‚ s = refl
- ... | false rewrite correctness eâ‚‚ s = refl
-
-
-**Exercise (difficulty: 2)** Prove the same theorem one the
-simply-typed implementations. You may prefer to work in Coq, so as to
-take advantage of tactics to automate the tedium.
-
-
-This exercise has its roots in the very origin of most programming and
-reasoning techniques we take for granted today:
-
- - the role of initiality in formal reasoning
- - the importance of equational reasoning for proving program correctness
-
-These ideas were, for examples, in their inception at the first
-edition of POPL with `Advice on structuring compilers and proving them
-correct`_ (1973), which was further refined by `More on advice on
-structuring compilers and proving them correct`_, (1980). This
-reflects the influence it had on a generation of computer scientists
-interested in language design on one hand (they gave us algebraic
-datatypes) and verified compilation on the other hand (they gave us
-denotational models). I learned these ideas from `Conor
-McBride <http://strictlypositive.org/>`_, who had learned them from
-`James McKinna <http://homepages.inf.ed.ac.uk/jmckinna/>`_.
-
************************************************
Computing normal forms of λ-terms
************************************************