News for hackers. Stuff that matters.
Re:Foundations of Mathematics (2015) [pdf] by Gondolin on Monday June 03, 2019 @11:49AM (#20084490)
More precisely the effective topos is a kind of realizability topos with a nno where every function is computable. Such a (non trivial) topos cannot be classical, otherwise the halting problem would be decidable. However the effective topos can only deal with calculability, not complexity. For complexity linear logic (without exponentials) and symmetric monoidal categories are better suited (but I don't know if there exists a model where every function is in P for instance).

There are no comments on this comment yet.