Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
  1. starting page on free group types


    v1, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJan 24th 2023

    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.

  2. 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 AA.

  3. on second thought this is probably more accurate


    diff, v2, current

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJan 24th 2023

    But this renaming makes the problem worse: What you wrote exhibits the \infty-group structure even less than group structure! What you define is — presumably — the underlying type of an \infty-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…)

  4. more accurate


    diff, v3, current

  5. classifying -> underlying


    diff, v3, current

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJan 24th 2023

    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 “(A))(A))”. The first occurrence is correct, but for the following ones the second closing bracket is spurious.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJan 25th 2023

    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.