Crisp type theory is a kind of modal type theory that features in semantic investigations of homotopy type theory. Kripke-Joyal forcing is a technique for relating two kinds of reasoning in a category: the standard, diagrammatic method and the logical approach of reasoning with judgements in an “internal type theory”. I will explain why we want to reason with crisp type theory as the internal language of some category and how we can set this up by first introducing fibred models of crisp type theory. I will include plenty of background and motivation.