I wrote:

> **Puzzle 140.** Show that \\(1_F:F \to F\\), defined this way, really is natural.

Christopher solved it! I'll change his notation to the notation I'm using:

Each naturality square coming from a morphism \\(f : x \to y\\) is of the form \\(F(f) \circ 1_{F(x)} = 1_{F(y)} \circ F(f)\\) which commutes because \\(1_x\\) and \\(1_y\\) obey the left and right unit laws:

\[ F(f) \circ 1_{F(x)} = F(f) = 1_{F(y)} \circ F(f) .\]

> This was weirdly hard for me to write out a proof of, I ?knew? that it was natural because id "doesn't do anything" but figuring out what that actually means formally seemed hard.

Yes, that sort of mental block sometimes kicks in when I have to verify something that seems 'too simple' or 'too obvious'. The solution is just to turn off my intuitions for a while, patiently follow the definitions, and see exactly what needs to be checked.

> **Puzzle 140.** Show that \\(1_F:F \to F\\), defined this way, really is natural.

Christopher solved it! I'll change his notation to the notation I'm using:

Each naturality square coming from a morphism \\(f : x \to y\\) is of the form \\(F(f) \circ 1_{F(x)} = 1_{F(y)} \circ F(f)\\) which commutes because \\(1_x\\) and \\(1_y\\) obey the left and right unit laws:

\[ F(f) \circ 1_{F(x)} = F(f) = 1_{F(y)} \circ F(f) .\]

> This was weirdly hard for me to write out a proof of, I ?knew? that it was natural because id "doesn't do anything" but figuring out what that actually means formally seemed hard.

Yes, that sort of mental block sometimes kicks in when I have to verify something that seems 'too simple' or 'too obvious'. The solution is just to turn off my intuitions for a while, patiently follow the definitions, and see exactly what needs to be checked.