Credits in notes to homotopy chapter

[awodey]

Is it really necessary to list exactly who proved what here? It's not done in any other chapter. Moreover, since everything is done by some combination of about 5 people, it doesn't really give that much more information than just saying something like "most of the results were proved by some combination of Dan, Guillaume, ...". The actual credit for who did what will be given in the talks and papers to come later.

[andrejbauer]

Agreed, perhaps the detailed list can be reduced to a couple of sentences about what group of people found and formalized the proofs. As these are mostly the youngsters, it would be nice to give them credit, even though we're not doing that in other chapter notes.

[dlicata335]

Hmm, I think we need to have a more general discussion about how we are attributing the original research in the book, since we seem to be inconsistent about it. For example, the notes to chapter 7 feel like they are at the same granularity as the notes to chapter 6 (which mike wrote, I think, so I'm not comparing two things I wrote), in that they give individual people credit for specific things. Thoughts?

[awodey]

yes, at least the first 2 par.s of notes in 6 are also breaking out everything and assigning individual credit. this doesn't make sense to me, since these are at the same time the authors of the book. I assume people will publish separate papers and get individual credit that way. my thinking on the notes is that they give credit to other people for things not original to us -- as is done n the rest of the notes in 6 and the notes in 7. other views?

On Apr 22, 2013, at 2:47 PM, Dan Licata notifications@github.com wrote:

Hmm, I think we need to have a more general discussion about how we are attributing the original research in the book, since we seem to be inconsistent about it. For example, the notes to chapter 7 feel like they are at the same granularity as the notes to chapter 6 (which mike wrote, I think, so I'm not comparing two things I wrote), in that they give individual people credit for specific things. Thoughts?

— Reply to this email directly or view it on GitHub.

[awodey]

just to be clear: I have no objection to saying general things like: "most of the results in section n.m are due to x, y, and z" -- it's just the detailed attributions that seem out of place -- and likely to lead to an avalanche of further such notes.

[dlicata335]

I'm happy to find some middle ground between the current 6/8 notes and the rest, but here are some arguments for trying to be a little more specific than usual in attribution in the notes:

0) I agree with you that in a normal book it would be strange if the notes to every chapter remarked on what specifically the authors had contributed, because in a research book like this I would take it as given that anything not specifically attributed to someone else is the work of the authors. But this isn't a normal book, in that it has either 16 or 57 authors. The book contains significant amounts of currently unpublished research, and to my knowledge the specific research results (at the level of a definition or a theorem in the book) are generally attributable to 1-5 people, which to me feels like a smaller enough subset that it is worth distinguishing from the 16 or 57.

1) The book is going to be publicly available next month. I expect that lots of people are going to be excited by it and read it before more papers on this stuff appear, which will take months or years, and because of that whatever we say in the book will stick in people's minds better than whatever we say in later papers. It seems wrong to me to have the first publicly available written proofs of big new research results attributed to a vague conglomerate of people, rather than to the people who put the effort in to prove them.

2) We currently give more detailed attributions throughout when there are already papers to cite, by citing the papers. It seems to me like we should be more careful with attribution when there is not already a record of it. Moreover, we want the book to still read well 10 years from now, and I think it will seem unfair (and less useful to people) at that point if the book says "For Pi1(S1), see Licata&Shulman,'13." but not "Brunerie proved the total space of the Hopf fibration." Moreover, it's not totally clear that all of these results will successfully make it into separate papers, and that leaves the historical record at the whims of journal reviewers, when we have an opportunity to set it here.

3) We give some detailed attributions like

The first definition of equivalence given in homotopy type theory was the one that we have called isContr(f), which was due to Voevodsky. The possibility of the other definitions was subsequently observed by various people. Using bi-invertibility as a definition of equivalences was suggested by Andre ́ Joyal.

How would you revise this to fit the less-precise attribution scheme? Particularly for basic definitions, it seems vague to me to say "some of the material in this chapter is due to Voevodsky and Joyal". But if we are attributing basic definitions to specific people, it seems inconsistent not to attribute specific tools (e.g. the flattening lemma) and specific big theorems.

4) It seems likely to me that the book, and not forthcoming papers, will in the long run be people's de facto citation for the techniques/methods/results in it because it, if only because it's a single reference that's easy to remember (e.g. "We use the flattening lemma (see the [HoTT book])"). It would be nice if somewhere in the book it said who developed those things.

On the other hand, I agree that we should avoid an explosion of additional attributions, because it will start to look petty. I could be wrong, but it looks to me like this is what would happen if we tried to make everything about as detailed as Chapters 6/8 currently are: 1) Chapter 1 is not our work. 2) Chapter 2 is common knowledge, in the sense that many people proved these things independently, so I don't think the results need more specific attribution. 3) Chapter 3 is already fairly specific. (Would you cut some of this under the less specific scheme?) 4) A bunch of Chapter 4 is also common knowledge, but maybe there are some more specific attributions for the second half. 5) Chapter 5 is already fairly specific, but we should e.g. attribute identity systems to Aczel. 6) Chapter 6 is already specific. 7) Chapter 7 would get a little more specific. 8) The people most involved in each chapter in part 2 could decide whether it makes more sense to just have a blanket "the results in this section were developed by ..." or whether it makes sense to attribute specific things.

[DanGrayson]

A minor point: something like

Guillaume Brunerie proved $\pi_4(\Sn ^3)$

, which is actually in the book, or

Brunerie proved the total space of the Hopf fibration.

makes no sense. The thing being proved should be a proposition, after all.

On Mon, Apr 22, 2013 at 9:55 AM, Dan Licata notifications@github.comwrote:

I'm happy to find some middle ground between the current 6/8 notes and the rest, but here are some arguments for trying to be a little more specific than usual in attribution in the notes:

0) I agree with you that in a normal book it would be strange if the notes to every chapter remarked on what specifically the authors had contributed, because in a research book like this I would take it as given that anything not specifically attributed to someone else is the work of the authors. But this isn't a normal book, in that it has either 16 or 57 authors. The book contains significant amounts of currently unpublished research, and to my knowledge the specific research results (at the level of a definition or a theorem in the book) are generally attributable to 1-5 people, which to me feels like a smaller enough subset that it is worth distinguishing from the 16 or 57.

1) The book is going to be publicly available next month. I expect that lots of people are going to be excited by it and read it before more papers on this stuff appear, which will take months or years, and because of that whatever we say in the book will stick in people's minds better than whatever we say in later papers. It seems wrong to me to have the first publicly available written proofs of big new research results attributed to a vague conglomerate of people, rather than to the people who put the effort in to prove them.

2) We currently give more detailed attributions throughout when there are already papers to cite, by citing the papers. It seems to me like we should be more careful with attribution when there is not already a record of it. Moreover, we want the book to still read well 10 years from now, and I think it will seem unfair (and less useful to people) at that point if the book says "For Pi1(S1), see Licata&Shulman,'13." but not "Brunerie proved the total space of the Hopf fibration." Moreover, it's not totally clear that all of these results will successfully make it into separate papers, and that leaves the historical record at the whims of journal reviewers, when we have an opportunity to set it here.

3) We give some detailed attributions like

The first definition of equivalence given in homotopy type theory was the one that we have called isContr(f), which was due to Voevodsky. The possibility of the other definitions was subsequently observed by various people. Using bi-invertibility as a definition of equivalences was suggested by Andre ́ Joyal.

How would you revise this to fit the less-precise attribution scheme? Particularly for basic definitions, it seems vague to me to say "some of the material in this chapter is due to Voevodsky and Joyal". But if we are attributing basic definitions to specific people, it seems inconsistent not to attribute specific tools (e.g. the flattening lemma) and specific big theorems.

4) It seems likely to me that the book, and not forthcoming papers, will in the long run be people's de facto citation for the techniques/methods/results in it because it, if only because it's a single reference that's easy to remember (e.g. "We use the flattening lemma (see the [HoTT book])"). It would be nice if somewhere in the book it said who developed those things.

On the other hand, I agree that we should avoid an explosion of additional attributions, because it will start to look petty. I could be wrong, but it looks to me like this is what would happen if we tried to make everything about as detailed as Chapters 6/8 currently are: 1) Chapter 1 is not our work. 2) Chapter 2 is common knowledge, in the sense that many people proved these things independently, so I don't think the results need more specific attribution. 3) Chapter 3 is already fairly specific. (Would you cut some of this under the less specific scheme?) 4) A bunch of Chapter 4 is also common knowledge, but maybe there are some more specific attributions for the second half. 5) Chapter 5 is already fairly specific, but we should e.g. attribute identity systems to Aczel. 6) Chapter 6 is already specific. 7) Chapter 7 would get a little more specific. 8) The people most involved in each chapter in part 2 could decide whether it makes more sense to just have a blanket "the results in this section were developed by ..." or whether it makes sense to attribute specific things.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/165#issuecomment-16792613 .

[awodey]

well, I guess I don't care that much. if some people want specific credit for things, they should take credit in the notes. just one point about:

2) Chapter 2 is common knowledge, ...

4) A bunch of Chapter 4 is also common knowledge, …

what seems like common knowledge to those who learned it from others is often hard-won original research to those who first did it, so don't be too quick to call something "common knowledge" just becasue you're not sure who did it, and don't underestimate what people might want to take credit for once we start crediting this and that to different people.

On Apr 22, 2013, at 4:55 PM, Dan Licata notifications@github.com wrote:

I'm happy to find some middle ground between the current 6/8 notes and the rest, but here are some arguments for trying to be a little more specific than usual in attribution in the notes:

0) I agree with you that in a normal book it would be strange if the notes to every chapter remarked on what specifically the authors had contributed, because in a research book like this I would take it as given that anything not specifically attributed to someone else is the work of the authors. But this isn't a normal book, in that it has either 16 or 57 authors. The book contains significant amounts of currently unpublished research, and to my knowledge the specific research results (at the level of a definition or a theorem in the book) are generally attributable to 1-5 people, which to me feels like a smaller enough subset that it is worth distinguishing from the 16 or 57.

1) The book is going to be publicly available next month. I expect that lots of people are going to be excited by it and read it before more papers on this stuff appear, which will take months or years, and because of that whatever we say in the book will stick in people's minds better than whatever we say in later papers. It seems wrong to me to have the first publicly available written proofs of big new research results attributed to a vague conglomerate of people, rather than to the people who put the effort in to prove them.

2) We currently give more detailed attributions throughout when there are already papers to cite, by citing the papers. It seems to me like we should be more careful with attribution when there is not already a record of it. Moreover, we want the book to still read well 10 years from now, and I think it will seem unfair (and less useful to people) at that point if the book says "For Pi1(S1), see Licata&Shulman,'13." but not "Brunerie proved the total space of the Hopf fibration." Moreover, it's not totally clear that all of these results will successfully make it into separate papers, and that leaves the historical record at the whims of journal reviewers, when we have an opportunity to set it here.

3) We give some detailed attributions like

The first definition of equivalence given in homotopy type theory was the one that we have called isContr(f), which was due to Voevodsky. The possibility of the other definitions was subsequently observed by various people. Using bi-invertibility as a definition of equivalences was suggested by Andre ́ Joyal.

How would you revise this to fit the less-precise attribution scheme? Particularly for basic definitions, it seems vague to me to say "some of the material in this chapter is due to Voevodsky and Joyal". But if we are attributing basic definitions to specific people, it seems inconsistent not to attribute specific tools (e.g. the flattening lemma) and specific big theorems.

4) It seems likely to me that the book, and not forthcoming papers, will in the long run be people's de facto citation for the techniques/methods/results in it because it, if only because it's a single reference that's easy to remember (e.g. "We use the flattening lemma (see the [HoTT book])"). It would be nice if somewhere in the book it said who developed those things.

On the other hand, I agree that we should avoid an explosion of additional attributions, because it will start to look petty. I could be wrong, but it looks to me like this is what would happen if we tried to make everything about as detailed as Chapters 6/8 currently are: 1) Chapter 1 is not our work. 2) Chapter 2 is common knowledge, in the sense that many people proved these things independently, so I don't think the results need more specific attribution. 3) Chapter 3 is already fairly specific. (Would you cut some of this under the less specific scheme?) 4) A bunch of Chapter 4 is also common knowledge, but maybe there are some more specific attributions for the second half. 5) Chapter 5 is already fairly specific, but we should e.g. attribute identity systems to Aczel. 6) Chapter 6 is already specific. 7) Chapter 7 would get a little more specific. 8) The people most involved in each chapter in part 2 could decide whether it makes more sense to just have a blanket "the results in this section were developed by ..." or whether it makes sense to attribute specific things.

— Reply to this email directly or view it on GitHub.

[guillaumebrunerie]

"Brunerie proved the total space of the Hopf fibration" makes no sense. The thing being proved should be a proposition, after all.

Technically speaking, using propositions as types one can prove any type by just inhabiting it. So here is a proof of the total space of the Hopf fibration : (north, base) (or (base2, base) if you use the other definition of S^2).

About the issue, I basically agree with Dan.

[dlicata335]

2) Chapter 2 is common knowledge, ... > > 4) A bunch of Chapter 4 is also common knowledge, … what seems like common knowledge to those who learned it from others is often hard-won original research to those who first did it, so don't be too quick to call something "common knowledge" just becasue you're not sure who > did it,

you're right about that; sorry. I should have been more careful and just said that we are already giving credit to the people I know to give credit to.

anyway, this is just how I feel about the matter. I am curious to hear what more people think the approach to the notes should be, and if most people think that the more specific notes are opening a dangerous can of worms, I'm OK with that. I wouldn't want a fight about credit to ruin the good collaborative spirit that we have.

[dlicata335]

@DanGrayson @guillaumebrunerie point taken about the Hopf fibration. I have acquired a habit of using "pi_k(S^n)" as the name of the theorem that pi_k(S^n) = whatever it is supposed to equal. Do you think this is confusing?

[DanGrayson]

Maybe that would be called the "Types as Propositions" approach to informal mathematics :-)

On Mon, Apr 22, 2013 at 12:19 PM, Guillaume Brunerie < notifications@github.com> wrote:

"Brunerie proved the total space of the Hopf fibration" makes no sense. The thing being proved should be a proposition, after all.

Technically speaking, using propositions as types one can prove any type by just inhabiting it. So here is a proof of the total space of the Hopf fibration : (north, base) (or (base2, base) if you use the other definition of S^2).

About the issue, I basically agree with Dan.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/165#issuecomment-16803044 .

[andrejbauer]

I don't care either, so more detailed credits are ok too. I am kind of convinced by Dan. I do need to write notes for the reals chapter, to explain where I stole it from.

[awodey]

But now, what about crediting the people who really first proved these things -- like, I dunno, Poincare and Hopf and Brouwer and those guys. Should we cite them, too? And didn't Andre' Joyal suggest using the James construction to get pi_4(S^3)? Ages ago, I myself first proposed the idea of doing the Hopf fibration, and I pointed out then that it would give us some more pi_k(S^n)s using Mike's proof of pi_1(S^1), by using the long exact homotopy fiber sequence, which Vladimir had already done. Where does it end?

I suggest we let the young people who need credit get credit, but we also find a way to say that these, too, are ultimately collaborative results. I guess this is the down-side of working together so closely -- no one really knows who's responsible for what. But I think that's also a good thing.

On Apr 22, 2013, at 9:12 PM, Andrej Bauer notifications@github.com wrote:

I don't care either, so more detailed credits are ok too. I am kind of convinced by Dan. I do need to write notes for the reals chapter, to explain where I stole it from.

— Reply to this email directly or view it on GitHub.

[andrejbauer]

The upside is an immense increase in productivity.

[dlicata335]

I revised the notes to include these comments and be more inclusive about the general colloraborativeness of the results.

I would be very happy to have notes on the classical homotopy theoretic proofs of these things as well, but someone who has some real knowledge on that side should do them, since I think I would do a bad job.

I'm also very happy to have more comments like the above about your suggesting the Hopf fibration and Andre' the James construction and Vladimir doing the LES. At the meeting after I wrote the notes, I said that it was just the stuff I could remember and I asked everyone to fill in their contributions, but thus far it seems to be mostly just the history that I knew about.

Regarding long-exact-sequence specifically, I added a line in the table and said Vladimir formalized it, but is this quite right? The theorem statement uses truncations, and I know he didn't use higher inductives. did he use the impredicative 0-truncation to this?

[awodey]

I don't need to be mentioned here -- that was just meant as an example.

On Apr 23, 2013, at 12:17 AM, Dan Licata notifications@github.com wrote:

I revised the notes to include these comments and be more inclusive about the general colloraborativeness of the results.

I would be very happy to have notes on the classical homotopy theoretic proofs of these things as well, but someone who has some real knowledge on that side should do them, since I think I would do a bad job.

I'm also very happy to have more comments like the above about your suggesting the Hopf fibration and Andre' the James construction and Vladimir doing the LES. At the meeting after I wrote the notes, I said that it was just the stuff I could remember and I asked everyone to fill in their contributions, but thus far it seems to be mostly just the history that I knew about.

Regarding long-exact-sequence specifically, I added a line in the table and said Vladimir formalized it, but is this quite right? The theorem statement uses truncations, and I know he didn't use higher inductives. did he use the impredicative 0-truncation to this?

— Reply to this email directly or view it on GitHub.

[awodey]

I removed myself and Vladimir -- those were supposed to be counter-examples, not suggestions for more details. Also switched first person to passive in a few places. I also removed the word "first" in each item: it goes without saying. I still think this would benefit from being compressed a bit.

[mikeshulman]

I condensed this a little more. Is there more that needs to be done? I'm not sure that trying to give references to the original homotopy-theoretic proofs is a good idea; maybe we could just refer to some standard textbooks?

[DanGrayson]

Those theorems must be in 20 or 30 textbooks, so giving a reference to one of them is perhaps not so useful, since a typical reader will own another.

On Fri, Apr 26, 2013 at 6:50 PM, Mike Shulman notifications@github.comwrote:

I condensed this a little more. Is there more that needs to be done? I'm not sure that trying to give references to the original homotopy-theoretic proofs is a good idea; maybe we could just refer to some standard textbooks?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/165#issuecomment-17106199 .

[awodey]

just say at the beginning that these are of course standard results, and we are only talking about who did the proofs in this new setting.

[dlicata335]

I said what steve suggested and added a reference to hatcher's book, which contains most of these things and is available online. Mike's condensing looks good to me. closing because there is nothing left undone in this discussion; please reopen if there's still something that can be improved.