Library HoTT.Categories.ExponentialLaws.Law3

The law that exponentiation distributes over product

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

Require ExponentialLaws.Law3.Functors.
Require ExponentialLaws.Law3.Law.

Include ExponentialLaws.Law3.Functors.
Include ExponentialLaws.Law3.Law.