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.

@[class]

A category has finite coproducts if there is a chosen colimit for every diagram with shape discrete J, where we have [fintype J].

Instances of this typeclass

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