Ssreflect Users Discussion List

[Bas Spitters <>]

Hi Frederic,

This is called Hedberg's theorem. While writing the book on homotopy
type theory we had some mild simplifications:
books.google.nl/books?id=LkDUKMv3yp0C&pg=PA219

Best,

Bas

On Wed, Oct 23, 2013 at 12:22 PM, Frédéric Chyzak
<> wrote:
> Benjamin, Georges, thanks for your comments.
>
>
>
> On Wednesday 23 October 2013 09:54:48 Benjamin Werner wrote:
>
>> Not about the error message but :
>
>>
>
>> Proving that equality proofs are equal cannot be done in general in Coq's
>
>> type theory. (whether this is good, is bad, is a minor defect of the type
>
>> theory, etc is another story). Here your lemma is true because equality is
>
>> decidable over the considered type (boolean).
>
>
>
> I had heard about these general facts.
>
>
>
>> In SSR, this is proved generally for eqtypes by the lemma eq_irrelevance.
>
>
>
> Probably I should have mentioned how I got the error message: I was doing
> the exercise of getting a proof of proof irrelevance for bool, just using
> Coq terms and ssreflect tactics. I am still trying to understand the
> fundamentals and at this point I am not aiming at a general decidable type,
> just at bool. So, I don't use eqtypes. Also, I am looking for a proof that
> speaks to me (== that I can explain to someone).
>
>
>
> (Maybe I can make sense of the / switch after I got the fundamentals.)
>
>
>
> Frédéric
>
>