The Coq mailing list

[José Manuel Rodriguez Caballero <josephcmac AT gmail.com>]

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. ?
>