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.
A few minor issues that are easily addressed:
The concern I have with the page is that the main theorem is really nothing about (algebraic) theories: it’s an immediate consequence of the (discrete) Grothendieck construction, as you explain in the proof. It’s not clear that this deserves its own name. Perhaps it would be better to explain that this is a useful consequence of the Grothendieck construction on the Grothendieck construction page?
1 to 2 of 2