The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Here's my latest attempt at defining a product topology on X * .. * Z
in terms of a condition on X -> .. -> Z -> Prop.  This looks like it's
working OK; and in principle, if I add semantics for the Heyting
algebras, I should be able to inductively prove nice things like "open
(interior A)", "interior A <= A", etc.  But it ends up reversing the
order of variables on the inside, and if I do "intros" when trying to
work with the definitions I get lots of extraneous "prop_embed" in the
types of the intro'd variables.

I was wondering if anybody here might have any ideas on how to make
this prettier (e.g. correct the reverse order issue without making
things too much more complicated), or less cumbersome to work with.
-- 
Daniel Schepler

Attachment: ProdTop2.v
Description: Binary data