michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge branch 'dev' of github.com:plfa/plfa.github.io into dev

Browse source
This commit is contained in:
wadler 2021-08-29 18:37:14 +01:00
commit af45cdcfdb
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/plfa/part1/Quantifiers.lagda.md
View file

@ -105,7 +105,7 @@ Show that a disjunction of universals implies a universal of disjunctions:
``` ```
postulate postulate
⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} → ⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} →
(∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
``` ```
Does the converse hold? If so, prove; if not, explain why. Does the converse hold? If so, prove; if not, explain why.
@ -463,21 +463,21 @@ And to establish the following properties:
to (from b) ≡ b to (from b) ≡ b
Using the above, establish that there is an isomorphism between `ℕ` and Using the above, establish that there is an isomorphism between `ℕ` and
`∃[ b ](Can b)`. `∃[ b ] Can b`.
We recommend proving the following lemmas which show that, for a given We recommend proving the following lemmas which show that, for a given
binary number `b`, there is only one proof of `One b` and similarly binary number `b`, there is only one proof of `One b` and similarly
for `Can b`. for `Can b`.
≡One : ∀{b : Bin} (o o' : One b) → o ≡ o' ≡One : ∀ {b : Bin} (o o′ : One b) → o ≡ o′
≡Can : ∀{b : Bin} (cb : Can b) (cb' : Can b) → cb ≡ cb' ≡Can : ∀ {b : Bin} (cb cb′ : Can b) → cb ≡ cb′
Many of the alternatives for proving `to∘from` turn out to be tricky. Many of the alternatives for proving `to∘from` turn out to be tricky.
However, the proof can be straightforward if you use the following lemma, However, the proof can be straightforward if you use the following lemma,
which is a corollary of `≡Can`. which is a corollary of `≡Can`.
proj₁≡→Can≡ : {cb cb′ : ∃[ b ](Can b)} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′ proj₁≡→Can≡ : {cb cb′ : ∃[ b ] Can b} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′
``` ```
-- Your code goes here -- Your code goes here