Induced morphisms between Heyting-valued models
Abstract
To the best of our knowledge, there are very few results on how Heyting-valued models are affected by the morphisms on the complete Heyting algebras that determine them: the only cases found in the literature are concerning automorphisms of complete Boolean algebras and complete embedding between them (\emph{i.e}., injective Boolean algebra homomorphisms that preserves arbitrary suprema and arbitrary infima). In the present work, we consider and explore how more general kinds of morphisms between complete Heyting algebras and induce arrows between and , and between their corresponding localic toposes () and (). In more details: any {\em geometric morphism} , (that automatically came from a unique locale morphism ), can be "lifted" to an arrow . We also provide also some semantic preservation results concerning this arrow .
Cite
@article{arxiv.1910.08193,
title = {Induced morphisms between Heyting-valued models},
author = {José Goudet Alvim and Arthur Francisco Schwerz Cahali and Hugo Luiz Mariano},
journal= {arXiv preprint arXiv:1910.08193},
year = {2021}
}
Comments
28 pages