What was once a set-theoretic concept, forcing is now recognised as a very general tool with applications to many areas of logic. One such application, is for giving models of dependent type theories through presheaf and sheaf categories, where picking the base categories appropriately can yield some level of effects in the resulting type theory. In order to introduce these models, first we look at Kripke semantics, which gives a class of models sound and complete with respect to intuitionistic propositional logic. Then, by relaxing the definition of Kripke semantics, we will get Beth semantics, which are a helpful tool in proving completeness results and can model larger classes of effects. Respectively, these semantics will correspond to a proof-irrelevant version of presheaves and sheaves, paving the way for an introduction of the proof-irrelevant case.