The Axiom of Choice (AC) is one of the basic assumptions of modern mathematics. It has an essential role in much of our understanding of the infinite, particularly in connection with objects at the level of subsets $X$ of the real numbers, and beyond. Its utility notwithstanding, it has various surprising and unintuitive consequences. Large cardinals, which are infinite structures well beyond objects such as the real numbers, are a fundamental discovery of set theory. Although their defining features are far removed from ordinary mathematical considerations, they have a profound influence on the nature of the reals. Large cardinals are natural extensions of the standard Zermelo-Fraenkel axioms for set theory (ZFC, including AC), providing answers to many basic questions which are left unanswered by ZFC alone. They are arranged in a rich and detailed complexity hierarchy. In the early days, it may have appeared that this hierarchy would extend ever upward. However, Kunen proved in the 1970s that the large cardinal hierarchy actually reaches a rather abrupt (and surprising) end. He identified a specific large cardinal notion, and showed that it is inconsistent with ZFC - even though in the half century since then, apparently similar large cardinal notions just below this level have remained immune to this issue. Now Kunen's proof made important use of AC, and it has been open since that time, as to whether AC is necessary. By excluding AC from the basic assumptions, one can study large cardinals at the level of Kunen's inconsistency, and beyond. In recent years, such investigations have begun to reveal significant structure and coherence at such heights. Could it be that these "choiceless large cardinals" are in fact consistent with ZF? If so, how do they relate to the true set-theoretic universe? I will give a general discussion of the themes outlined above, and in particular the paper "On the consistency of ZF with an elementary embedding from $V_{\lambda+2}$ into $V_{\lambda+2}$" (published in Journal of Mathematical Logic). This work focuses on the boundary of the Kunen inconsistency. It shows that the key large cardinal notion refuted by Kunen using ZFC (which is an elementary embedding $j:V_{\lambda+2}\to V_{\lambda+2}$) is in fact consistent with the ZF axioms without AC, assuming that certain well-studied large cardinal hypotheses are consistent. (These well-studied hypotheses sit superficially just below the Kunen inconsistency.) Therefore, modulo these assumptions, Kunen's proof really does require AC. Further, the result (and its proof) adds to the evidence that choiceless large cardinals are natural objects, which should have an important role in our understanding of the universe.