Topos theory can be used to abstract models of higher-order logic the same way Heyting algebras can be used for propositional logic. A topos is a cartesian closed category that satisfies certain properties (e.g. the category of sets is a topos), but it is interesting to see whether it also satisfies some of these:

(1) The internal logic of the topos has the law of excluded middle (2) Every morphism of the topos is computable (3) The topos has an object of natural integers (definition of Lawvere)

With these three properties, the halting problem can be proved computable; hence, a (non-degenerated) topos cannot have these three properties at the same time:

• With properties (1) and (3), we have classical logic: the category of sets is a good example.
• With properties (1) and (2), we have finite logic: the category of finite sets is a good example

• With properties (2) and (3), we have intuitionistic logic.

  One of the most famous topos satisfying these two properties is Hyland's effective topos, which can be seen as the universe of realisability. While it is quite simple to check that the category of sets and the category of finite sets are topos, proving that the effective topos is indeed a topos is much harder.

We introduce here an alternative definition of Hyland's effective topos, based on a realisability framework with two levels of abstraction: a low level and a high level. With this definition, the proof that this framework forms a topos is almost as simple as proving that the category of sets is a topos. Moreover, the high level of the framework can be directly used as a model of higher-order intuitionistic systems.

Indeed, topos satisfying (2) and (3) are the most interesting ones for computer science because they ensure that a programming language based on topos theory can be given a constructive semantics. In such a programming language, we can only write functions that terminate, as in proof assistants like Coq, so the language cannot be Turing-complete. The main advantage of having a programming language based on topos theory over more usual intuitionistic systems such as Martin-Loef type theory is the notion of equality: it is extensional, has proof-irrelevance, and allows the axiom of unique choice.