diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md
index 4c943d7e4..3f0e88ee7 100644
--- a/src/plfa/part1/Quantifiers.lagda.md
+++ b/src/plfa/part1/Quantifiers.lagda.md
@@ -141,6 +141,7 @@ record Σ (A : Set) (B : A → Set) : Set where
   field
     proj₁ : A
     proj₂ : B proj₁
+open Σ
 ```
 Here we have a dependent record, where the type of `proj₂`
 refers to the field `proj₁`.