 The fibred semantics of modal logics was originally proposed in Gabbay 1996a and Gabbay 1996b (see also Gabbay 1999). As in the case of fusion and products, the mechanism of fibring also applies to modal logics only. Assume the same notation as in  subsection 4.1.  Thus, given \({{\cal L}}_1\) and \({{\cal L}}_2\), we start by defining the fibred language (or the fibring of the languages), which is the language generated by \(\square_1\), \(\square_2\), \(\neg\) and \(\to\) from the propositional variables. The basic idea is to consider Kripke models with distinguished (actual) worlds together with two transfer mappings: \(h_1\) from the set of worlds of the class of models \({{\cal M}}_1\) of \({{\cal L}}_1\) into the class of models \({{\cal M}}_2\) of \({{\cal L}}_2\), and \(h_2\) from the set of worlds of the class of models \({{\cal M}}_2\) of \({{\cal L}}_2\) into the class of models \({{\cal M}}_1\) of \({{\cal L}}_1\). When a Kripke model of \({{\cal L}}_1\) has to evaluate a formula of the form \(\square_2 \varphi\) at the actual world \(w_1\), the validity checking is then transferred to the validity checking of \(\square_2 \varphi\) within the Kripke model \(h_1(w_1)\) at its actual world. The evaluation of a formula of the form \(\square_1 \varphi\) within a Kripke model of \({{\cal L}}_2\) at the actual world \(w_2\) is performed analogously, but now using the map \(h_2\).