Solution (source code)

= Solution

Because $\kappa_0<\kappa_1=\operatorname{crit}(j_1)$, the definition of the <critical point of an elementary embedding> immediately gives
$$
j_1(\kappa_0)=\kappa_0.
$$

To evaluate $j_0(\kappa_1)$, first use the regularity of the measurable cardinal $\kappa_1$. Every function $f:\kappa_0\to\kappa_1$ has bounded range, so every ordinal below $j_0(\kappa_1)$ lies below $j_0(\beta)$ for some $\beta<\kappa_1$. Hence
$$
j_0(\kappa_1)=\sup_{\beta<\kappa_1}j_0(\beta).
$$
The <measurable cardinal is a strong limit cardinal>[strong-limit property] of $\kappa_1$ gives $\beta^{\kappa_0}<\kappa_1$ for every $\beta<\kappa_1$. There are therefore fewer than $\kappa_1$ functions $\kappa_0\to\beta$, which implies $j_0(\beta)<\kappa_1$. On the other hand $j_0(\beta)\geq\beta$. Taking suprema yields
$$
\boxed{j_0(\kappa_1)=\kappa_1,
\qquad j_1(\kappa_0)=\kappa_0,}
$$
the <two measurable cardinals under an ultrapower embedding> formula.