Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
It seems wrong to call something a “free group” which is not explicitly of group type and whose universal property (elimination rule) is not with respect to other group types.
If one doesn’t care about explicitly fomalizing the actual universal property of free groups, then there is a slick definition simply as the looping of the reduced suspension type of the pointed set of generators. That’s how free groups are constructed in Bezem et al. Symmetry (pp. 167). And if we identify groups with pointed connected 1-truncated types, then this is essentially the expected form of the universal property, after all.
On a different note, it is not good to typeset formulas extending horizontally way over the page margin. Not if you care your formulas to be read by humans instead of by machines. Also, in your case the line breaks easily suggest themselves: Just arrange the list of antecedents vertically instead of horizontally, using an array-environment. An example of how to readably typeset large inference rules is here.
This definition is missing a set-truncation in the introduction rules, for the same reason why free monoids have a set-truncation in their introduction rules and lists do not. I think that currently the rules result in the free infinity-group on .
But this renaming makes the problem worse: What you wrote exhibits the -group structure even less than group structure! What you define is — presumably — the underlying type of an -group type.
By the way, there are at least 3 spurious closing brackets in your code (far beyond the right margin, one has to scroll horizontally to spot them…)
More accurate but less compelling. Why not stick with the original title “free group type” and write the proper definition? That would be useful. If you get stuck, you can take the Symmetry-book as a guide.
By the way, if you can’t spot them (understandably, given the formatting) you can find the syntax errors in your code by searching for the string “”. The first occurrence is correct, but for the following ones the second closing bracket is spurious.
I see that you made a silent effort to fix the horizontal overflow. But you still carry those syntax errors around: I count 9 (nine) occurrences of what is now UTFIG(A)) with a spurious closing bracket.
Apart from your struggle with the typesetting, it’s weird that you write random code, without daring to assign a name to it, and then start wild guesses on what it might describe and what title the entry might carry. You just made up this UTFIG business on the spot after the comment in #3, I don’t think you have an idea how to define in IG, much less a FIG or anUTFIG. You are just guessing.
This entry deserves to be deleted.
1 to 9 of 9