Why is the derivative of a regular type its type of one-hole contexts?
Let us define a function that counts the elements of a type, |()| = 1, |Void| = 0, |Either x y| = |x|+|y|, |(x,y)|=|x|*|y|, |List A| = 0 + |A| + |A|^2 + |A|^3 + ... (because lists can be , [a], [a,b], and so on)
In general the 'size' of any type can be written as a power series (like an infinite polynomial), now for the type |k|*|x|^3, if we punch a hole in it, we get |k|*|x|^2 but we could have picked one of 3 different places to put it so we need to say which one, this gives 3*|k|*|x|^2, and this should be done to every term of a power series.
Since the derivative of a type = the derivative of its powerseries* this explains why we can 'differentiate' a type and get a zipper. (At least it sort of makes sense).
(* why is this true?)