A globalisation of the Gelfand duality theorem

In this paper we bring together results from a series of previous papers to prove the constructive version of the Gelfand duality theorem in any Grothendieck topos E, obtaining a dual equivalence between the category of commutative C∗-algebras and the category of compact, completely regular locales in the topos E.