AlexMennen comments on Scott Garrabrant’s problem on recovering Brouwer as a corollary of Lawvere

• Let α be the least countable ordinal such that there is no polynomial-time computable recursive well-ordering of length α.