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.
On g+ here is a question about the $n$Lab entry syntactic category asking for references. (“Who originally proved the universal property given there?”)
I wish people would know to take such questions to the $n$Forum. Certainly I would hope that “steering committee” members would do so! (hint :-)
Ok, I was just curious if anyone on G+ who doesn’t frequent the forum might know. Next suggestion would be the categories mailing list, or possibly HoTT list, as there are a bunch of people there with relevant history.
Is that result in syntactic+category#group proved somewhere online? I mean the one that claims that the category of contexts for the theory of group is the opposite of the category of finitely presented groups (disguised in rot13)?
The page links to Lawvere theory, but that just relates the Lawvere theory of groups to the opposite of the category of free groups.
I was looking there really to find out what is known about the structure of (slices of) the category of contexts for a Martin-Löf type theory, pursing the modal thoughts here, where morphisms aren’t just context extensions but any morphisms of contexts.
It should be free groups on finite sets, since a Lawvere theory only uses finite products. I learned this from Jim Dolan, so I don’t know a reference. It probably goes back to Lawvere…
Is there not a difference? The objects of the category of contexts are contexts, such as $\Delta \;=\; a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2$, while the objects of the Lawvere theory of groups are just the powers of the single generating object.
I mean the Lawvere theory should be finitely presented free groups, I’m unsure of the relation to the category of contexts.
Edit: now I check Lawvere theory I see that it is using free groups on finite sets, but just doesn’t specify so after the first slightly ambiguous mention.
Clearly Lawvere theory pertains to the wrong doctrine in this example, since the doctrine one has in mind here is that of finite limits, not finite products. I’m not sure what is the best page to link to instead of Lawvere theory. Finite limit theories are closely related to Gabriel-Ulmer duality though.
One place the general result can be found is Part D of the Elephant (the category of contexts for a finite-limit theory is the opposite of the category of finitely-presented models in Set).
1 to 8 of 8