[Added a universe and a variant of the compiler which uses the universe.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080305011239] hunk ./MultiComposition.agda 28
-lemma : forall {a} ts₁ {ts₂} ->
-        Fun ts₁ (Fun ts₂ a) ≡₁ Fun (ts₁ ++₁ ts₂) a
-lemma []₁        = ≡₁-refl
-lemma (t ∷₁ ts₁) = ≡₁-ext \_ -> lemma ts₁
+Fun-lemma : forall {a} ts₁ {ts₂} ->
+            Fun ts₁ (Fun ts₂ a) ≡₁ Fun (ts₁ ++₁ ts₂) a
+Fun-lemma []₁        = ≡₁-refl
+Fun-lemma (t ∷₁ ts₁) = ≡₁-ext \_ -> Fun-lemma ts₁
hunk ./Wand.agda 23
+open import Data.List
hunk ./Wand.agda 27
+open import Relation.Binary.PropositionalEquality1
hunk ./Wand.agda 248
+  -- We can still combine the proofs:
+
+  correct : forall e -> E e ≡ ⟦ comp e ⟧
+  correct e = begin
+    E e
+      ≡⟨ proof (Step₁.E'P e) ⟩
+    Step₁.E' e
+      ≡⟨ ≡-refl ⟩
+    ⟦ comp e ⟧
+      ∎
+
+module Universe where
+
+  open Language
+  open import Data.List
+
+  -- To simplify the development, let's define a type ("universe")
+  -- capturing the types used. Having a representation for types means
+  -- that we can pattern match on them.
+
+  infixr 0 _→_
+
+  data Ty : Set where
+    id  : Ty
+    v   : Ty
+    _→_ : Ty -> Ty -> Ty
+
+  ⟦_⟧⋆ : Ty -> Set
+  ⟦ id ⟧⋆    = Id
+  ⟦ v ⟧⋆     = V
+  ⟦ σ → τ ⟧⋆ = ⟦ σ ⟧⋆ -> ⟦ τ ⟧⋆
+
+  fun : [ Ty ] -> Ty -> Ty
+  fun []       τ = τ
+  fun (σ ∷ σs) τ = σ → fun σs τ
+
+  s : Ty
+  s = id → v
+
+  c : Ty
+  c = s → v
+
+  k : Ty
+  k = v → c
+
+  lemma : forall σs {τ} ->
+          ⟦ fun σs τ ⟧⋆ ≡₁ Fun (map₀₁ ⟦_⟧⋆ σs) ⟦ τ ⟧⋆
+  lemma []       = ≡₁-refl
+  lemma (σ ∷ σs) = ≡₁-cong (\t -> ⟦ σ ⟧⋆ -> t) (lemma σs)
+
+module Step₂'' where
+
+  open Language
+  open Universe
+
+  -- A variant of Step₂' which uses the universe.
+
+  _⟪_⟫'_ : forall {a b} ->
+           ⟦ a → b ⟧⋆ -> (ts : [ Ty ]) -> ⟦ fun ts a ⟧⋆ -> ⟦ fun ts b ⟧⋆
+  f ⟪ τs ⟫' g = ≡₁-subst (≡₁-sym (lemma τs))
+                         (f ⟪ map₀₁ ⟦_⟧⋆ τs ⟫ ≡₁-subst (lemma τs) g)
+
+  -- Step₂ can be simplified by indexing the Exp' type on the
+  -- semantics of expressions:
+
+  data Exp' : (t : Ty) -> ⟦ t ⟧⋆ -> Set1 where
+    B     : forall {a b} ts {f g} ->
+            Exp' (a → b) f -> Exp' (fun ts a) g ->
+            Exp' (fun ts b) (f ⟪ ts ⟫' g)
+    add   : Exp' (k → v → v → c) Step₁.add
+    fetch : (I : Id) -> Exp' (k → c) (Step₁.fetch I)
+    halt  : Exp' k Step₁.halt
+
+  -- The semantics is encoded in the type:
+
+  ⟦_⟧ : forall {t f} -> Exp' t f -> ⟦ t ⟧⋆
+  ⟦_⟧ {f = f} _ = f
+
+  -- Correctness of compilation is ensured through the type of comp:
+
+  comp : (e : Exp) -> Exp' (k → c) (Step₁.E' e)
+  comp (id I)      = fetch I
+  comp [ e₁ + e₂ ] = B (k ∷ []) (comp e₁) (B (k ∷ v ∷ []) (comp e₂) add)
+
+  -- Note: Now we are using some proof code. See _⟪_⟫'_ above.
+