Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-08 00:32 02cf7a61

View on Github →

feat(category_theory): product categories and functor categories (#239)

Estimated changes

Created category_theory/functor_category.lean

added theorem category_theory.functor_category.comp_app

added theorem category_theory.functor_category.id_app

added theorem category_theory.functor_category.nat_trans.app_naturality

added theorem category_theory.functor_category.nat_trans.naturality_app

Created category_theory/products.lean

added theorem category_theory.functor.product_map

added theorem category_theory.functor.product_obj

added theorem category_theory.nat_trans.product_app

added theorem category_theory.product_category.comp

added theorem category_theory.product_category.id