The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

I have some trouble with canonical structures. In one file I have:

Definition isapropimpl_hprop ( X Y : hProp ) : hProp := hProppair ( X -> Y ) 
( isapropimpl X Y (uu1.pr22 _ _ Y) ) .
Canonical Structure isapropimpl_hprop.


which is accepted.

In another one which imports the first I have:


Definition iff (A B: hProp) :=  ( A -> B ) /\ ( B -> A ) .

where /\ has been re-defined for hProp.  

The system complains:

Toplevel input, characters 64-70:
Error: In environment
A : hProp
B : hProp
The term "A -> B" has type "Type" while it is expected to have type 
"hProp".


When I check things by Print Canonical Projections it shows me :

_ -> _ <- uu1.pr21 ( isapropimpl_hprop ) 

What's wrong here?

Vladimir.