mathlib documentation

category_theory.limits.shapes.finite_products

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 [decidable_eq J] and [fintype J].

Equations
Instances

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