The Coq mailing list

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