On the normal completion of a Boolean algebra

A familiar construction for a Boolean algebra A is its normal completion , given by its normal ideals or, equivalently, the intersections of its principal ideals, together with the embedding taking each element of A to its principal ideal. In the classical setting of Zermelo–Fraenkel set theory with Choice, is characterized in various ways; thus, it is the unique complete extension of A in which the image of A is join-dense, the unique essential completion of A, and the injective hull of A. Here, we are interested in characterizing the normal completion in the constructive context of an arbitrary topos. We show among other things that it is, even at this level, the unique join-dense, or alternatively, essential completion. En route, we investigate the functorial properties of and establish that it is the reflection of A, in the category of Boolean homomorphisms which preserve all existing joins, to the complete Boolean algebras. In this context, we make crucial use of the notion of a skeletal frame homomorphism.