From 306d881b1a3da7bb75b5f2825d7ed711ee6de03f Mon Sep 17 00:00:00 2001 From: Murilo Giacometti Rocha <43705847+murilogiacometti@users.noreply.github.com> Date: Sun, 30 Sep 2018 13:26:56 +0100 Subject: [PATCH] Fix small typo ("Russel" vs "Russell") --- src/plfa/Equality.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/Equality.lagda b/src/plfa/Equality.lagda index e0cd8121..1326ed32 100644 --- a/src/plfa/Equality.lagda +++ b/src/plfa/Equality.lagda @@ -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. 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, where `Set : Set₁`, `Set₁ : Set₂`, and so on. In fact, `Set` itself is just an abbreviation for `Set₀`. Since the equation defining `_≐_`