From adc4d3abb2c7bca12cda0a0c8b45caf489147375 Mon Sep 17 00:00:00 2001 From: wadler Date: Sat, 26 May 2018 12:22:30 -0300 Subject: [PATCH] minor update to Naturals --- src/Connectives.lagda | 7 ++++--- src/Naturals.lagda | 4 ++-- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Connectives.lagda b/src/Connectives.lagda index 81b2328e..203347b3 100644 --- a/src/Connectives.lagda +++ b/src/Connectives.lagda @@ -770,11 +770,12 @@ embedding, revealing a sense in which one of these laws is "more true" than the other. -### Exercise (`×⊎-implies-⊎×`) +### Exercise (`⊎×-implies-×⊎`) -Show that a conjunct of disjuncts implies a disjunct of conjuncts. +Show that a disjunct of conjuncts implies a conjunct of disjuncts. \begin{code} -×⊎-Implies-⊎× = ∀ {A B C D : Set} → (A ⊎ B) × (C ⊎ D) → (A × C) ⊎ (B × D) +postulate + ⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D) \end{code} Does the converse hold? If so, prove; if not, explain why. diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 86f95c3f..57e431f5 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -82,8 +82,8 @@ zero or more *judgments* written above a horizontal line, called the *conclusion*. The first rule is the base case. It has no hypotheses, and the conclusion asserts that `zero` is a natural. The second rule is the inductive case. It has one hypothesis, which assumes that `m` -is a natural, and the conclusion asserts that `suc n` is a also a -natural. +is a natural, and in that case the conclusion asserts that `suc n` +is a also a natural. ## Unpacking the Agda definition