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

products distributes -> product distributes

Browse source
This commit is contained in:
Juhana Laurinharju 2018-05-14 22:09:32 +03:00
parent 5ffb1c9876
commit 19b2cda6b9
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
Product distributes 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)