The axioms of set theory – the Zermelo Fraenkel axioms with the Axiom of Choice (ZFC) – are highly incomplete, with many basic questions known to be independent. Large cardinal axioms, a major discovery of the last century, form a natural and com- pelling hierarchy of extensions of ZFC, which resolve many of the unanswered ques- tions. Their investigation is a central program in the foundations of mathematics. In the 1970s, Kenneth Kunen demonstrated, with what is now known as the Kunen inconsistency, that the large cardinal hierarchy has a rather surprising hard upper bound, with the non-existence of elementary embeddings of the form j : V_{λ+2} → V_{λ+2}. This dispelled hopes for potentially much larger cardinals, such as Reinhardt cardinals. However, his proof made strong use of the Axiom of Choice, leaving a long-standing open question, as to whether his result could be proved without it. I will discuss some recent work demonstrating that, assuming the consistency of the large cardinal axiom I0, Choice is in fact necessary. This result is part of a recent body of work, due to various researchers, exploring significant structure in these large cardinals “beyond” the Axiom of Choice, such as Reinhardt cardinals. This structure suggests that these principles are coherent, and could in fact play a foundational role. But their direct conflict with Choice leads to significant questions as to what that role could be, and how they might actually feature in the set theoretic universe.