here's the trick

for any definable functors F and G, any term of type ∏_X:Type(F(X)→G(X)) must be a natural transformation.

Bonus: set theory in 10 simple axioms: https://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html