For the dummies like me, what is it that is meant with carrier and group here below?
So when we say that the carrier of a group is a set, it doesn’t have
to be specifically a ZF set; but if we imagine collecting up all
groups as a single entity, that warning light should flash. It’s
dangerous to take the collection of all sets as a single entity, then
to build on top of that. And yet, that is precisely what is done in
category theory, again and again.
"Carrier" isn't a mathematical term, they're just using that word in place of the word "set" to distinguish it from ZF sets. "Group" refers to a specific kind of mathematical structure[0], but it's just given as an example. The important part is that any object can be part of a group, so if the collection of all groups existed as an object, then it would also be part of a group, indirectly containing itself and leading to paradox.
I don't think you're quite right. "Carrier" is absolutely a mathematical term, referring to the set of elements of a group, as opposed to the group operation. That is, a group is defined as a binary operation satisfying the group axioms, on the elements of a certain carrier set.
For those unfamiliar with groups, one way to comprehend groups (by the Cayley theorem) is to essentially imagine groups to be sets of permutations (and in this case, the Carrier set would be the set of permutations, with the group operation being composition of permutations).
I'm not sure I'm any convinced by your argument of the collection of all groups being a group either, and whether that was what was referred to by the author. In any case, I don't think that follows the usual form of the Russell's paradox or Girard's paradox. I'm fairly certain that the "warning light" that the author mentions in relation to the set of all groups is about the set being too large to be consistently considered a set, rather than anything circularly related to groups.
"Carrier" is much more a minority slang than a well-known mathematical term. "Carrier set" is sometimes mentioned as an alternative, but the common term for that is "underlying set".
I have no idea what TFA tries to say, it seems to argue about aesthetics, I am not really into that. If it is very clear, and the authors enthusiasm about their favourite is sticky then sure, but TFA is unclear to me.
It seems to me that the author is attempting to put together some analysis on the essential meaning, purposes, and distinctions of type theory and set theory. While what on offer may not satisfy you or me, it seems a task worthy of doing.
