The Coq mailing list

[Max New <maxsnew AT gmail.com>]

I think it was sarcasm. The factual error is that McBride's thesis says "John Major was the LAST ever leader of the Conservative Party to be Prime Minister (1990 to 1997) of the United Kingdom" (emphasis mine) which is clearly not relevant to the contributions of the thesis.

-Max Stewart New

---------- Forwarded message ----------
From: José Manuel Rodriguez Caballero <josephcmac AT gmail.com>
Date: Mon, May 14, 2018 at 10:47 PM
Subject: Re: [Coq-Club] Coq'Art : Who is J.M. ?
To: coq-club AT inria.fr

If I'm not wrong, I read that Conor McBride's thesis contains fatal errors in the comment 21 November 2012 at 13:11 of the discussion : https://homotopytypetheory.org/2012/11/21/on-heterogeneous-equality/#comment-2537

I quote this comment (I don't know if it is sarcasm) :

andrejbauer says:
21 November 2012 at 13:11
And also, strip Connor of his PhD since his thesis contains factual errors.

 

2018-05-14 22:06 GMT+02:00 Christian Doczkal <christian.doczkal AT ens-lyon.fr>:

Its a reference to John Major: https://coq.inria.fr/library/Coq.Logic.JMeq.html

Best,
Christian

On 05/14/2018 10:00 PM, Matej Košík wrote:
> Hi,
>
> While reading the Coq'Art book, I've noticed the following footnote:
>
>   in the French original, page 251 (§ Égalité dépendante)
>
>     Les initiales « J.M. » font référence à un homme politique britannique, et sont le fruit
>     d’une plaisanterie. Les types représentent des classes et l’introduction de cette égalité semble
>     représenter un progrès social, puisque l’on peut énoncer la possibilité que deux individus de
>     classe différente aspirent à être égaux, même si au fond, seuls des individus de même classe
>     pourront effectivement être égaux.
>
>   in the English translation, page 220 (§ Heterogeneous Equality)
>
>     The initials refer to a British political figure and come from a joke. Types represent
>     social classes and introducing this kind of equality is a political trick that looks like
>     social progress. We can now express the idea that individuals from different classes
>     may aspire to be equal, but, in fact, nothing has changed and only individuals
>     from the same class can actually be equal.
>
> Does anyone have an idea who is/was J.M. ?
>