And for those who like their math hard to understand (and rigorous): "The Derivative of a Regular Type is its Type of One-Hole Contexts" (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.8...)

It's cited as "Conor's paper" in your article. But the link there doesn't work.