Contents

Idea

Kripke–Joyal semantics is a natural semantics in a topos.

The Mitchell–Bénabou language of a topos is a higher-order type theory in which one can write ordinary mathematics, which can then be interpreted in the topos using the Kripke–Joyal semantics.

References

Textbook introductions include

section VI.6 of

Lecture notes include

Revised on August 14, 2014 08:57:43 by Bas Spitters (83.128.115.142)