If we build L but use second-order definable power set rather than first-order, we get HOD, assuming ZFC in the background. This result, due to Myhill and Scott, is well-known. One may wonder whether AC is necessary here. Szczepaniak showed that the answer is yes: we can have ZF models where these two come apart. This is something that I’ve long wanted to understand, but the outdated notation has been fuel to my procrastination. (Isn’t it a good thing that we now have AI to translate old math in modern notation for us?) The notes give a modern exposition of Szczepaniak’s construction, making the symmetric-extension argument explicit and expanding the key steps.