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

Merge pull request #68 from murilogiacometti/patch-2

Browse source 
Fix small typo ("Russel" vs "Russell")
This commit is contained in:
wadler 2018-10-02 12:03:48 +01:00 • committed by GitHub
commit 26e1754860
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/Equality.lagda
View file

@ -528,7 +528,7 @@ and instead we write `_≐_ {A} x y` to provide access to the implicit
parameter `A` which appears on the right-hand side. parameter `A` which appears on the right-hand side.
This is our first use of _levels_. We cannot assign `Set` the type This is our first use of _levels_. We cannot assign `Set` the type
`Set`, since this would lead to contradictions such as Russel's `Set`, since this would lead to contradictions such as Russell's
Paradox and Girard's Paradox. Instead, there is a hierarchy of types, Paradox and Girard's Paradox. Instead, there is a hierarchy of types,
where `Set : Set₁`, `Set₁ : Set₂`, and so on. In fact, `Set` itself where `Set : Set₁`, `Set₁ : Set₂`, and so on. In fact, `Set` itself
is just an abbreviation for `Set₀`. Since the equation defining `_≐_` is just an abbreviation for `Set₀`. Since the equation defining `_≐_`