Library HoTT.Categories.ExponentialLaws.Law2

The law that a sum in an exponent is a product

yⁿ⁺ᵐ ≅ yⁿ × yᵐ

Require ExponentialLaws.Law2.Functors.
Require ExponentialLaws.Law2.Law.

Include ExponentialLaws.Law2.Functors.
Include ExponentialLaws.Law2.Law.