Open existential record so that short names can be used

Jefferson Carpenter · Jefferson Carpenter · commit 345b7d6ab131 · 2025-01-23T09:34:33.000Z
diff --git 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₁`.
