category_theory.limits.pi_obj

pi_obj f computes the product of a family of elements f. (It is defined as an abbreviation for limit (functor.of_function f), so for most facts about pi_obj f, you will just use general facts about limits.)

category_theory.limits.sigma_obj

sigma_obj f computes the coproduct of a family of elements f. (It is defined as an abbreviation for colimit (functor.of_function f), so for most facts about sigma_obj f, you will just use general facts about colimits.)