Note to “Continuous domains as formal spaces”, Mathematical Structures in Computer Science (2002), vol. 12, pp. 19–52. Sara Negri

On page 26-27 a general method is described for proving equivalences between categories: A full and faithful functor that restricts and corestricts to a dense functor between full subcategories is an equivalence. However QFTop is not a full subcategory of FTop.

In order to prove that the equivalence between QFtop and SL restricts to an equivalence between FTop and Frm observe that, given any two formal topologies A and B, the functor Sat gives a bijection between FTop(A, B) and Frm(Sat(A), Sat(B)). Given the inclusion of categories, it is enough to verify that for f in FTop(A, B), Sat(f) preserves the meet operation, and that the inverse map is in FTop, that is, condition 2 of Definition 2.4 is satisfied. These properties are immediate consequence of the definition of meet in Sat(A) (page 23),

AU ∧ AV ≡ AU ∩ AV = A(U ⊓ V)

Page 31, proof of Proposition 2.17: It is said Pos/Pos is a frame morphism. Correct to “left adjoint to a frame map”.