Port exponential laws proofs

Port the proofs of the exponential laws from HoTT-categories.

There's slow, at about 2m total, increasing the total compilation time from 3m20s to 5m12s.  This isn't so terrible that I feel bad about asking these to be merged, anymore.

This is on top of #418.