# A polytime feasible subuniverse of the Effective Topos

The effective topos is a well known universe of sets suitable for abstract computability, as it is build "from the ground up" via the classical notion of realisability by Kleene.

I have found a few articles on the web which develop notions of polynomial time realizability, such as this one, so I wonder if there has been some attempt to carve out of the effective topos a subuniverse of "polytime feasible sets".

Any ref is appreciated.

ADDENDUM: My simple-minded idea would be to consider the Heyting algebra $H$ of subsets of codes, equipped with an additional operator $\pi$ which extracts the polytime codes $\pi: H\rightarrow H$ from each subset (this corresponds to accepting only the constructions/proofs which are feasible, and reject the others).$\pi$ is not to be expected to be an heyting algebra endomap, but I think it is at least a meet semilattice one. So this should induce an exact endofunctor on Hyland's topos, and the feasible subuniverse would probably be its fixed points..

-
Doesn't Seely's paper you reference do what you want, more or less. By the way, I don't think you can get an honest Heyting algebra here. You will have to fiddle with implications and make them weird in order to keep the complexity of realizers down. –  Andrej Bauer May 31 '11 at 22:05
Unless I missed the point, it is more less than more, though I think it is perhaps a starting point to bake the feasible universe. As for the Heyting algebra, perhaps I misunderstand u, but my point was: start from the canonical Heyting algebra for the effective topos (ie you take ALL subsets of ALL codes, not just the polytime ones). Then, construct an meet-semilattice of this algebra, that basically takes a subset of all recursive codes and picks the polytime ones (some kind of interior operator). I do not expect the fixed points for this operator to form an Heyting algebra, only a lattice –  Mirco Mannucci May 31 '11 at 22:20
Perhaps your operator is a $j$-operator, although someone would have noticed that by now. –  Andrej Bauer Jun 1 '11 at 6:38
I think it is not: the $j$-operator maps Truth to Truth, but here the Truth is the entire set of codes. This is ok, because I do not expect the polytime feasible subcategory of the effective topos to be a topos. Would be interesting though to know what property such a cat has, and how it sits in the effective topos. –  Mirco Mannucci Jun 2 '11 at 11:11