# 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

(page 58 and following)

Revised on November 10, 2011 03:07:30 by Toby Bartels (64.89.53.18)