I was really stunned reading Algebra, chapter 0 when I saw the idea of "group object" that can be expressed in any category. I never thought to ask what is the group object in the category of groups? The answer is abelian groups!
To prove this you NEED to use the Eckmann-Hilton argument.
Suppose you have a group object made up of the group $(G,\cdot)$ with morphisms $\circ$, identity and inverse. Then what you can do is show that $\cdot = \circ$ and they are both commutative.
We need to show that $$(a \circ b) \cdot (c \circ d) = (a \cdot c) \circ (b \cdot d).$$
I wasn't able to figure this out myself, I played around with the equations for a while but it's very very difficult! It's also extremely simple.
The proof is to take $\circ((a,b)\cdot^2(c,d))$ and then reduce it in two different ways.
Notice that we didn't use inverses at all? This proof equally applies to monoid objects in the category of monoids.
Caught a really interesting by Andrej Bauer about constructive maths <https://www.youtube.com/watch?v=zmhd8clDd_Y>.
Constructively there is a subset of the natural numbers that isn't finite or infinite! He also talked about a way to reorganize topology to defeat the Banach-Tarski Paradox, that's brilliant!
I thought about proving this in normal set theory, Define the finite sets $F_n = \{ i \in \mathbb N | i \le n \}$. Let $S \subset \mathbb N$ then by excluded middle either
We can conclude in the first case so it remains to conclude in the second - in that case we will show $|S| = |\mathbb N|$. We know $|S| \le |\mathbb N|$ since it's a subset.
We know $S$ is non-empty (it's not isomorphic to $F_0$) so take $s_0 \in S$. We know $S \setminus \{s_0\}$ is not empty, ... this continues forever. $|\{s_0,s_1,s_2,\cdots\}| = |\mathbb N|$ and the collection is a subset of $S$ so $|\mathbb N| \le |S|$.
I also learned about a very strong constructive axiom that can be added to a system <https://en.wikipedia.org/wiki/Church's_thesis_%28constructive_mathematics%29> which implies the negation of excluded middle!
In the slides here <http://homes.di.unimi.it/~sel/scuola2006/synthetic_computability.pdf> he mentions a different proof of Cantors theorem! Very interesting. (Maybe it's only a little different though)