Theory Morphisms in Church's Type Theory with Quotation and Evaluation

${\mathrm{C}\mathrm{T}\mathrm{T}}_{\mathrm{q}\mathrm{e}}$ is a version of Church’s type theory with global quotation and evaluation operators that is engineered to reason about the interplay of syntax and semantics and to formalize syntax-based mathematical algorithms. ${\mathrm{C}\mathrm{T}\mathrm{T}}_{\mathrm{u}\mathrm{q}\mathrm{e}}$ is a variant of ${\mathrm{C}\mathrm{T}\mathrm{T}}_{\mathrm{q}\mathrm{e}}$ that admits undefined expressions, partial functions, and multiple base types of individuals. It is better suited than ${\mathrm{C}\mathrm{T}\mathrm{T}}_{\mathrm{q}\mathrm{e}}$ as a logic for building networks of theories connected by theory morphisms. This paper presents the syntax and semantics of ${\mathrm{C}\mathrm{T}\mathrm{T}}_{\mathrm{u}\mathrm{q}\mathrm{e}}$, defines a notion of a theory morphism from one ${\mathrm{C}\mathrm{T}\mathrm{T}}_{\mathrm{u}\mathrm{q}\mathrm{e}}$ theory to another, and gives two simple examples that illustrate the use of theory morphisms in ${\rm CTT}_{\rm uqe}$.