Commit 2023-02-15 07:48 5965ba40

View on Github →

feat: port CategoryTheory.Functor.Currying (#2298)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Functor/Currying.lean

added def CategoryTheory.curry

added def CategoryTheory.curryObj

added def CategoryTheory.currying

added def CategoryTheory.flipIsoCurrySwapUncurry

added def CategoryTheory.uncurry

added def CategoryTheory.uncurryObjFlip

added def CategoryTheory.whiskeringRight₂