The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 04/08/2014 18:20, Jonathan wrote:
> > How can you argue that a value of type "False \/ P" contains no
> > information? There are two constructors!
>
> I can have a rewrite rule "False \/ P <-> P", which of course is
> reversible.  I am under the impression that a rewrite, by being
> reversible, demonstrates that the two sides contain the same
> information.  So, there must not be any extra information in the "False
> \/" part, so to speak.  Is that incorrect?

Yes. As already pointed out by Arnaud, True \/ True is equivalent to 
True, which is a singleton type, yet it is isomorphic to bool, which is 
definitely not a singleton type. So just knowing about an equivalence is 
not enough for deciding whether a type can be destructed.

Best regards,

Guillaume