Library HoTT.Categories.ExponentialLaws.Law4

Currying

(yⁿ)ᵐ ≅ yⁿᵐ

Require ExponentialLaws.Law4.Functors.
Require ExponentialLaws.Law4.Law.

Include ExponentialLaws.Law4.Functors.
Include ExponentialLaws.Law4.Law.