How to construct a product of a-frames (Q2910982)

This paper is developed in the framework of constructive lattice theory, where constructive mathematics is defined as mathematics that uses intuitionistic logic'' in the style of E. Bishop. It presents a notion of a-frame, which in particular is a complete lattice, i.e. admits arbitrary joins. (It thus seems to the reviewer that, in opposition of what is stated in Footnote 2, non-trivial examples can only be produced using some form of impredicativity.) The question which is analyzed is then when one can put a structure of a-frame on a product of two a-frames where such a product is characterized abstractly by some axioms listed in Section 2. A crucial role is played by a new notion of ``decency'' for lattice. A lattice is ``decent'' if \(x\leqslant y\) follows from \(x\neq 0\rightarrow x\leqslant y\) (a notion which classically always holds but is intuitionistically non-trivial).