From bfff110f308b1ade572d3a81023ec0769bc27476 Mon Sep 17 00:00:00 2001 From: Owen Shepherd Date: Thu, 25 Dec 2025 22:45:57 +0000 Subject: [PATCH] Clarify type-in-type assignment section When I first read this, it sounded like the problem was 'assigning Type to Type', but the problem is really 'making the type of Type equal to Type'. I think this can be made clearer by saying 'the type *of* Type'. --- book/FPLean/FunctorApplicativeMonad/Universes.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/FPLean/FunctorApplicativeMonad/Universes.lean b/book/FPLean/FunctorApplicativeMonad/Universes.lean index 0ba803f..c265d54 100644 --- a/book/FPLean/FunctorApplicativeMonad/Universes.lean +++ b/book/FPLean/FunctorApplicativeMonad/Universes.lean @@ -50,7 +50,7 @@ This is a contradiction, which demonstrates that something was wrong with the in In particular, allowing sets to be constructed by providing an arbitrary property is too powerful. Later versions of set theory restrict the formation of sets to remove the paradox. -A related paradox can be constructed in versions of dependent type theory that assign the type {anchorTerm SomeTypes}`Type` to {anchorTerm SomeTypes}`Type`. +A related paradox can be constructed in versions of dependent type theory that assign the type of {anchorTerm SomeTypes}`Type` to {anchorTerm SomeTypes}`Type`. To ensure that Lean has consistent logical foundations and can be used as a tool for mathematics, {anchorTerm SomeTypes}`Type` needs to have some other type. This type is called {anchorTerm SomeTypes}`Type 1`: ```anchor TypeType