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..