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

More: fixes the projection function used in the informal definition of from×⊤ (#533)

Browse source
This commit is contained in:
Marko Dimjašević 2020-10-24 17:03:53 +02:00 committed by GitHub
parent c70e990c29
commit 753029e3ad
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/plfa/part2/More.lagda.md
View file

@ -381,7 +381,7 @@ Here is the isomorphism between `A` and ``A `× `⊤``:
to×⊤ = ƛ x ⇒ `⟨ x , `tt ⟩ to×⊤ = ƛ x ⇒ `⟨ x , `tt ⟩
from×⊤ : ∅ ⊢ A `× `⊤ ⇒ A from×⊤ : ∅ ⊢ A `× `⊤ ⇒ A
from×⊤ = ƛ z ⇒ proj₁ z from×⊤ = ƛ z ⇒ `proj₁ z
## Alternative formulation of unit type ## Alternative formulation of unit type