Insertion of continuous real functions on spaces, bispaces, ordered spaces and pointfree spaces -- a common root (Q535362)

A biframe is a triple consisting of a frame (called the total part of the biframe) and two subframes which together generate the total part. In the same way that a frame has its co-frame of sublocales which can be made into a frame by reverse inclusion, a biframe also has what could informally be called a ``biframe of sublocales''. For a given biframe, the authors define a real function (not necessarily continuous) on the biframe to be a real function on the first part of the ``biframe of sublocales'' which is a biframe homomorphism from the biframe of reals to the given biframe. This done, they then characterise normal and extremally disconnected biframes in terms of insertion of continuous real functions between given lower and upper semicontinuous real functions. The various insertion-type theorems (and characterisations of normality and extremal disconnectedness) for frames, topological spaces, ordered topological spaces and bispaces appear as special cases of similar results for biframes. This fully justifies the appendage ``a common root'' in the title of the paper.