The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

On 08/04/2014 01:05 PM, Jonathan wrote:
> On 08/04/2014 01:02 PM, Guillaume Melquiond wrote:
> > 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
>
> True \/ True is not isomorphic to bool.  Instead, the eerily similar 
> {True} + {True} is isomorphic to bool.  At least if I am properly 
> understanding isomorphisms.
>
> -- Jonathan

The question is the following: what amount of information does a proof 
of a given proposition reveal if you allow to eliminate it to a type in 
Set. If the answer is "none", then the elimination can be allowed. The 
definition of singleton types gives a criterion that ensures it is the case.

Now, you were asking: is the answer to that question the same for proofs 
of two equivalent propositions. No, as Guillaume showed it : True and 
True \/ True are logically equivalent. Yet, if you allow to eliminate a 
proof of True to Set, you don't reveal anything, whereas allowing the 
same elimination from a proof of True \/ True reveals one bit of 
information. Relaxing the elimination restriction on True \/ True made 
it isomorphic to bool.

Maxime.