added pointer to:

Univalent Foundations Project, Thm. 2.1.6 in:

*Homotopy Type Theory – Univalent Foundations of Mathematics*2013 (web, pdf)Kristina Sojakova,

*Syllepsis in Homotopy Type Theory*, 2021 (pdf)

added pointer to:

- Tomer Schlank, Lior Yanovski,
*The ∞-Categorical Eckmann-Hilton Argument*, Algebr. Geom. Topol. 19 (2019) 3119-3170 (arXiv:1808.06006, doi:10.2140/agt.2019.19.3119)

added pointer to the original argument

- Beno Eckmann, Peter Hilton, Theorem 1.12:
*Structure maps in group theory*, Fundamenta Mathematicae 50 (1961), 207-221 (doi:10.4064/fm-50-2-207-221)

reviewed (somewhat imperfectly!?) in:

- Beno Eckmann, Peter Hilton, Theorem 5.4.2 in:
*Group-like structures in general categories I multiplications and comultiplications*, Math. Ann. 145, 227–255 (1962) (doi:10.1007/BF01451367)

Gives a trivial proof by string diagram.

Yuxi Liu

]]>A bit about two symmetric idempotent operations without units, which I often need to remind myself of. I am not sure if this goes here, but the proof is quite similar to the standard EH proof. Happy to move it somewhere else if need be.

]]>Thanks, Todd.

]]>Got rid of the redundancy noted in the (nForum) discussion.

]]>Getting back to the mathematical content, I don’t see why in step 2 in the proof (each operation preserves the other’s identity element) is needed. When I presented this proof to my class yesterday, someone asked about this, because it didn’t seem to be used further down. And it follows once you know the identities and the operations coincide, no? On Twitter, Eugenia suggested (something to the tune of) it might be to prove that the first binary operation (say) is a unital magma object internal to the category of unital magmas (though she phrased it as a monoid object in $Mon$).

]]>I think that you put too much emphasis on that

That’s no fair. I said several times that I’d rather give up this discussion here than insist on my point.

Your respons sounds like a non sequitur to me, so I think that we’re still talking past each other. (How insistent you are with a point is independent of how much emphasis that point puts on something.)

I don’t think that you have behaved unreasonably.

]]>Urs, I think incorporating common wisdom of many people in early phases of $n$lab is worthy its trouble in long run. Of course, nobody needs to sacrifice for it now or ever, but I do not feel that most of the discussions in past several bursts of discussions on technical background and organization of $n$lab were fruitless. On the contrary, with few notable exceptions.

]]>I think that you put too much emphasis on that

That’s no fair. I said several times that I’d rather give up this discussion here than insist on my point. We do need to find a more effective way to deal with such issues, it steals too much time. Unfortunately, when I said this before here (suggesting that it would be more effective to discuss this in person) even more discussion ensued.

You all please put your theorem-environments where you like.

]]>Toby, we must be talking past each other.

I think that we are a bit, but it probably does not matter too much, since I agree with this.

I am advocating to put each proof in a proof-environment.

Perhaps I think that you put too much emphasis on that, but it’s not worth arguing about.

I didn’t like where you put the proof environment at Eckmann-Hilton argument, but I’m happy with where I put it. If you’re happy with that too, then we’re OK.

so that it is possible to have a computer program scan the Lab for, say, all theorems and proofs asserting existence of limits in some categories

Since this has nothing to do with the Eckmann–Hilton argument, I’ve responded to it here.

]]>Formatted how?

Toby, we must be talking past each other.

I think it would eventually be good if the nLab pages have uniform formatting of formal definition/lemma/theorem/proof content. Uniformly formatted such that it is easy for the reader to spot what is supposed to be a formal statement, what is supposed to be a formal proof, and uniformly marked in the source code, so that it is possible to have a computer program scan the Lab for, say, all theorems and proofs asserting existence of limits in some categories (that’s what this student is trying to do).

Therefore I am advocating to put each proof in a proof-environment.

I think this is a simple means to increase a certain robustness of the nLab content and a little step in making the content we provide here be usefully extractable, hence a little step in improving the effect that our efforts here have.

]]>@Toby Mea culpa … probably.

Is it you who keeps putting link breaks in the opening of the environments?

I have tried to see what determines the formatting, looking at pages that look good with no large breaks, but have been unable to work it out as I sometimes copy source material from a page that looks good, paste where I want it then do a minor edit…. Doh! Large white spaces have appeared from nowhere and I can find no reason. I have tried editing separately (Mac with Textedit) and it still does not look good. (I have guiltily thought ’Well Toby will come behind and clean it up!’ Sorry (and thanks)) I found it difficult to find the necessary formatting advice in FAQs ’How to’ etc. It is probably there but I cannot find it.

]]>RIP Hilton; good luck Zoran.

]]>I’ve started a new thread if anybody wants to continue the general discussion.

]]>@ Zoran

If it helps, the person who’s extracting things from the nLab (I vaguely remember the conversation) is *not* going to be writing over our material. So Urs is just trying to have the Lab in a state where it’s useful for him.

@ Tim

(The result does not always look quite as nice as I had hope but someone usually notices this and smooths out the formatting :-))

Is it you who keeps putting link breaks in the opening of the environments?

]]>If you don’t put it in an environment, then there’s nothing to globally change,

Exactly. So that’s too bad if we have all other proofs elsewhere formatted uniformly.

Formatted how?

The only thing that the proof environment does it to write ‘Proof.’ at the beginning and put a box at the end. If you put the proof in a section labelled ## Proof ##, then you don’t need this. If someday we change the period to a colon or fill the box in black, that’s irrelevant for a proof that doesn’t use the environment. (It *is* relevant for people who write ‘Proof.’ and put in the box by hand. I agree that people should use the environment instead of that.)

Dear Zoran,

Not to be a gossip, but…

When I went to the MWTS, you came up in a conversation that I was listening to (unfortunately, I’m not at a high enough level to actually participate), and you’re very highly regarded, so take heart!

]]>Thank you for kind concern, Urs. I applied to only one place (the one I mentioned to you, Urs, a couple of weeks ago). Long term I can probably promote my adjunct assistant professorship at the university, math dept, into a full time assistant professorship, but this needs a decision and much preparation and administrative help of colleagues, what means delay of roughly a year. Legally I could try to extend present position for another 3 months or so (more than that could happen if some things improve in the meantime), and-or take another few months of a kind low-paid guest stipend at one German University, which I discussed with a person there. I skipped applying for a nice two year position of my profile (nc geometry) in Denmark, what I feel sorry now. The whole thing is not that bad, except for loosing additional peace (more worries, including for my parents and relatives) and stability; so it will be diffcult to stay focused. I do not have short-term problem with money, living in my own appartment (not really my own, but effectively, in a family) and having reasonable savings. I also have some students in Zagreb who I care about and would not like to go too far from them, unless I can help them in some better way.

]]>Sorry to hear that, Zoran. What’s the perspective?

]]>UK is too far from my parents, unfortunately. I will try to stay near by.

]]>Keep and eye on the jobs in the UK. There are a few around still. Not everything has shut down yet!

]]>