Sheaves of structures, Heyting-valued structures, and a generalization of Los's theorem

Sheaves of structures are useful to give constructions in universal algebra and model theory. We can describe their logical behavior in terms of Heyting-valued structures. In this paper, we first provide a systematic treatment of sheaves of structures and Heyting-valued structures from the viewpoint of categorical logic. We then prove a form of Los's theorem for Heyting-valued structures. We also give a characterization of Heyting-valued structures for which Los's theorem holds with respect to any maximal filter.