From 00a04e43d191c072cda70fc1131740121975e36c Mon Sep 17 00:00:00 2001 From: wadler Date: Sat, 26 Jun 2021 15:43:48 +0100 Subject: [PATCH] small fix to Connectives --- src/plfa/part1/Connectives.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part1/Connectives.lagda.md b/src/plfa/part1/Connectives.lagda.md index 17d73e33..df116b15 100644 --- a/src/plfa/part1/Connectives.lagda.md +++ b/src/plfa/part1/Connectives.lagda.md @@ -58,8 +58,8 @@ Evidence that `A × B` holds is of the form `⟨ M , N ⟩`, where `M` provides evidence that `A` holds and `N` provides evidence that `B` holds. -Given evidence that `A × B` holds, we can conclude that either -`A` holds or `B` holds: +Given evidence that `A × B` holds, we can conclude that both +`A` holds and `B` holds: ``` proj₁ : ∀ {A B : Set} → A × B