[FOM] constructive Tychonov

[Robert Black]

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?

I ask because it seems to me that using classical Tychonov with the 
usual definition of compactness as open covers having finite 
subcovers it's rather straightforward to get the fan theorem (without 
going through bar induction) through fans being compact. But I might 
be wrong about that (none of the books I've looked at seem to mention 
it, and I'm rather vague about just what can be carried over from 
classical topology into a constructive setting).

Robert
-- 
PS I am at present in Berlin, which is why this message is coming 
from a gmx address. You can reply either to this address or to my 
usual <Robert.Black at nottingham.ac.uk>.

Robert Black
Dept of Philosophy
University of Nottingham
Nottingham NG7 2RD

tel. 0115-951 5845
home tel. 0115-947 5468
[in Berlin: 0(049)30-44 05 69 96]
mobile 0(044)7974 675620