Can boolean algebra be expressed in simply typed lambda caclulus? Boolean algebra can be expressed in untyped lambda calculus in (for example) this way.

true  = \t. \f. t;
false = \t. \f. t;
not   = \x. x false true;
and   = \x. \y. x y false;
or    = \x. \y. x true y;


Also boolean algebra can be encoded in System F in this way:

CBool = All X.X -&gt; X -&gt; X;
true  = \X. \t:X. \f:X. t;
false = \X. \t:X. \f:X. f;
not   = \x:CBool. x [CBool] false true;
and   = \x:CBool. \y:CBool. x [CBool] y false;
or    = \x:CBool. \y:CBool. x [CBool] true y;


Is there a way to express boolean algebra in simply typed lambda calculus? I assume that answer is NO. (For example, Predecessor and lists are not representable in simply typed lambda-calculus.) If the answer is NO indeed, is there a simple intuitive explanation, why it is impossible to encode booleans in simply typed lambda calculus?

UPDATE: We assume that there are base types.

UPDATE: The negative answer with explanation was found here (Comment "Here's a proof sketch to show that simply-typed lambda calculus with products and infinitely many base types does not have booleans.") This is what I was looking for.
The OP wrote above that the question is answered by a post on @AndrejBauer's blog.