[FOM] constructive Tychonov

[Andrej Bauer]

Robert Black wrote:
> Is there a constructively provable version of the Tychonov product 
> theorem? And if there is, exactly what does it say, and what 
> definition of 'compact' does it use?

Yes, see for example Steve Vicker's "Some constructive roads to
Tychonoff", published in "From Sets and Types to Topology and Analysis:
Towards Practicable Foundations for Constructive Mathematics", Edited by
Laura Crosilla and Peter Schuster, Oxford University Press, 2005,
http://www.oup.com/uk/catalogue/?ci=9780198566519

The paper can be downloaded at
http://www.cs.bham.ac.uk/~sjv/InfiniteTych.pdf

Best regards,

Andrej