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

Merge pull request #20 from Fingerzam/connectives-product-distributes

Browse source 
Fix typo: products distributes -> product distributes
This commit is contained in:
wadler 2018-05-15 13:09:30 -03:00 • committed by GitHub
commit 20c87f503d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Connectives.lagda
View file

@ -713,7 +713,7 @@ and the rule `η-×` for products.
## Distribution
Products distributes over sum, up to isomorphism. The code to validate
Products distribute over sum, up to isomorphism. The code to validate
this fact is similar in structure to our previous results.
\begin{code}
×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)