I have reverted the edit from #2 (which was an incomplete duplication of just the same material we just criticized in another thread here).
I’d like to appeal to all “Anonymous” contributors on type theory matters to think twice before making edits: If you don’t dare to sign your contribution with your name, then maybe that means you are not ready yet to edit here. You can still discuss on the nForum, ask questions etc.
]]>You have now added also here exactly what we just discussed in the other thread here.
Why the confusion? I see it’s done correctly already in the HoTT book, p. 201. You could copy from there.
]]>added reference
free groups appear in section 6.11
Anonymous
]]>adding formation and introduction rules for the free group of a type in type theory
Anonymous
]]>added pointer to §6.2 in Symmetry
]]>