Commit 2020-08-16 06:05 dba30189

View on Github →

feat(category_theory): the category of indexed families of objects (#3735) Pulling out a definition from #3638, and add some associated basic material.

Estimated changes

Modified src/category_theory/graded_object.lean

deleted def category_theory.graded_object.comap

deleted def category_theory.graded_object.comap_comp

modified def category_theory.graded_object.comap_eq

deleted def category_theory.graded_object.comap_id

deleted theorem category_theory.graded_object.comp_apply

deleted theorem category_theory.graded_object.id_apply

Created src/category_theory/pi/basic.lean

added def category_theory.functor.pi

added def category_theory.nat_trans.pi

added def category_theory.pi.comap

added def category_theory.pi.comap_comp

added def category_theory.pi.comap_eval_iso_eval

added def category_theory.pi.comap_id

added theorem category_theory.pi.comp_apply

added def category_theory.pi.eval

added theorem category_theory.pi.id_apply

added def category_theory.pi.sum

Modified src/category_theory/products/associator.lean

Modified src/category_theory/products/basic.lean