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

Merge branch 'master' of github.com:wenkokke/sf

Browse source 
Merging in small fixes.
This commit is contained in:
wadler 2018-05-15 17:08:00 -03:00
commit 1c4796721e
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Connectives.lagda
View file

@ -663,7 +663,7 @@ is isomorphic to a function that accepts a pair of arguments:
Agda is optimised for currying, so `2 + 3` abbreviates `_+_ 2 3`.
In a language optimised for pairing, we would instead take `2 +′ 3` as
an abbreviation for `_+′_ (2 , 3)`.
an abbreviation for `_+′_ ⟨ 2 , 3 ⟩`.
Corresponding to the law
@ -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)