Compact spaces and distributive lattices

This note presents a general construction connecting compact locales and distributive lattices, that allows us to reduce results about compactness of locales to theorems about distributive lattices. Two applications are given. One noteworthy feature of our arguments is that they can be formulated both in topos theory and in a predicative theory such as CZF.