We can evaluate a power series on the real line, or we can evaluate it on the unit circle in the complex plane. The latter gives us Fourier series. We can also evaluate it on the whole complex plane. These three options also show up in the continuous transforms, giving the Laplace transform on the real line, the Fourier transform, and the Laplace transform on the entire complex plane. The function being transformed is the analogue of the coefficients of the power series, and the function you get after transforming is the analogue of the function you get when you evaluate the power series.

The coefficient of $x^k$ of the characteristic polynomial $det(xI + L)$ is the number of ways to take a subset of the edges of the directed graph such that the connected components form k directed trees.

I guess another way to ask the same question is: where exactly does this proof fail for System F?

I was worried about the ∗ at the end of R : A -> A -> ∗. What about that one? Doesn't this make Set : □, which means that you can't instantiate A with Set?

I think I understand how this works with * : *, but could you elaborate how this works in System U? I'm assuming that the construction of {x | P x} relies on instantiating A : * with Set itself somehow? Is that not disallowed in System U, since Set : □ and not Set : *? Or do we have A : □ but still R : A -> A -> *?

If the state space has dimension n > 1 you can still divide n-forms. For example in n=2 you can do (dx /\ df) / (dx /\ dy), which turns out to be the partial derivative df/dy holding x constant.

Isn't it the case that if there constructively exists an element in each set then there constructively exists an element in the product? The constructive existence already chose an element of each set for us (namely, the one that was constructed).

You can also do Gram-Schmidt on the indefinite inner product $<x,y> = x^t A y$. It finds a basis in which the inner product looks like a diagonal matrix with only $1,0,-1$ entries.

Actually, you don't even need Maxwell's equations. Using only the principle of relativity you can deduce the form of the Lorentz transformation with some unknown parameter c with units of speed. The Galilean transformation has $c=\infty$, the Lorentz transformation has c = 3*10^8 m/s.

Do you mean X -> Bool instead of Bool -> X?

You can calculate the signed area of the polygon and check if it is positive or negative.