Restructured directory.

beta.md

@@ -39,16 +39,16 @@ Pull requests are encouraged.
   - [Bisimulation]({{ site.baseurl }}/Bisimulation/): Relating reductions systems
   - [Inference]({{ site.baseurl }}/Inference/): Bidirectional type inference
   - [Untyped]({{ site.baseurl }}/Untyped/): Untyped lambda calculus with full normalisation
-  - [Confluence]({{ site.baseurl }}/Confluence/): Confluence of untyped lambda calculus
-  - [CallByName]({{ site.baseurl }}/CallByName/): Big-step semantics for call-by-name evaluation
+  - [Confluence]({{ site.baseurl }}/Confluence/): Confluence of untyped lambda calculus 🚧
+  - [BigStep]({{ site.baseurl }}/BigStep/): Big-step semantics of untyped lambda calculus 🚧
 
 ## Part 3: Denotational Semantics of Lambda Calculus
 
-  - [Denotational]({{ site.baseurl }}/Denotational/): Denotational semantics of untyped lambda calculus
-  - [Compositional]({{ site.baseurl }}/Compositional/): The denotational semantics is compositional
-  - [Soundness]({{ site.baseurl }}/Soundness/): Soundness of reduction with respect to denotational semantics
-  - [Adequacy]({{ site.baseurl }}/Adequacy/): Adequacy of denotational semantics with respect to operational semantics
-  - [ContextualEquivalence]({{ site.baseurl }}/ContextualEquivalence/): Denotational equality implies contextual equivalence
+  - [Denotational]({{ site.baseurl }}/Denotational/): Denotational semantics of untyped lambda calculus 🚧
+  - [Compositional]({{ site.baseurl }}/Compositional/): The denotational semantics is compositional 🚧
+  - [Soundness]({{ site.baseurl }}/Soundness/): Soundness of reduction with respect to denotational semantics 🚧
+  - [Adequacy]({{ site.baseurl }}/Adequacy/): Adequacy of denotational semantics with respect to operational semantics 🚧
+  - [ContextualEquivalence]({{ site.baseurl }}/ContextualEquivalence/): Denotational equality implies contextual equivalence 🚧
 
 ## Appendix
 

src/plfa/part1/Connectives.lagda.md

@@ -7,7 +7,7 @@ next      : /Negation/
 ---
 
 ```
-module plfa.Connectives where
+module plfa.part1.Connectives where
 ```
 
 <!-- The ⊥ ⊎ A ≅ A exercise requires a (inj₁ ()) pattern,
@@ -35,8 +35,8 @@ open Eq using (_≡_; refl)
 open Eq.≡-Reasoning
 open import Data.Nat using (ℕ)
 open import Function using (_∘_)
-open import plfa.Isomorphism using (_≃_; _≲_; extensionality)
-open plfa.Isomorphism.≃-Reasoning
+open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality)
+open plfa.part1.Isomorphism.≃-Reasoning
 ```
 
 

src/plfa/part1/Decidable.lagda.md

@@ -7,7 +7,7 @@ next      : /Lists/
 ---
 
 ```
-module plfa.Decidable where
+module plfa.part1.Decidable where
 ```
 
 We have a choice as to how to represent relations:
@@ -33,8 +33,8 @@ open import Relation.Nullary.Negation using ()
   renaming (contradiction to ¬¬-intro)
 open import Data.Unit using (⊤; tt)
 open import Data.Empty using (⊥; ⊥-elim)
-open import plfa.Relations using (_<_; z<s; s<s)
-open import plfa.Isomorphism using (_⇔_)
+open import plfa.part1.Relations using (_<_; z<s; s<s)
+open import plfa.part1.Isomorphism using (_⇔_)
 ```
 
 ## Evidence vs Computation

src/plfa/part1/Equality.lagda.md

@@ -7,7 +7,7 @@ next      : /Isomorphism/
 ---
 
 ```
-module plfa.Equality where
+module plfa.part1.Equality where
 ```
 
 Much of our reasoning has involved equality.  Given two terms `M`

src/plfa/part1/Induction.lagda.md

@@ -7,7 +7,7 @@ next      : /Relations/
 ---
 
 ```
-module plfa.Induction where
+module plfa.part1.Induction where
 ```
 
 > Induction makes you feel guilty for getting something out of nothing

src/plfa/part1/Isomorphism.lagda.md

@@ -7,7 +7,7 @@ next      : /Connectives/
 ---
 
 ```
-module plfa.Isomorphism where
+module plfa.part1.Isomorphism where
 ```
 
 This section introduces isomorphism as a way of asserting that two

src/plfa/part1/Lists.lagda.md

@@ -7,7 +7,7 @@ next      : /Lambda/
 ---
 
 ```
-module plfa.Lists where
+module plfa.part1.Lists where
 ```
 
 This chapter discusses the list data type.  It gives further examples
@@ -28,7 +28,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
 open import Function using (_∘_)
 open import Level using (Level)
-open import plfa.Isomorphism using (_≃_; _⇔_)
+open import plfa.part1.Isomorphism using (_≃_; _⇔_)
 ```
 
 

src/plfa/part1/Naturals.lagda.md

@@ -7,7 +7,7 @@ next      : /Induction/
 ---
 
 ```
-module plfa.Naturals where
+module plfa.part1.Naturals where
 ```
 
 The night sky holds more stars than I can count, though fewer than five

src/plfa/part1/Negation.lagda.md

@@ -7,7 +7,7 @@ next      : /Quantifiers/
 ---
 
 ```
-module plfa.Negation where
+module plfa.part1.Negation where
 ```
 
 This chapter introduces negation, and discusses intuitionistic
@@ -21,7 +21,7 @@ open import Data.Nat using (ℕ; zero; suc)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Product using (_×_)
-open import plfa.Isomorphism using (_≃_; extensionality)
+open import plfa.part1.Isomorphism using (_≃_; extensionality)
 ```
 
 

src/plfa/part1/Quantifiers.lagda.md

@@ -7,7 +7,7 @@ next      : /Decidable/
 ---
 
 ```
-module plfa.Quantifiers where
+module plfa.part1.Quantifiers where
 ```
 
 This chapter introduces universal and existential quantification.
@@ -21,7 +21,7 @@ open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
 open import Relation.Nullary using (¬_)
 open import Data.Product using (_×_; proj₁) renaming (_,_ to ⟨_,_⟩)
 open import Data.Sum using (_⊎_)
-open import plfa.Isomorphism using (_≃_; extensionality)
+open import plfa.part1.Isomorphism using (_≃_; extensionality)
 ```
 
 

src/plfa/part1/Relations.lagda.md

@@ -7,7 +7,7 @@ next      : /Equality/
 ---
 
 ```
-module plfa.Relations where
+module plfa.part1.Relations where
 ```
 
 After having defined operations such as addition and multiplication,

src/plfa/part2/BigStep.lagda.md

@@ -1,13 +1,13 @@
 ---
-title     : "CallByName: Big-step semantics for call-by-name evaluation"
+title     : "BigStep: Big-step semantics of untyped lambda calculus 🚧"
 layout    : page
 prev      : /Confluence/
-permalink : /CallByName/
+permalink : /BigStep/
 next      : /Denotational/
 ---
 
 ```
-module plfa.CallByName where
+module plfa.part2.BigStep where
 ```
 
 ## Introduction
@@ -34,17 +34,16 @@ single sub-computation has been completed.
 ## Imports
 
 ```
-open import plfa.Untyped
-  using (Context; _⊢_; _∋_; ★; ∅; _,_; Z; S_; `_; #_; ƛ_; _·_;
-         subst; subst-zero; exts; rename; β; ξ₁; ξ₂; ζ; _—→_; _—↠_; _—→⟨_⟩_; _∎;
-         —↠-trans; appL-cong)
-open import plfa.Substitution using (Subst; ids)
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; trans; sym; cong-app)
-
 open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
   renaming (_,_ to ⟨_,_⟩)
 open import Function using (_∘_)
+open import plfa.part2.Untyped
+     using (Context; _⊢_; _∋_; ★; ∅; _,_; Z; S_; `_; #_; ƛ_; _·_;
+            subst; subst-zero; exts; rename; β; ξ₁; ξ₂; ζ; _—→_; _—↠_; _—→⟨_⟩_; _∎;
+            —↠-trans; appL-cong)
+open import plfa.part2.Substitution using (Subst; ids)
 ```
 
 ## Environments
@@ -213,7 +212,7 @@ the same term.
 ```
 sub-id : ∀{Γ} {A} {M : Γ ⊢ A}
          → subst ids M ≡ M
-sub-id = plfa.Substitution.sub-id
+sub-id = plfa.part2.Substitution.sub-id
 ```
 
 
@@ -240,7 +239,7 @@ Chapter [Substitution]({{ site.baseurl }}/Substitution/).
 subst-zero-exts : ∀{Γ Δ}{σ : Subst Γ Δ}{B}{M : Δ ⊢ B}{x : Γ ∋ ★}
                 → (subst (subst-zero M) ∘ exts σ) (S x) ≡ σ x
 subst-zero-exts {Γ}{Δ}{σ}{B}{M}{x} =
-   cong-app (plfa.Substitution.subst-zero-exts-cons{σ = σ}) (S x)
+   cong-app (plfa.part2.Substitution.subst-zero-exts-cons{σ = σ}) (S x)
 ```
 
 So the proof of `≈ₑ-ext` is as follows.
@@ -272,7 +271,7 @@ composing the two substitutions and then applying them.
 ```
 sub-sub : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Σ}
             → subst σ₂ (subst σ₁ M) ≡ subst (subst σ₂ ∘ σ₁) M
-sub-sub {M = M} = plfa.Substitution.sub-sub {M = M}
+sub-sub {M = M} = plfa.part2.Substitution.sub-sub {M = M}
 ```
 
 We arive at the main lemma: if `M` big steps to a

src/plfa/part2/Bisimulation.lagda.md

@@ -7,7 +7,7 @@ next      : /Inference/
 ---
 
 ```
-module plfa.Bisimulation where
+module plfa.part2.Bisimulation where
 ```
 
 Some constructs can be defined in terms of other constructs.  In the
@@ -128,7 +128,7 @@ are in bisimulation.
 We import our source language from
 Chapter [More]({{ site.baseurl }}/More/):
 ```
-open import plfa.More
+open import plfa.part2.More
 ```
 
 

src/plfa/part2/Confluence.lagda.md

@@ -1,13 +1,13 @@
 ---
-title     : "Confluence: Confluence of untyped lambda calculus"
+title     : "Confluence: Confluence of untyped lambda calculus 🚧"
 layout    : page
 prev      : /Untyped/
 permalink : /Confluence/
-next      : /CallByName/
+next      : /BigStep/
 ---
 
 ```
-module plfa.Confluence where
+module plfa.part2.Confluence where
 ```
 
 ## Introduction
@@ -61,17 +61,17 @@ confluence for parallel reduction.
 ## Imports
 
 ```
-open import plfa.Substitution using (Rename; Subst)
-open import plfa.Untyped
-    using (_—→_; β; ξ₁; ξ₂; ζ; _—↠_; _—→⟨_⟩_; _∎;
-           abs-cong; appL-cong; appR-cong; —↠-trans;
-           _⊢_; _∋_; `_; #_; _,_; ★; ƛ_; _·_; _[_];
-           rename; ext; exts; Z; S_; subst; subst-zero)
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
 open import Function using (_∘_)
 open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
      renaming (_,_ to ⟨_,_⟩)
+open import plfa.part2.Substitution using (Rename; Subst)
+open import plfa.part2.Untyped
+     using (_—→_; β; ξ₁; ξ₂; ζ; _—↠_; _—→⟨_⟩_; _∎;
+     abs-cong; appL-cong; appR-cong; —↠-trans;
+     _⊢_; _∋_; `_; #_; _,_; ★; ƛ_; _·_; _[_];
+     rename; ext; exts; Z; S_; subst; subst-zero)
 ```
 
 ## Parallel Reduction
@@ -270,7 +270,7 @@ and restate here.
 ```
 rename-subst-commute : ∀{Γ Δ}{N : Γ , ★ ⊢ ★}{M : Γ ⊢ ★}{ρ : Rename Γ Δ }
     → (rename (ext ρ) N) [ rename ρ M ] ≡ rename ρ (N [ M ])
-rename-subst-commute {N = N} = plfa.Substitution.rename-subst-commute {N = N}
+rename-subst-commute {N = N} = plfa.part2.Substitution.rename-subst-commute {N = N}
 ```
 
 Now for the `par-rename` lemma.
@@ -324,7 +324,7 @@ and restate it below.
 ```
 subst-commute : ∀{Γ Δ}{N : Γ , ★ ⊢ ★}{M : Γ ⊢ ★}{σ : Subst Γ Δ }
     → subst (exts σ) N [ subst σ M ] ≡ subst σ (N [ M ])
-subst-commute {N = N} = plfa.Substitution.subst-commute {N = N}
+subst-commute {N = N} = plfa.part2.Substitution.subst-commute {N = N}
 ```
 
 We are ready to prove that substitution respects parallel reduction.

src/plfa/part2/DeBruijn.lagda.md

@@ -7,7 +7,7 @@ next      : /More/
 ---
 
 ```
-module plfa.DeBruijn where
+module plfa.part2.DeBruijn where
 ```
 
 The previous two chapters introduced lambda calculus, with a

src/plfa/part2/Inference.lagda.md

@@ -7,7 +7,7 @@ next      : /Untyped/
 ---
 
 ```
-module plfa.Inference where
+module plfa.part2.Inference where
 ```
 
 So far in our development, type derivations for the corresponding
@@ -262,7 +262,7 @@ can compare with our previous development, we import
 module `pfla.DeBruijn`:
 
 ```
-import plfa.DeBruijn as DB
+import plfa.part2.DeBruijn as DB
 ```
 
 The phrase `as DB` allows us to refer to definitions

src/plfa/part2/Lambda.lagda.md

@@ -7,7 +7,7 @@ next      : /Properties/
 ---
 
 ```
-module plfa.Lambda where
+module plfa.part2.Lambda where
 ```
 
 The _lambda-calculus_, first published by the logician Alonzo Church in

src/plfa/part2/More.lagda.md

@@ -7,7 +7,7 @@ next      : /Bisimulation/
 ---
 
 ```
-module plfa.More where
+module plfa.part2.More where
 ```
 
 So far, we have focussed on a relatively minimal language, based on

src/plfa/part2/Properties.lagda.md

@@ -7,7 +7,7 @@ next      : /DeBruijn/
 ---
 
 ```
-module plfa.Properties where
+module plfa.part2.Properties where
 ```
 
 This chapter covers properties of the simply-typed lambda calculus, as
@@ -31,8 +31,8 @@ open import Data.Product
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Function using (_∘_)
-open import plfa.Isomorphism
-open import plfa.Lambda
+open import plfa.part1.Isomorphism
+open import plfa.part2.Lambda
 ```
 
 

src/plfa/part2/Substitution.lagda.md

@@ -8,7 +8,7 @@ next      : /Acknowledgements/
 
 
 ```
-module plfa.Substitution where
+module plfa.part2.Substitution where
 ```
 
 ## Introduction
@@ -46,14 +46,13 @@ system that _decides_ whether any two substitutions are equal.
 ## Imports
 
 ```
-open import plfa.Untyped
-  using (Type; Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_;
-         rename; subst; ext; exts; _[_]; subst-zero)
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; cong; cong₂; cong-app)
 open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
 open import Function using (_∘_)
--- open import plfa.Isomorphism using (extensionality)  -- causes a bug!
+open import plfa.part2.Untyped
+     using (Type; Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_;
+            rename; subst; ext; exts; _[_]; subst-zero)
 ```
 
 ```

src/plfa/part2/Untyped.lagda.md

@@ -7,7 +7,7 @@ next      : /Confluence/
 ---
 
 ```
-module plfa.Untyped where
+module plfa.part2.Untyped where
 ```
 
 In this chapter we play with variations on a theme:

src/plfa/part3/Adequacy.lagda.md

@@ -1,5 +1,5 @@
 ---
-title     : "Adequacy: Adequacy of denotational semantics with respect to operational semantics"
+title     : "Adequacy: Adequacy of denotational semantics with respect to operational semantics 🚧"
 layout    : page
 prev      : /Soundness/
 permalink : /Adequacy/
@@ -7,7 +7,7 @@ next      : /ContextualEquivalence/
 ---
 
 ```
-module plfa.Adequacy where
+module plfa.part3.Adequacy where
 ```
 
 ## Introduction
@@ -70,21 +70,6 @@ The rest of this chapter is organized as follows.
 ## Imports
 
 ```
-open import plfa.Untyped
-  using (Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_;
-         rename; subst; ext; exts; _[_]; subst-zero;
-         _—↠_; _—→⟨_⟩_; _∎; _—→_; ξ₁; ξ₂; β; ζ)
-open import plfa.CallByName
-  using (Clos; clos; ClosEnv; ∅'; _,'_; _⊢_⇓_; ⇓-var; ⇓-lam; ⇓-app; ⇓-determ;
-         cbn→reduce)
-open import plfa.Denotational
-  using (Value; Env; `∅; _`,_; _↦_; _⊑_; _⊢_↓_; ⊥; Funs∈; _⊔_; ∈→⊑;
-         var; ↦-elim; ↦-intro; ⊔-intro; ⊥-intro; sub; ℰ; _≃_; _iff_;
-         Trans⊑; ConjR1⊑; ConjR2⊑; ConjL⊑; Refl⊑; Fun⊑; Bot⊑; Dist⊑;
-         sub-inv-fun)
-open import plfa.Soundness using (soundness)
-open import plfa.Substitution using (ids; sub-id)
-
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app)
 open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
@@ -96,6 +81,21 @@ open import Data.Empty using (⊥-elim) renaming (⊥ to Bot)
 open import Data.Unit
 open import Relation.Nullary using (Dec; yes; no)
 open import Function using (_∘_)
+open import plfa.part2.Untyped
+     using (Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_;
+            rename; subst; ext; exts; _[_]; subst-zero;
+            _—↠_; _—→⟨_⟩_; _∎; _—→_; ξ₁; ξ₂; β; ζ)
+open import plfa.part2.Substitution using (ids; sub-id)
+open import plfa.part2.BigStep
+     using (Clos; clos; ClosEnv; ∅'; _,'_; _⊢_⇓_; ⇓-var; ⇓-lam; ⇓-app; ⇓-determ;
+            cbn→reduce)
+open import plfa.part3.Denotational
+     using (Value; Env; `∅; _`,_; _↦_; _⊑_; _⊢_↓_; ⊥; Funs∈; _⊔_; ∈→⊑;
+            var; ↦-elim; ↦-intro; ⊔-intro; ⊥-intro; sub; ℰ; _≃_; _iff_;
+            Trans⊑; ConjR1⊑; ConjR2⊑; ConjL⊑; Refl⊑; Fun⊑; Bot⊑; Dist⊑;
+            sub-inv-fun)
+open import plfa.part3.Soundness using (soundness)
+
 ```
 
 

src/plfa/part3/Compositional.lagda.md

@@ -1,5 +1,5 @@
 ---
-title     : "Compositional: The denotational semantics is compositional"
+title     : "Compositional: The denotational semantics is compositional 🚧"
 layout    : page
 prev      : /Denotational/
 permalink : /Compositional/
@@ -7,7 +7,7 @@ next      : /Soundness/
 ---
 
 ```
-module plfa.Compositional where
+module plfa.part3.Compositional where
 ```
 
 ## Introduction
@@ -27,19 +27,18 @@ with such a definition and prove that it is equivalent to ℰ.
 ## Imports
 
 ```
-open import plfa.Untyped
-  using (Context; _,_; ★; _∋_; _⊢_; `_; ƛ_; _·_)
-open import plfa.Denotational
-  using (Value; _↦_; _`,_; _⊔_; ⊥; _⊑_; _⊢_↓_;
-         Bot⊑; Fun⊑; ConjL⊑; ConjR1⊑; ConjR2⊑; Dist⊑; Refl⊑; Trans⊑; Dist⊔↦⊔;
-         var; ↦-intro; ↦-elim; ⊔-intro; ⊥-intro; sub;
-         up-env; ℰ; _≃_; ≃-sym; Denotation; Env)
-open plfa.Denotational.≃-Reasoning
-
 open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
   renaming (_,_ to ⟨_,_⟩)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Unit using (⊤; tt)
+open import plfa.part2.Untyped
+     using (Context; _,_; ★; _∋_; _⊢_; `_; ƛ_; _·_)
+open import plfa.part3.Denotational
+     using (Value; _↦_; _`,_; _⊔_; ⊥; _⊑_; _⊢_↓_;
+           Bot⊑; Fun⊑; ConjL⊑; ConjR1⊑; ConjR2⊑; Dist⊑; Refl⊑; Trans⊑; Dist⊔↦⊔;
+           var; ↦-intro; ↦-elim; ⊔-intro; ⊥-intro; sub;
+           up-env; ℰ; _≃_; ≃-sym; Denotation; Env)
+open plfa.part3.Denotational.≃-Reasoning
 ```
 
 ## Equation for lambda abstraction

src/plfa/part3/ContextualEquivalence.lagda.md

@@ -1,5 +1,5 @@
 ---
-title     : "ContextualEquivalence: Denotational equality implies contextual equivalence"
+title     : "ContextualEquivalence: Denotational equality implies contextual equivalence 🚧"
 layout    : page
 prev      : /Adequacy/
 permalink : /ContextualEquivalence/
@@ -7,21 +7,20 @@ next      : /Substitution/
 ---
 
 ```
-module plfa.ContextualEquivalence where
+module plfa.part3.ContextualEquivalence where
 ```
 
 ## Imports
 
 ```
-open import plfa.Untyped using (_⊢_; ★; ∅; _,_; ƛ_; _—↠_)
-open import plfa.Denotational using (ℰ; _≃_; ≃-sym; ≃-trans; _iff_)
-open import plfa.Compositional using (Ctx; plug; compositionality)
-open import plfa.Soundness using (soundness)
-open import plfa.Adequacy using (adequacy)
-open import plfa.CallByName using (_⊢_⇓_; cbn→reduce)
-
 open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
-  renaming (_,_ to ⟨_,_⟩)
+     renaming (_,_ to ⟨_,_⟩)
+open import plfa.part2.Untyped using (_⊢_; ★; ∅; _,_; ƛ_; _—↠_)
+open import plfa.part2.BigStep using (_⊢_⇓_; cbn→reduce)
+open import plfa.part3.Denotational using (ℰ; _≃_; ≃-sym; ≃-trans; _iff_)
+open import plfa.part3.Compositional using (Ctx; plug; compositionality)
+open import plfa.part3.Soundness using (soundness)
+open import plfa.part3.Adequacy using (adequacy)
 ```
 
 ## Contextual Equivalence

src/plfa/part3/Denotational.lagda.md

@@ -1,13 +1,13 @@
 ---
-title     : "Denotational: Denotational semantics of untyped lambda calculus"
+title     : "Denotational: Denotational semantics of untyped lambda calculus 🚧"
 layout    : page
-prev      : /CallByName/
+prev      : /BigStep/
 permalink : /Denotational/
 next      : /Compositional/
 ---
 
 ```
-module plfa.Denotational where
+module plfa.part3.Denotational where
 ```
 
 The lambda calculus is a language about _functions_, that is, mappings
@@ -61,14 +61,14 @@ open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; p
     renaming (_,_ to ⟨_,_⟩)
 open import Data.Sum
 open import Agda.Primitive using (lzero)
-open import plfa.Untyped
-    using (Context; ★; _∋_; ∅; _,_; Z; S_; _⊢_; `_; _·_; ƛ_;
-           #_; twoᶜ; ext; rename; exts; subst; subst-zero; _[_])
-open import plfa.Substitution using (Rename; extensionality; rename-id)
 open import Relation.Nullary using (¬_)
 open import Relation.Nullary.Negation using (contradiction)
 open import Data.Empty using (⊥-elim)
 open import Function using (_∘_)
+open import plfa.part2.Untyped
+     using (Context; ★; _∋_; ∅; _,_; Z; S_; _⊢_; `_; _·_; ƛ_;
+            #_; twoᶜ; ext; rename; exts; subst; subst-zero; _[_])
+open import plfa.part2.Substitution using (Rename; extensionality; rename-id)
 ```
 
 

src/plfa/part3/Soundness.lagda.md

@@ -1,5 +1,5 @@
 ---
-title     : "Soundness: Soundness of reduction with respect to denotational semantics"
+title     : "Soundness: Soundness of reduction with respect to denotational semantics 🚧"
 layout    : page
 prev      : /Compositional/
 permalink : /Soundness/
@@ -7,7 +7,7 @@ next      : /Adequacy/
 ---
 
 ```
-module plfa.Soundness where
+module plfa.part3.Soundness where
 ```
 
 
@@ -33,18 +33,6 @@ expansion is false for most typed lambda calculi!
 ## Imports
 
 ```
-open import plfa.Untyped
-  using (Context; _,_; _∋_; _⊢_; ★; Z; S_; `_; ƛ_; _·_;
-         subst; _[_]; subst-zero; ext; rename; exts;
-         _—→_; ξ₁; ξ₂; β; ζ; _—↠_; _—→⟨_⟩_; _∎)
-open import plfa.Substitution using (Rename; Subst; ids)
-open import plfa.Denotational
-  using (Value; ⊥; Env; _⊢_↓_; _`,_; _⊑_; _`⊑_; `⊥; _`⊔_; init; last; init-last;
-         Refl⊑; Trans⊑; `Refl⊑; Env⊑; EnvConjR1⊑; EnvConjR2⊑; up-env;
-         var; ↦-elim; ↦-intro; ⊥-intro; ⊔-intro; sub;
-         rename-pres; ℰ; _≃_; ≃-trans)
-open import plfa.Compositional using (lambda-inversion; var-inv)
-
 open import Relation.Binary.PropositionalEquality
   using (_≡_; _≢_; refl; sym; cong; cong₂; cong-app)
 open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
@@ -55,7 +43,17 @@ open import Relation.Nullary.Negation using (contradiction)
 open import Data.Empty using (⊥-elim)
 open import Relation.Nullary using (Dec; yes; no)
 open import Function using (_∘_)
--- open import plfa.Isomorphism using (extensionality)  -- causes a bug!
+open import plfa.part2.Untyped
+     using (Context; _,_; _∋_; _⊢_; ★; Z; S_; `_; ƛ_; _·_;
+            subst; _[_]; subst-zero; ext; rename; exts;
+            _—→_; ξ₁; ξ₂; β; ζ; _—↠_; _—→⟨_⟩_; _∎)
+open import plfa.part2.Substitution using (Rename; Subst; ids)
+open import plfa.part3.Denotational
+     using (Value; ⊥; Env; _⊢_↓_; _`,_; _⊑_; _`⊑_; `⊥; _`⊔_; init; last; init-last;
+            Refl⊑; Trans⊑; `Refl⊑; Env⊑; EnvConjR1⊑; EnvConjR2⊑; up-env;
+            var; ↦-elim; ↦-intro; ⊥-intro; ⊔-intro; sub;
+            rename-pres; ℰ; _≃_; ≃-trans)
+open import plfa.part3.Compositional using (lambda-inversion; var-inv)
 ```
 
 ## Forward reduction preserves denotations