# Partitions of unity in constructive mathematics

Can someone point me to any substitutes for the partition of unity in Bishop's constructive mathematics?

In particular, under what circumstances can we construct a partition of unity subordinate to some open cover of a compact set in Euclidean space?

In my PhD thesis modern intuitionistic topology in chapter 3 there is a comprehensive treatment of partitions of unity within BISH.

In essence the main theorem is that per-enumerable open covers of a metric space admit a subordinate partition of unity. An open cover is per-enumerable iff it is an enumerable collection of open sets which themselves are an enumerable union of basic open metric balls (where the base point comes from a fixed enumerable dense set.)

• sorry the link was defective... but should work now. Jun 25 '18 at 17:03
• Can your result be related to complete regularity (every open set is the inverse image of $(0, 1)$)? Jun 25 '18 at 19:03