The Coq mailing list

[Tadeusz Litak <tadeusz.litak AT gmail.com>]

*Factual* is not *fatal*. And yes, it's exactly what Max says. It was perfectly clear in the context of that discussion:

https://homotopytypetheory.org/2012/11/21/on-heterogeneous-equality/#comment-2534

On a side note, the fate of the term got complicated already before Labour lost three elections in a row (2010, 2015, 2017). The explanation of the name was still there in the draft citeseer version of "Elimination with a Motive", Section 3:

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.23.6292&rep=rep1&type=pdf

but it seems to have completely disappeared from the final version of the paper published in TYPES 2000, which uses simply the name "heterogeneous equality":

https://link.springer.com/chapter/10.1007%2F3-540-45842-5_13

Perhaps the referees made him remove it.  But, 1) as Mikhail Bulgakov put it so memorably, manuscripts don't burn, 2) you cannot rewrite history and 3) mathematics and politics do not mix, but create nice names anyway.


On 14/05/18 23:06, José Manuel Rodriguez Caballero wrote:

thank you. because it is not a mathematical error, I think that I will read the thesis. I do not care too much about politics.

2018-05-14 23:04 GMT+02:00 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. ?
>