diff --git a/courses/puc/2019/Assignment1.lagda.md b/courses/puc/2019/Assignment1.lagda.md
index f2d6f269..8dd978c6 100644
--- a/courses/puc/2019/Assignment1.lagda.md
+++ b/courses/puc/2019/Assignment1.lagda.md
@@ -31,7 +31,7 @@ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
   ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
-open import plfa.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
+open import plfa.part1.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
 ```
 
 ## Naturals
diff --git a/courses/puc/2019/Assignment2.lagda.md b/courses/puc/2019/Assignment2.lagda.md
index 1aa06905..b51f2ca8 100644
--- a/courses/puc/2019/Assignment2.lagda.md
+++ b/courses/puc/2019/Assignment2.lagda.md
@@ -31,7 +31,6 @@ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
   ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
-open import plfa.Relations using (_<_; z<s; s<s)
 open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 open import Data.Product using (Σ; ∃; Σ-syntax; ∃-syntax)
 open import Data.Unit using (⊤; tt)
@@ -47,10 +46,10 @@ open import Relation.Nullary.Negation using (contraposition)
 open import Relation.Unary using (Decidable)
 open import Function using (_∘_)
 open import Level using (Level)
-open import plfa.Relations using (_<_; z<s; s<s)
-open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
-open plfa.Isomorphism.≃-Reasoning
-open import plfa.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
+open import plfa.part1.Relations using (_<_; z<s; s<s)
+open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open plfa.part1.Isomorphism.≃-Reasoning
+open import plfa.part1.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
   _++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
 ```
 
diff --git a/courses/puc/2019/Assignment3.lagda.md b/courses/puc/2019/Assignment3.lagda.md
index d43acb6a..4dba998e 100644
--- a/courses/puc/2019/Assignment3.lagda.md
+++ b/courses/puc/2019/Assignment3.lagda.md
@@ -39,13 +39,13 @@ open import Function using (_∘_)
 open import Algebra.Structures using (IsMonoid)
 open import Level using (Level)
 open import Relation.Unary using (Decidable)
-open import plfa.Relations using (_<_; z<s; s<s)
-open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
-open plfa.Isomorphism.≃-Reasoning
-open import plfa.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
+open import plfa.part1.Relations using (_<_; z<s; s<s)
+open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open plfa.part1.Isomorphism.≃-Reasoning
+open import plfa.part1.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
   _++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
-open import plfa.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
-open import plfa.Properties hiding (value?; unstuck; preserves; wttdgs)
+open import plfa.part2.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
+open import plfa.part2.Properties hiding (value?; unstuck; preserves; wttdgs)
 ```
 
 ## Lambda
diff --git a/courses/puc/2019/Assignment4.lagda.md b/courses/puc/2019/Assignment4.lagda.md
index 6d68956b..92b232e2 100644
--- a/courses/puc/2019/Assignment4.lagda.md
+++ b/courses/puc/2019/Assignment4.lagda.md
@@ -54,7 +54,7 @@ module DeBruijn where
 Remember to indent all code by two spaces.
 
 ```
-  open import plfa.DeBruijn
+  open import plfa.part2.DeBruijn
 ```
 
 
diff --git a/courses/puc/2019/Assignment5.lagda.md b/courses/puc/2019/Assignment5.lagda.md
index f915c2a7..ae0dc86a 100644
--- a/courses/puc/2019/Assignment5.lagda.md
+++ b/courses/puc/2019/Assignment5.lagda.md
@@ -55,7 +55,7 @@ Remember to indent all code by two spaces.
 ### Imports
 
 ```
-  import plfa.More as DB
+  import plfa.part2.More as DB
 ```
 
 ### Syntax
diff --git a/courses/tspl/2018/Assignment1.lagda.md b/courses/tspl/2018/Assignment1.lagda.md
index de5c4014..2b48c6a5 100644
--- a/courses/tspl/2018/Assignment1.lagda.md
+++ b/courses/tspl/2018/Assignment1.lagda.md
@@ -34,7 +34,7 @@ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
   ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
-open import plfa.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
+open import plfa.part1.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
 ```
 
 ## Naturals
diff --git a/courses/tspl/2018/Assignment2.lagda.md b/courses/tspl/2018/Assignment2.lagda.md
index 9d75e28c..7483a333 100644
--- a/courses/tspl/2018/Assignment2.lagda.md
+++ b/courses/tspl/2018/Assignment2.lagda.md
@@ -34,7 +34,6 @@ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
   ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
-open import plfa.Relations using (_<_; z<s; s<s)
 open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 open import Data.Unit using (⊤; tt)
 open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
@@ -47,9 +46,9 @@ open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Nullary.Sum using (_⊎-dec_)
 open import Relation.Nullary.Negation using (contraposition)
 open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
-open import plfa.Relations using (_<_; z<s; s<s)
-open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
-open plfa.Isomorphism.≃-Reasoning
+open import plfa.part1.Relations using (_<_; z<s; s<s)
+open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open plfa.part1.Isomorphism.≃-Reasoning
 ```
 
 ## Equality
diff --git a/courses/tspl/2018/Assignment3.lagda.md b/courses/tspl/2018/Assignment3.lagda.md
index 51c9d8ae..2cafa1b2 100644
--- a/courses/tspl/2018/Assignment3.lagda.md
+++ b/courses/tspl/2018/Assignment3.lagda.md
@@ -42,13 +42,13 @@ open import Function using (_∘_)
 open import Algebra.Structures using (IsMonoid)
 open import Level using (Level)
 open import Relation.Unary using (Decidable)
-open import plfa.Relations using (_<_; z<s; s<s)
-open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
-open plfa.Isomorphism.≃-Reasoning
-open import plfa.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
+open import plfa.part1.Relations using (_<_; z<s; s<s)
+open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open plfa.part1.Isomorphism.≃-Reasoning
+open import plfa.part1.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
   _++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
-open import plfa.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
-open import plfa.Properties hiding (value?; unstuck; preserves; wttdgs)
+open import plfa.part2.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
+open import plfa.part2.Properties hiding (value?; unstuck; preserves; wttdgs)
 ```
 
 #### Exercise `reverse-++-commute` (recommended)
diff --git a/courses/tspl/2018/Assignment4.lagda.md b/courses/tspl/2018/Assignment4.lagda.md
index f5fb3774..9a9829ed 100644
--- a/courses/tspl/2018/Assignment4.lagda.md
+++ b/courses/tspl/2018/Assignment4.lagda.md
@@ -57,7 +57,7 @@ module DeBruijn where
 Remember to indent all code by two spaces.
 
 ```
-  open import plfa.DeBruijn
+  open import plfa.part2.DeBruijn
 ```
 
 
@@ -770,7 +770,7 @@ Remember to indent all code by two spaces.
 ### Imports
 
 ```
-  import plfa.More as DB
+  import plfa.part2.More as DB
 ```
 
 ### Syntax
diff --git a/courses/tspl/2018/Exam.lagda.md b/courses/tspl/2018/Exam.lagda.md
index c90d1046..fc8c7b1f 100644
--- a/courses/tspl/2018/Exam.lagda.md
+++ b/courses/tspl/2018/Exam.lagda.md
@@ -398,7 +398,7 @@ module Problem3 where
 ### Imports
 
 ```
-  import plfa.DeBruijn as DB
+  import plfa.part2.DeBruijn as DB
 ```
 
 ### Syntax