February 1st
Today I learned the definition of a natural transformation. These, are more or less, maps—or homotopies—between functors. Actually, because I know some homotopy type theory, I'll present these as homotopies. Fix categories $\mathcal C$ and $\mathcal D$ with two functors $F,G:\mathcal C\to\mathcal D.$ Formally, a natural transformation $\eta$ is, type-theoretically, the data\[\eta_\bullet:\prod_{X:\mathcal C}F(X)\to G(X)\]which commutes with $F$ and $G$ nicely. In other words, $\eta$ is made up morphisms $\eta_X:F(x)\to G(X),$ and we require the following diagram to commute.
As an example, in the category of vector spaces over $k,$ we have a natural transformation from $\op{id}$ to the endofunctor $V\mapsto V^{\vee\vee}$ the double-dual of $V.$ Proving this is not terribly enlightening: the required $\eta_V$ takes $v\in V$ to $(T:V\to k)\mapsto Tv\in V^{\vee\vee},$ and this works. In fact, if we restrict our view to finite-dimensional vector spaces, this natural transformation is made up of isomorphisms, and we call $\eta$ a natural isomorphism.
Let's make the analogy to homotopy type theory explicit. Viewing a morphism between objects in a type $A:\UU$ as a "path'' between them, functions between types become functors for free. To be explicit, this amounts to the statement\[\prod_{(x,y:A)}(x=_Ay)\to(f(x)=_Bf(y)),\]where $f:A\to B.$ Now our natural transformation $\eta$ goes between two functor/functions $f,g:A\to B,$ in our analogy that $\to$ is $=$ for objects, we see\[\eta_\bullet:\prod_{x:A}f(x)=_Bg(x)\]in terms of homotopy type theory. That is, $\eta$ is just a witness for the $f\sim g,$ so natural transformations are really just homotopies in this analogy.