Mozibur says his comment above was intended as a joke.

I'm sure you're striving to optimize this post, but please be aware that each edit bumps this post to the top of the stack and other posts (also vying for attention) down. So if you could condense several improvements into an edit, rather than changing by a single character, it would be appreciated.

@TimothyChow Thanks; I listened again and you're right. Still, I'm not sure how to take this assertion of "doing nothing".

I hope Buzzard joins the discussion. But one thing I found strange is this mention of "chaps" around Voevodsky who haven't done anything with Coq except formalize rings and modules. Did I hear that correctly? It sounded really misleading. Clearly there are extensive libraries of math formalized by Coq; for example, the formalization of the odd order theorem (finite groups of odd order are solvable) by Gonthier et al. was one such tour de force, although not necessarily one developed by the "Voevodsky chaps".

What Paul says is correct, and it resonates most convincingly when you hear an Australian category theorist say it. (I tend to be somewhat lax [haha] in my usage, where any morphism you derive from an adjunction in similar fashion could also be called a "mate". For example, in informal chat, I might also refer to Maxime's $id \to F^\wedge G$ as a mate.)

Yes. Let $\eta: 1 \to F^\wedge F$ denote the unit and $\varepsilon: G G^\wedge \to 1$ the counit. Then form the evident composite $$G^\wedge \stackrel{\eta G^\wedge}{\to} F^\wedge F G^\wedge \stackrel{F^\wedge TG^\wedge}{\to} F^\wedge G G^\wedge \stackrel{F^\wedge \varepsilon}{\to} F^\wedge$$

Any idea how old he was? I don't know the history of the result that any 1-knot in 4-space is equivalent to an unknot, but for some reason thought this would have been known for a long time, even predating Zeeman's birth year.

Convergence would follow if sums of the form $\sum_{n=1}^M \sin(n)\sin(n^2)$ had an upper bound independent of $M$. This is certainly known for sums $\sum_{n=1}^M \sin(n)$. I'm sure it's also true for these sums, but I don't have an immediate proof.

I suggest you try asking your question at MO main, and see what happens. You might get an answer for free!

@creillyucla That's right.

"Arithmetical identities" like $(ab)^c = a^c b^c$, $a^{b+c} = a^b a^c$, and $(a^b)^c = a^{bc}$ can all be understood in the light of cartesian closed categories. The binomial identity $(a+b)^n = \sum_j \binom{n}{j} a^j b^{n-j}$ can understood in terms of extensive categories.

Very interesting answer: +1.