Merge pull request #530 from mdimjasevic/more-prod-proj

More: fixes an informal definition of swap×
This commit is contained in:
Philip Wadler 2020-10-14 20:57:41 +01:00 committed by GitHub
commit 2ef2824d3a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -206,7 +206,7 @@ construct to a calculus without the construct.
Here is a function to swap the components of a pair:
swap× : ∅ ⊢ A `× B ⇒ B `× A
swap× = ƛ z ⇒ `⟨ proj₂ z , proj₁ z ⟩
swap× = ƛ z ⇒ `⟨ `proj₂ z , `proj₁ z ⟩
## Alternative formulation of products