У Жирара все просто, на уровне парадокса Рассела - на то, как я понял, и завели люди различие между types и kinds. А тут что-то хитренькое... для меня, в смысле.

Студенты классные. У меня все хреново в этом смысле. Для формального доказательства ассоциативности объединения множеств в ZFC берут три множества в качестве premises... дальше в таком же духе.