constructive Gelfand duality theorem
Cohomology and homotopy
In higher category theory
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.
- Bernhard Banaschewski; Christopher J. Mulvey A globalisation of the Gelfand duality theorem Annals of Pure and Applied Logic, 137(1–3):62–103, 2006
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
- Thierry Coquand, Bas Spitters, Constructive Gelfand duality for -algebras , Mathematical Proceedings of the Cambridge Philosophical society , Volume 147, Issue 02, September 2009, pp 323-337 (arXiv:0808.1518)
A review of some aspects of constructive Gelfand duality is in section 2 of
Revised on February 16, 2014 18:31:58
by John Dougherty?