From 6db78d33201e5d8a6e6b7a0e92b8a03b603ed7bf Mon Sep 17 00:00:00 2001
From: hafniz <42380178+hafniz@users.noreply.github.com>
Date: Wed, 13 Nov 2024 13:00:30 +0000
Subject: [PATCH] Use double substitution for alternative formulation of
 products

---
 src/plfa/part2/More.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md
index a1cc84c3e..af7b7d4ef 100644
--- a/src/plfa/part2/More.lagda.md
+++ b/src/plfa/part2/More.lagda.md
@@ -268,7 +268,7 @@ One might think that we could instead use a more compact translation:
     -- WRONG
       (case× L [⟨ x , y ⟩⇒ N ]) †
     =
-      (N †) [ x := `proj₁ (L †) ] [ y := `proj₂ (L †) ]
+      (N †) [ x := `proj₁ (L †) ][ y := `proj₂ (L †) ]
 
 But this behaves differently.  The first term always reduces `L`
 before `N`, and it computes `` `proj₁ `` and `` `proj₂ `` exactly once.  The
@@ -299,7 +299,7 @@ We can also translate back the other way:
       `inj₂ W                             inject second component
 
 ### Typing
-⊥
+
     Γ ⊢ M ⦂ A
     -------------------- `inj₁ or ⊎-I₁
     Γ ⊢ `inj₁ M ⦂ A `⊎ B