Theorems · Definition · category theory

CategoryTheory.Limits.piObj

{β : Type w} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (f : β → C) → [CategoryTheory.Limits.HasProduct f] → C

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

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Products

Cited by

237 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 80 definitions · uses propext, Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasProduct