Instead of spending time beating one’s head against Russell and Whitehead, I would advise reading Homotopy Type Theory (aka the HoTT Book). Dependent types are cool and mind-expanding, but higher inductive types are downright mind-altering. The Little Schemer/Typer could be used as a preparatory text to gear one up for HoTT. It also has the advantage of being a bit more applicable to functional programming languages,…
But I find univalence axiom intriguing. I am interested in different approach to types, using triage calculus, which is more "materialist" than "structuralist" - type is given by the structure of the (quoted) term in normal form (unlike lambda calculus, triage calculus makes quoting easy). And I feel like univalence is related to quoting, something like if the two quoted terms are equal under "standard self-interpreter", then they are equal.