Exponential Laws

We want to have the following as subdirectories/modules, not at top level. Unfortunately, namespacing in Coq is kind-of broken (see, e.g., https://coq.inria.fr/bugs/show_bug.cgi?id=3676), so we don't get the ability to rename subfolders by Including into other modules.

Laws about the initial category

x⁰ ≅ 1

0ˣ ≅ 0 if x ≠ 0

Laws about the terminal category

x¹ ≅ x

1ˣ ≅ 1

The law that a sum in an exponent is a product

yⁿ⁺ᵐ ≅ yⁿ × yᵐ

The law that exponentiation distributes over product

(y × z)ⁿ ≅ yⁿ × zⁿ

Currying

(yⁿ)ᵐ ≅ yⁿᵐ