There is a statement and proof of Gelfand duality in constructive mathematics. This therefore makes sense in any topos.
A proof of Gelfand duality claimed to be constructive was given in.
This uses however Barr's theorem which requires itself non-constructive logic and requires the ambient topos to be a Grothendieck topos
A fully constructive proof is claimed in
A review of some aspects of constructive Gelfand duality (with an eye towards Bohr toposes) is in
Further disussion includes
Simon Henry, Constructive Gelfand duality for non-unital commutative $C^\ast$-algebras (arXiv:1412.2009)
Simon Henry, Localic Metric spaces and the localic Gelfand duality (arXiv:1411.0898)
Last revised on June 3, 2017 at 09:11:04. See the history of this page for a list of all contributions to it.