The Coq mailing list

[Max New <maxsnew AT gmail.com>]

JM is John Major. The joke is in Conor McBride's thesis, section 5.1.3: http://strictlypositive.org/thesis.pdf

-Max Stewart New

On Mon, May 14, 2018 at 10:00 PM, Matej Košík <mail AT matej-kosik.net> 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. ?