mathlib documentation

category_theory.limits.shapes.finite_products

Categories with finite (co)products #

Typeclasses representing categories with (co)products over finite indexing types.

If a category has all products then in particular it has finite products.

If a category has all coproducts then in particular it has finite coproducts.