Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-02 11:34 efa94590

View on Github →

feat(category_theory/whiskering): whiskering nat_trans by functors (#360)

feat(category_theory/whiskering): whiskering nat_trans by functors
simplify whiskering

Estimated changes

Created category_theory/whiskering.lean

added theorem category_theory.whisker_left.app

added def category_theory.whisker_left

added theorem category_theory.whisker_left_twice

added theorem category_theory.whisker_left_vcomp

added theorem category_theory.whisker_right.app

added def category_theory.whisker_right

added theorem category_theory.whisker_right_left

added theorem category_theory.whisker_right_twice

added theorem category_theory.whisker_right_vcomp

added def category_theory.whiskering_left

added def category_theory.whiskering_right