 the language context corresponds to a type language. Two
theories can be linked by a theory morphism, as illustrated by the
theory morphism <span style="font-weight: bold; font-style: italic;">f</span>
: <span style="font-weight: bold; font-style: italic;">T</span><small><sub>1</sub></small>
&#8594; <span style="font-weight: bold; font-style: italic;">T</span><small><sub>2</sub></small>
in the upper left part of the theory
context in Figure 3. The closure construction <span
 style="font-family: arial; font