The chapter on sets needs a lot of work

[andrejbauer]

The Pi-W-pretopos part of the chapter on sets will take some work before it fits in with the rest of the book. The text is sometimes repetitive, the diagrams are in TiKZ rather than in xypic, there are footnotes to obscure PDFs in the wiki, definitions define two concepts but only one is in \emph, it says "in the present paper", etc. How finished is this, precisely?

Section 9.1.3 should not be called "Voevodsky's Impredicative quotients" but just "Impredicative quotients", and then explain in the text it is something Vladimir came up with.

If you'd like me to help with any of this, let me know. For example, I can turn TiKZ to xypic.

[mikeshulman]

On Wed, Mar 27, 2013 at 12:22 AM, Andrej Bauer notifications@github.com wrote:

Section 9.1.3 should not be called "Voevodsky's Impredicative quotients"
but just "Impredicative quotients", and then explain in the text it is
something Vladimir came up with.

Or, better, in the Notes. And also mention that it's a simple
adaptation of a well-known construction in topos theory, which in turn
is a simple generalization of the standard construction in set theory.

Some stuff on quotients is going to appear earlier in Ch 5, but it's
tricky because right now it's all intertwined with effectiveness,
which we probably don't want to get into in Ch 5 -- or do we?

[awodey]

On Mar 27, 2013, at 1:08 AM, Mike Shulman notifications@github.com wrote:

On Wed, Mar 27, 2013 at 12:22 AM, Andrej Bauer notifications@github.com wrote:

Section 9.1.3 should not be called "Voevodsky's Impredicative quotients"
but just "Impredicative quotients", and then explain in the text it is
something Vladimir came up with.

Or, better, in the Notes. And also mention that it's a simple
adaptation of a well-known construction in topos theory, which in turn
is a simple generalization of the standard construction in set theory.

Some stuff on quotients is going to appear earlier in Ch 5, but it's
tricky because right now it's all intertwined with effectiveness,
which we probably don't want to get into in Ch 5 -- or do we?

it would be better to disentangle the construction(s) of quotients from the discussion of effectiveness, I think, and move the basic construction to ch. 5.
then in 9 we go into effectiveness in conection with quotients of sets.
Maybe the general notion of effectiveness for higher types is beyond the scope of the book?

[mikeshulman]

Is it a good use of anyone's time at the moment to turn TikZ diagrams into
xypic? Perhaps eventually we want a consistent look for all diagrams in
the book, but right now maybe we should concentrate on the content.

On Wed, Mar 27, 2013 at 12:22 AM, Andrej Bauer notifications@github.comwrote:

The Pi-W-pretopos part of the chapter on sets will take some work before
it fits in with the rest of the book. The text is sometimes repetitive, the
diagrams are in TiKZ rather than in xypic, there are footnotes to obscure
PDFs in the wiki, definitions define two concepts but only one is in \emph,
it says "in the present paper", etc. How finished is this, precisely?

Section 9.1.3 should not be called "Voevodsky's Impredicative quotients"
but just "Impredicative quotients", and then explain in the text it is
something Vladimir came up with.

If you'd like me to help with any of this, let me know. For example, I can
turn TiKZ to xypic.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/37
.

[awodey]

this chapter is done -- right?