Construction of a monadic Heyting algebra in a logos

Connections between certain types of categories (logoses and toposes) and intuitionistic predicate logic was established in 1960–1970 by Lowvere. The possibility of extending this connection to some types of modal logics by using the internal structure of categories of particular type (logos) was also established. Category-theoretical constructs were hence used as one of the possible semantic interpretations of intuitionistic logic. This interpretation has also included intuionistic modal logics using different semantical tools such as adjoint pair of functors. In this paper, we discuss one of the possible extension of intuitionistic logic.