Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-06 16:50 6eba20b0

View on Github →

feat(category_theory): currying for functors (#981)

feat(category_theory): currying for functors
Update src/category_theory/currying.lean Co-Authored-By: semorrison scott@tqft.net
compacting
fix import
change from review
rfl on same line

Estimated changes

Created src/category_theory/currying.lean

added theorem category_theory.curry.map_app_app

added theorem category_theory.curry.obj_map_app

added theorem category_theory.curry.obj_obj_map

added theorem category_theory.curry.obj_obj_obj

added def category_theory.curry

added def category_theory.curry_obj

added def category_theory.currying

added theorem category_theory.uncurry.map_app

added theorem category_theory.uncurry.obj_map

added theorem category_theory.uncurry.obj_obj

added def category_theory.uncurry